Information Technology Reference
In-Depth Information
implements a timeout which guarantees that the process either stays in state
B
at most one time unit, or gets stuck in
B
forever. When moving from
B
to
C
,
the process sets the value of the shared variable to its own index
i
and again
resets its clock. From state
, the process can proceed to the critical section if
the clock is strictly more than 1 and if the value of the shared variable is still
i
C
C
the clock enforces a delay which
is longer than the length of the timeout in state
, the index of the process. Thus, in state
B
. Finally, when exiting the
critical section, the process resets the shared variable to
?
. Processes that get
stuck in state
. Since we do
not intend to model liveness properties, such as e.g., absence of starvation, we
do not impose requirements that force processes to change their state
1
.
C
can reenter the protocol by returning to state
A
A rough argument for the correctness of the protocol goes as follows. The con-
ditions on the shared variable ensure that a process cannot reach
B
if any other
processisin
C
or
CS
. The timing conditions on the clocks ensure that a process
cannot move from
.Thus,ifaset
of processes start the mutual exclusion protocol and all arrive in
C
to
CS
if some other process is still in
B
C
, then the
process which was the last to enter
C
will read its own identity in the shared
variable and enter the critical section.
Verication by Backwards Reachability Analysis
If we perform a backwards
reachability analysis for Fischer's protocol, starting from negation of the in-
variant being equivalent to
9i; j:CS
[
i
]
^ CS
[
j
]
then we end up with convergence and the following xedpoint
9i; j: CS
[
i
]
^ CS
[
j
]
_9i; j: C
[
i
]
^ v
=
i ^ CS
[
j
]
_9i; j: B
[
i
]
^ x
[
i
]
<
1
^ CS
[
j
]
_9i; j: B
[
i
]
^ x
[
i
]
<
1
^ C
[
j
]
^ v
=
j ^ x
[
i
]
<x
[
j
]
_9i; j: A
[
i
]
^ v
=0
^ CS
[
j
]
_9i; j: C
i
^ v
^ CS
j
[
]
=0
[
]
The negation of this assertion is a universal invariant, which can be written as
follows.
8i; j: :
(
CS
[
i
]
^ CS
[
j
])
^8i; j:
(
C
[
i
]
^ CS
[
j
]) =
) v 6
=
i
^8i; j:
(
B
[
i
]
^ CS
[
j
]) =
) x
[
i
]
1
^8i; j:
B
i
^ C
j
)
x
i
_ v 6
j _ x
i
x
j
(
[
]
[
]) =
(
[
]
1
=
[
]
[
])
^ i:
A
i
^ CS
i
)v6
(
[
]
[
]=
=0
^ i:
C
i
^ CS
i
)v6
=0
1
In fact, our formalism cannot express such requirements, although they can be added
in terms of e.g., fairness constraints.
(
[
]
[
]=
Search WWH ::
Custom Search