VV: Exercise 1, model checking

Readers and Writers

Introduction

In this exercise we will play with a classical example of concurrency problem: readers and writers. We have some shared resource containing information (a table in a database, a buffer, a cache memory, OS file metadata, etc) and two kinds of processes that can handle the resource as follows:

  • writer: makes changes (additions or updates) in the information contained in the shared resource.

  • reader: may query the shared resource but makes no changes on it. It executes an infinite loop.

We assume that each writer may update the resource an infinite number of times and, similarly, each reader may query the reource infinitely often. We will try the example with several values for W>=0 writers R>=0 readers. To guarantee coherence in the stored information, when one writer is writing (critical section) no other process can be handling the resource at the same time. However, several readers can be reading simultaneously (provided that no writer is working on the resource).

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" being at least one of them a writer.
  3. absence of starvation (liveness): check whether writers or readers may starve. In principle, any process should be able to work infinitely often. However, depending on the solutions we study, this condition may fail for readers, for writers or for both.

Note also that absence of deadlock does not imply absence of starvation: perhaps one writer works all the time but readers do not work, or perhaps readers starve the writer, etc.

The three conditions mentioned above will be checked on two solutions: readers-priority and writers-priority.

Algorithm 1 (readers-priority)

The first solution gives priority to reader processes. To this aim, we handle a binary semaphore can_write that controls that only one writer can write in the resource at a given time. If several readers are ready at a time, the first reader will lock that semaphore and the last reader will unlock it. To know if a reader is the first or the last one, we handle an additional shared variable readers counting the number of readers currently working on the resource. This variable is controlled by a binary semaphore rmutex. The pseudocodes for readers and writers are given below:

// Writer

while true begin
  // ready to write
  p(can_write);
  <write into resource> // critical section
  v(can_write);
end

// Consumer

while true begin
  // ready to read
  p(rmutex);
  readers++;
  if readers==1 then p(can_write); // first reader locks writers
  v(rmutex);

  <read from resource> // critical section

  p(rmutex);
  readers--;
  if readers==0 then v(can_write); // last reader unlocks writers
  v(rmutex);
 end

OPTIONAL: in this solution, try to check that we keep priority for readers, that is, that a writer will never write if a reader is ready to read.

Algorithm 2 (writers-priority)

In the second algorithm, we will try to give priority to writers. To this aim, we add a new mutex can_read that will block the readers when writers are working. As before, the first writer will lock that semaphore and the last writer will unlock it. We handle a counter of  writers and a new mutex wmutex to control this new counter.

// Writer

while true begin
  // ready to write
  p(wmutex);
  writers++;
  if writers==1 then p(can_read); // first writer locks readers
  v(wmutex);

  p(can_write);
  <write into resource> // critical section
  v(can_write);

  p(wmutex);
  writers--;
  if writers==0 then v(can_read); // last writer unlocks readers
  v(wmutex)
end

// Consumer

while true begin
  // ready to read
  p(can_read);
  p(rmutex);
  readers++;
  if readers==1 then p(can_write); // first reader locks writers
  v(rmutex);
  v(can_read);

  <read from resource> // critical section

  p(rmutex);
  readers--;
  if readers==0 then v(can_write); // last reader unlocks writers
  v(rmutex);
 end

This solution is still incorrect: when the writer tries to lock can_read it may compete with N readers and has no priority on them. To mitigate this problem, we can use an additional binary semaphore only_one that protects all the block code in the reader between p(can_read) and v(can_read). In this way, only one reader at each moment will be able to check the can_read semaphore.

Assessment & delivery

The maximum grade for this exercise is 1,3 points. The deadline for delivery is Friday,  May 8th,  2015, Friday,  May 15th,  2015. Exercises must be sent as a zipped file to my email address pedro%dot%cabalar%at%udc%dot%es.


Maintained by Pedro Cabalar. Last update May 7th, 2015