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