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’s algorithm

We consider a more general version of Peterson’s algorithm that is expected to be correct for N processes. The pseudo-code is shown 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 (cf. 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. Thus the role of the variable turn is to 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. Translate the pseudo-code above into a PlusCal model 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 properties, adding (* PlusCal options (-sf) *) before the definition of your PlusCal algorithm.

Part 2

In the pseudo-code of Peterson’s algorithm above, the wait instruction accesses several shared variables in a single atomic instruction.

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