Formal modeling and verification of Peterson's algorithm

We have studied different (incorrect) algorithms for mutual exclusion in a distributed setting. Our goal is to model and verify a generalized version of Peterson’s algorithm for any number of processes.

Part 1

Modelling Peterson’a algorithm

We consider a more general version of Peterson’s algorithm defined for process i below.

do forever {
  for l := 1 to N-1 {
    level[i] := l;
    turn[l] := i;
    wait until (turn[l] != i) or (forall j != i, level[j] < l);
  }
  // in critical section
  level[i] := 0
}

The algorithm uses two shared arrays:

  • level indexed from 1 to N which is initialized to 0,
  • and turn indexed from 1 to N-1 and initialized to 0.

In the first phase (the for loop), the process goes through N-1 levels.

  • The value of level[i] is the current level of process i, or 0 if process i does not request access to the critical section.
  • The value of turn[l] is the identifier of the last process that has reached level l (or 0 if no process has reached l so far).

When a process enters level l, it is blocked until either another process enters level l, or all the other processes are at lower levels (wait instruction in the algorithm above). Hence, one process among all those at level l is blocked there, whereas all the other processes at level l move up. As a result, there is at most one process that exits each level. In particular, at most one process can exit level N-1 and enter the critical section. Therefore, the turn variables ensure mutual exclusion.

The level variables are used to ensure progress. The process at the highest level can go to the next level (or enter the critical section) even if it is the last process at this level. Observe that this is crucial to ensure progress if less that N processes actually try to enter the critical section.

  1. Write a PlusCal model of this algorithm where each line is modelled as an atomic instruction.
  2. Check that your model satisfies the invariant Mutex as well as absence of deadlocks

Ensuring progress

  1. Explain why an algorithm that has no deadlock, and that satisfies the invariant Mutex, may not provide a satisfying solution to the mutual exclusion problem.
  2. Update the specification accordingly and model-check all three properties, adding (* PlusCal options (-sf) *).

Part 2

In the description of Peterson’s algorithm above, the wait instruction accesses several shared variables atomically.

  1. Explain why this is not realistic w.r.t. implementation of shared variables in standard programming languages (C, C++, Java, etc)
  2. Update your model to implement the wait statement as a non-atomic instruction.
  3. Check that your model satisfies the invariant Mutex as well as absence of deadlocks
  4. Check that your model ensures progress under (* PlusCal options (-sf) *).