Producer-consumer

Description

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

Highlights

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'. do a_producer.produce (900) end

It might occur to you that it would be easier, simpler, and clearer just to include this feature's single procedural line:

a_producer.produce (900)

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.

Wait condition

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 separate type:

buffer: separate BOUNDED_BUFFER [INTEGER] -- Shared product buffer.

The feature 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'. require not a_buffer.is_full do a_buffer.put (an_element) ensure not a_buffer.is_empty a_buffer.count = old a_buffer.count + 1 end

The store routine is called by the routine produce, passing a reference to the separate attribute buffer like this:

store (buffer, l_element)

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