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:

Back to TReX's Home Page