(Bi-)simulation quotienting and model-checking

This chapter is inspired from example 7.13 in "Principles of Model-Checking" by Joost-Pieter Katoen and Christel Baier.

A simplified Bakery algorithm

We consider the simplified version of Lamport's Bakery algorithm for 2 processes described below.

while (TRUE) {                               while (TRUE) {
n1:  x1 := x2 + 1;                           n2:  x2 := x1 + 1;
w1:  wait until(x2 = 0 || x1 < x2);          w2:  wait until(x1 = 0 || x2 < x1);
c1:  ... critical section ...                c2:  ... critical section ...
r1:  x1 := 0;                                r2:  x2 := 0;
}                                            }
  

This algorithm has an infinite state space and cannot be model-checked as is. Our goal is to define a finite bisimulation relation over the states of this algorithm. The resulting quotient transition system is finite and can be used to prove the correctness of this (simplified) Bakery algorithm.

We see from the algorthm above that the actual values of x1 and x2 are irrelevant. We only need to know if they are 0 or not. And, if both are non zero, we also need to know whether x1 < x2 or x2 < x1 (observe that in this simplified algorithm, two processes cannot have the same access number). Hence, we propose the following relation over the states of the algorithm.

(l1,l2,v1,v2) R (l1',l2',v1',v2') if:

  1. Prove that R is a bisimulation relation over the states of the algorithm above
  2. What is a state in the quotient of this algorithm by R?
  3. Represent the quotient of the algorithm by R
  4. Write a PlusCal model corresponding to the quotient of the algorithm by R.
  5. Check that your PlusCal model satisfies: mutual exclusion, absence of deadlock and absence of starvation. What can you deduce for the (simplified) Bakery algorithm?

Lamport's Bakery algorithm

We consider Lamport's Bakery algorithm as described in Formal design of a distributed mutual exclusion algorithm.

  1. Define a bisimulation relation R over the states of the algorithm.
  2. What is a state in the quotient of the algorithm by R?
  3. How can you represent a state in the quotient in PlusCal?
  4. Write a PlusCal model for the quotient of the algorithm by R
  5. Check that your PlusCal model satisfies: mutual exclusion, absence of deadlock and absence of starvation. What can you deduce for Lamport's Bakery algorithm?