A Dissemination Barrier

Designing efficient barriers is a big problem in concurrency theory. A barrier is a synchronization operation that is invoked by all threads or processes in a concurrent system. The defining property is that no process can leave the barrier until every process has entered the barrier. Of course, a barrier should not deadlock --- once all processes have entered, they should all be able to leave. A barrier should also be re-useable, i.e., it can be invoked more than once.

The dissemination barrier works as follows. There are n processes, numbered 0 .. n-1. The order is treated as cyclical. The protocol goes through ceil(log₂(n)) stages, i=0,1,.... At stage i, each process sends a message to the process 2ⁱ to its "right", and waits to receive a message from the process 2ⁱ to its "left". The content of the message is irrelevant (and can be empty).

Challenge 1: Design a dissemination barrier using MPI. Verify it up to some bound on the number of processes using CIVL.

Challenge 2: Design a dissemination barrier using semaphores. Verify it up to some bound on the number of threads using CIVL.

In both cases, there should be a function named barrier (possibly with parameters) that all processes/threads call in order to participate in a barrier. The function could use global variables.

In both cases, part of the challenge is to come up with an appropriate driver that tests the barrier. Try to develop the most universal (challenging) driver you can. Can you make one that guarantees the barrier is correct?

CIVL-C Reference

For installation instructions: CIVL Manual: Introduction.

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

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

Be sure to include the appropriate headers.

In standard C, function definitions can occur only in file scope. In CIVL-C, they can occur in any scope.

$input decl

Declares a variable in file scope to be an input variable. An input variable X is initialized according to the following protocol: (1) if a value for X is specified on the command line via -inputX=val, then val is the initial value; (2) otherwise, if an initializer is present in the declaration, the initializer is used; (3) otherwise, X is assigned an unconstrained value of its type---when using symbolic execution, it is assigned a fresh symbolic constant.

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

$assume(expr)

Assumes this expression is true, i.e., if the expression is not true, the the execution is not considered to be a valid execution of the program.

$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

int $choose_int(int n)

Returns an integer nondeterministically chosen from 0..n-1.

$choose { stmt1 stmt2 ... }

Structural nondeterminism. Chooses one of the enabled statements nondeterministically. The statements are often guarded using $when.

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. Note that MPI_Send may be forced to synchronize --- i.e., it can block until the receiving process reaches a matching receive statement.

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

A two-thread barrier using semaphores in CIVL-C

#include <stdio.h>

int s1=0, s2=0;
#define sem_wait(s) $when (s>0) s--;
#define sem_post(s) s++;
const int N=10;
int i1=0, i2=0;

void f1() {
  while (i1<N) {
    printf("thread 1 at iteration %d\n", i1);
    fflush(stdout);
    i1++;
    sem_post(s1);
    sem_wait(s2);
    $assert(i1==i2);
    sem_post(s1);
    sem_wait(s2);
  }
}

void f2() {
  while (i2<N) {
    printf("thread 2 at iteration %d\n", i2);
    fflush(stdout);
    i2++;
    sem_post(s2);
    sem_wait(s1);
    $assert(i1==i2);
    sem_post(s2);
    sem_wait(s1);
  }
}

int main() {
  $proc t1 = $spawn f1(), t2 = $spawn f2();
  $wait(t1);
  $wait(t2);
}