Changes between Initial Version and Version 1 of Challenge

Timestamp:

03/11/19 14:58:03 (7 years ago)

Author:

siegel

Comment:

--

Challenge

@@ +1 @@
+
+
+== 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.
+