== 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.