
This is Example 2.18 from "MPI: The Complete Reference, vol. 1," 2nd
edition.  It consists of a several producers and a single consumer.

Four properties are checked:

p0. Freedom from Deadlock and standard assertions

p1. Every message produced is eventually consumed.

p2. No producer becomes permanently blocked.

p3. For a fixed producer, the messages are consumed in the order in which they are produced.

