TReX's Examples
Fischer's Algorithm
Description of the example
Fischer's algorithm is a timed mutual exclusion algorithm.
It allows n timed processes (identical up to renaming) to access in
mutual exclusion a shared ressource.
The algorithm uses a shared variable id ranging from 0 to n
saying which process (indexed from 1 to n) requested access to the shared
ressource. If id is 0, it means that no process wants this ressource.
When a process i wants the shared ressource,
it tests the shared variable id.
If id= 0, in the next D time units it
sets id to its identifier, i.e., i. Then, it waits at least
T time units before testing again id.
If id is not equal to its identifier i (meaning that
another process has requested access) then process i retries
later. Otherwise, it enters in the critical section.
The algorithm is parameterized by the two real parameters
D and T corresponding to
the waiting times.
The following figure represents the timed automaton for process i.
Each process has its own clock xi to model the waiting intervals.
Experimental results
TReX allows us to obtain two kind of results:
-
Generate automatically the constraint between the parameters
D and T
such that the algorithm satisfies the mutual exclusion (safety) property.
For this, we compute with TReX the reachable configurations set
and the symbolic graph of the system with
2 (fischer_22.scf,
fischer_22.aut) and
3 processes
when the initial constraint on parameters is the most general one
D > 0 and T > 0.
We obtain that the state cs1 cs2 is reached (so the mutual exclusion
property is not verified) when T < D.
We infer that the necessary constraint on parameters to obtain mutual
exclusion is : T >= D.
-
Verify the constraint obtained above as being sufficient.
For this, we compute with TReX the reachable configurations set when
the initial constraint on parameters is T >= D.
The results obtained for the system with
2 (fischer_21.scf,
fischer_21.aut) and
3 (fischer_31.scf,
fischer_31.aut) processes,
show that the mutual exclusion property is satisfied (states of the form
csi * csj are not reached).
Back to TReX's Home Page