This is example 2.19 from "MPI: The Complete Reference, vol 1," 2nd
edition.  It modifies ex. 2.18 by replacing the round robin waits with
a busy wait loop that repeatedly tests for the completion of the
receive requests.  Notice there is a bug in the code as written
concerning the value of i upon exiting the loop.

The bug was actually caught by SPIN in checking p0: the number of
request can exceed the specified bound.  (There are other ways the bug
could have been revealed.)  This is demonstrated by the make target
mpsc_org_p0_0.   The resulting trail is written to trail.txt.

I corrected the program according to what seemed to me to be
the authors' intention.

After making the correction, we can verify the properties. 

Note that to verify p1, one of the MPI "progress" assumptions has to
be used---this is done by incorporating it into the property.  The
progress assumption is basically that you cannot have a receive
delayed forever....see the file mpi-nonblocking.c, function
MPI_delayedRecv for precise details.

An even stronger assumption is needed to verify p2: in addition to the
MPI progress assumption, we must assume weak fairness.  Otherwise, the
consumer can spin forever in the busy test loop, while the producer is
capable of sending a message but doesn't.


