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.

$when (expr) stmt

a guarded command. Blocks until expr is true. Executes the first atomic action of stmt atomically with the evaluation of expr to true. Example: $when (s>0) s-- defines Dijkstra's P operation on semaphores. The V operation is just s++. Note that s-- and s++ are both atomic in CIVL-C.

_Bool

The Boolean type. Values: 0 and 1. This is the same as C11.

$proc

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

$spawn stmt

creates a new process executing the statement. Returns a value of type $proc referencing the new process.

$wait($proc p)

blocks until process p terminates

$parfor (int i:a..b) stmt

spawns threads, one for each i in the range a..b, each executing stmt. Waits for them to terminate.

$assert(expr)

An assertion. This is treated exactly the same as C's assert, except with the latter you must include assert.h. CIVL-C has a richer assertion language that C---e.g., you can use quantifiers.

$forall and $exists

Mean what you think. Here are some examples to show the syntax:

• $forall (double x | x>1) x>0 -- for all doubles x that are greater than 1, x is greater than 0
• $forall (int i | a<=i && i<=b) p(i) -- for all i between a and b (inclusive), p(i) holds
• $forall (int i:a..b) p(i) -- same as above, but more convenient

MPI Reference

Constants

• MPI_COMM_WORLD (type MPI_Comm)
• MPI_STATUS_IGNORE (type MPI_Status*)
• MPI_ANY_SOURCE (type int)
• MPI_ANY_TAG (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.