Fischer's Mutual Exclusion Protocol
Author: Bruno Dutertre
Date: September 25, 2003
-----------------------------------
Description
-----------
The protocol ensures mutual exclusion among N processes
using real-time clocks and a shared variable 'lock'.
Initially lock is 0.
Every process is as follows:
loop
wait until lock = 0;
wait for a delay <= delta1;
set lock to process id;
wait for a delay >= delta2;
if lock = process id
enter critical section
end
The parameters delta1 and delta2 are two positive
constants that determine the length of the delays.
Mutual exclusion is ensured provided delta1 < delta2.
SAL Encoding
------------
The SAL model differs from timed automata in that it does not use
clocks. Instead, a global variable 'time' keeps the current time and a
variable 'time_out[i]' contains the time when the next discrete
transition of process i is scheduled to occur.
There are two types of transition:
- if time < time_out[i] for all i, then time is advanced
to the smallest of time_out[1],...,time_out[N] (time-progress
transition)
- otherwise, a process i for which time_out[i] = time
performs a discrete transition. This transition updates
time_out[i] to a new value strictly larger than the current
time. Timing constraints are encoded into the update of
time_out[i].
Example verifications
---------------------
- If delta2 <= delta1, find a counterexample to mutual exclusion:
sal-inf-bmc -v 10 fischer mutual_exclusion
There is a counterexample at depth 10 if delta2 <= delta1.
- If delta1 < delta2, prove mutual exclusion by induction
1) auxiliary invariants:
sal-inf-bmc -v 10 -i -d 1 fischer time_aux1
sal-inf-bmc -v 10 -i -d 1 fischer time_aux2
2) time_aux3 follows from time_aux2
sal-inf-bmc -v 10 -i -d 1 -l time_aux2 fischer time_aux3
3) logical_aux1 from time_aux1 and time_aux3
sal-inf-bmc -v 10 -i -d 1 -l time_aux3 -l time_aux1 fischer logical_aux1
4) logical_aux1 implies mutual exclusion
sal-inf-bmc -v 10 -i -d 0 -l logical_aux1 fischer mutual_exclusion
- Variant proofs for N=2 (the induction depth increases with N)
using time_aux2 as a lemma:
sal-inf-bmc -v 10 -d 3 -l time_aux2 fischer logical_aux1
sal-inf-bmc -v 10 -d 0 -l logical_aux1 fischer mutual_exclusion
sal-inf-bmc -v 10 -d 5 -l time_aux2 fischer mutex
sal-inf-bmc -v 10 -d 0 -l mutex fischer mutual_exclusion
sal-inf-bmc -v 10 -d 9 -l time_aux2 fischer mutual_exclusion