Information Technology Reference
In-Depth Information
v6
=
i
fg
true
true
fx
[
i
]
g
x
[
i
]
<
1
fx
[
i
]
g
x
[
i
]
>
1
fg
A
[
i
]
B
[
i
]
C
[
i
]
CS
[
i
]
v
=0
v
:=
i
v
=
i
fg
true
v
:= 0
Fig. 1. Fischer's Protocol for Mutual Exclusion.
Example In the example of the mutual exclusion algorithm, the three states of
the network invariant correspond to the following partitioning of the states.
left state : 0 occurrences of both t and c
middle state : 1 occurrence of t and 0 of c
right state :
0 occurrences of t and 1 of c
5
Application: Fischer's Protocol
In this section, we will illustrate the results of the preceding section by verifying
a parameterized version of Fischer's protocol.
The protocol has been used as a measure of the performance of tools for verica-
tion of timed automata. The example was suggested by Fred Schneider and has
been veried manually (e.g., [AL92]) and using theorem provers (e.g., [Sha93]).
Several tools for verifying automata with a xed number of clocks have been
used to verify it for an increasing number of processes (e.g., [ACHH92]). Kristof-
fersen et al. [KLL + 97] describes an experiment where the number of processes
is 50.
The purpose of the protocol is to guarantee mutual exclusion in a concurrent
system consisting of an arbitrary number of processes, using clocks and a shared
variable. Each process has a local clock, and runs a protocol before entering
the critical section. Each process has a local control state, which in our model
assumes values in the set
CS
represents the critical section. The processes also read from and write to a shared
variable whose value is either
fA; B; C; CSg
where
A
is the initial state and
or the index of one of the processes. A description
in a graphical pseudo-code (taken from [KLL + 97]) of the behavior of a process
with index
?
i
is given in Figure 1.
Intuitively, the protocol behaves as follows: A process wishing to enter the critical
section starts in state
A
. If the value of the shared variable is
?
, the process
can proceed to state
B
and reset its local clock. From state
B
, the process can
proceed to state
C
if the clock value is still less than 1. In other words, the clock
Search WWH ::




Custom Search