VVS Exercise: model checking

Producers and consumers

Introduction

In this exercise we will play with a classical example of concurrency problem: producers and consumers. We have two kind of processes:

  • producer: it executes an infinite loop producing items and writing them into a buffer

    while true begin
      <produce new item>
          <write into buffer> // critical section
    end     
  • consumer: it is another infinite loop that extracts items from the buffer and processes (or consumes) them

    while true begin
      <extract item from buffer> // critical section
      <consume item>
     end

We will try the example with several values for P=0,1,2 producers and C=0,1,2 consumers. The buffer has a limited size of N>0 items. Typically, the buffer is handled as a circular FIFO. In our case, however, we will not represent the buffer itself, as we are not interested in simulation, but only on the correctness of the concurrent protocol itself. The code for writing an item in the buffer can be just a simple printf representing that situation, and the same happens for extracting an item from the buffer. The same happens for producing or consuming items: they can be represented as printf's.

Goals

The goal of this exercise is playing with the example in SPIN and verifying three main conditions:
  1. absence of deadlock: we cannot reach a state in which all processes get blocked waiting for something to happen.
  2. mutual exclusion: there cannot be two processes trying to access their critical sections "simultaneously", that is, they cannot both point to their corresponding buffer access as the next executable instruction.
  3. absence of starvation (liveness): we want to check that no producer or consumer will starve. That is, any producer should be able to produce infinite items and any consumer should be able to consume infinite items. Note that if either P=0 or C=0 this may not hold.

Note also that absence of deadlock does not imply absence of starvation: perhaps one producer and one consumer work all the time, while others get waiting forever. We will use the classical solution with two general semaphores: items (counting the items in the buffer) and holes (counting the remaining holes in the buffer) plus a binary semaphor mutex for accessing the critical section. The pseudocodes for producers and consumers would look like:

// Producer

while true begin
  <produce new item>;
  p(holes);
  p(mutex);
  <write into buffer> // critical section
  v(mutex);
  v(items)
end

// Consumer

while true begin
  p(items);
  p(mutex);
  <extract from buffer> // critical section
  v(mutex);
  v(holes);
  <consume item>
end

What to do

You have to elaborate the following experiments.

  1. Write the Promela code (prodcom.pml) corresponding to the pseudocode above.
  2. For each combination of values for P and C, check the three conditions (no deadlock, mutual exclusion, no starvation).
  3. In the case of mutual exclusion, check what happens if we remove the mutex sempahore.

Assessment & delivery

The maximum grade for this exercise is 1,3 points. The deadline for delivery is Thursday,  May 19th,  2016. To submit your work, send me an e-mail with a pair of attachments: the promela source code prodcom.pml plus a summary (a PDF file) explaining the obtained results for each algorithm.

Warning: do not attach compressed files (zip, gz, tar, ...). The UDC anti-spam filter will delete them.
Maintained by Pedro Cabalar. Last update May 9th, 2016