Go backward to
The Formula
Psi
Go up to
Top
Go forward to
The Fairness Requirement
The Next-State Relation
alpha
1
step:
Starts in state with
pc
1
= "a" (first process is at control point
alpha
1
) and 0
<
sem
(no process in critical section).
Ends in staet with
pc
1
= "b" (first process is at control point
beta
1
).
Decrements
sem
and does not change
x
,
y
,
pc
2
.
A
1
step:
alpha
1
step or
beta
1
step or
gamma
1
step.
Execution of atomic operation by first process.
A
step:
Step of either process.
The program's next-state relation.
Author:
Wolfgang Schreiner
Last Modification: May 14, 1998