CIVL-C Reference

Almost everything from sequential C is allowed. The standard library is partially implemented, including:

printf, assert, malloc, free, ....

Be sure to include the appropriate headers.

Boolean type: _Bool. Values: 0 and 1.

(Same as C11).

Semaphore operations:

• V(s) = s++
• P(s) = $when (s>0) s--

You could define them as functions, or as preprocessor macros (#define ...)

$proc

the process type. A value of this type refers to a process.

$spawn stmt

create a new process executing stmt. Returns a $proc.

$wait($proc p)

block until process p terminates

$parfor (int i:a..b) f(.. i ..);

spawns threads calling f, one for each i in a..b, waits for them to terminate

assertions:

Use either C's assert (include <assert.h>) or CIVL's $assert. They mean the same thing.

Quantification: $forall and $exists. Examples:

$forall (double x | x>0) x>1 $forall (int i | a<=i && i<=b) p(i) $forall (int i:a..b) p(i)

MPI Reference =============

Constants:

MPI_COMM_WORLD (type MPI_Comm) MPI_STATUS_IGNORE (type MPI_Status*) MPI_ANY_SOURCE (type int) MPI_INT (type MPI_Datatype) MPI_DOUBLE (type MPI_Datatype)

Functions:

MPI_Init(NULL, NULL); MPI_Finalize();

MPI_Init must be called before other MPI functions. MPI_Finalize must be called before termination and after all other MPI functions.

MPI_Comm_size(MPI_Comm comm, int *nprocs); MPI_Comm_rank(MPI_Comm comm, int *rank);

Get the number of processes in the communicator, and the "rank" (ID number) of this process within the communicator.

int MPI_Send(const void *buf, int count, MPI_Datatype datatype,

int dest, int tag, MPI_Comm comm);

Sends a message to the process of rank dest. You can use NULL for buf if count is 0 --- an empty message.

int MPI_Recv(void *buf, int count, MPI_Datatype datatype, int source,

int tag, MPI_Comm comm, MPI_Status *status);

Receives a message from the specified source process. source can be MPI_ANY_SOURCE --- to receive from any source ("wildcard"). status can be MPI_STATUS_IGNORE, if you don't care about the status. Otherwise, declare a variable of type MPI_Status and pass a pointer to it.

int MPI_Sendrecv(const void *sendbuf, int sendcount, MPI_Datatype sendtype,

int dest, int sendtag, void *recvbuf, int recvcount, MPI_Datatype recvtype, int source, int recvtag, MPI_Comm comm, MPI_Status *status);

Combines one MPI_Send operation and one MPI_Recv operation into a single command. It behaves as if the two operations execute concurrently in separate threads. Used to avoid deadlocks that could result if all processes do MPI_Send; MPI_Recv.