The producer-consumer problem is a classic software concurrency problem. The problem features one or more "producers" and one or more "consumers". All producers and consumers must share access to a "buffer" into which producers insert the products they produce, and from which consumers take the products they consume. The shared buffer is "bounded", that is, it has a maximum capacity.
So at any time, the buffer could be empty, precluding any consumer from withdrawing a product. Or the buffer could be full, which would mean that no producer could produce a new product until a consumer had first consumed a product, making space in the buffer. To avoid concurrency related problems, producers and consumers can access the buffer only at times when no other producer or consumer is accessing it, and only when it is in the proper state for the particular type requesting access (i. e., not empty for consumers and not full for producers).
The root class of the example creates the bounded product buffer and a number of producers and consumers, all given
separate types. It requests the producers to create a number of products, and the consumers, in the aggregate, to consume that same number of products.
Separate argument rule
Notice that the root class uses a feature
launch_producer (and a corresponding feature
launch_consumer) for instructing the producers and consumers on how many products to handle.
launch_producer looks like this:
launch_producer (a_producer: separate PRODUCER)
-- Launch `a_producer'.
It might occur to you that it would be easier, simpler, and clearer just to include this feature's single procedural line:
in place of the call to
launch_producer, and dispense with the
launch_producer feature entirely. But that is not possible in this case.
The reason is that
a_producer.produce (900) is a separate call (i. e., the object attached to
a_producer is declared of a separate type), and according to the separate argument rule, calls on a separate object are valid only when applied to an argument of the enclosing routine.
This example also shows an uncontrolled precondition serving as a "wait condition". In the class
PRODUCER we see the buffer declared as a class attribute with a
buffer: separate BOUNDED_BUFFER [INTEGER]
-- Shared product buffer.
store contains a precondition which ensures that the shared buffer is not full when
store gets applied:
store (a_buffer: separate BOUNDED_BUFFER [INTEGER]; an_element: INTEGER)
-- Store `an_element' into `a_buffer'.
a_buffer.count = old a_buffer.count + 1
store routine is called by the routine
produce, passing a reference to the
buffer like this:
store (buffer, l_element)
buffer is considered uncontrolled in the context of
produce, then the precondition for
store becomes a wait condition, rather than a correctness condition. This means that if the buffer is full, then the application of the feature
store will wait until some consumer removes an product from the buffer. The removal of a product makes the precondition hold again, and the application of
store can proceed.