bool cs_occupied = false
// entry protocol
{ true }
while (cs_occupied) skip
{ !cs_occupied }
cs_occupied = true
{ cs_occupied }
// critical section
// exit protocol
{ cs_occupied }
cs_occupied = false
{ !cs_occupied }
cs_occupied = true in computation j interferes with the
entry-protocol predicate { !cs_occupied } in computation i.
{ !cs_occupied } can't get any weaker.
cs_occupied must be read and
written at the same time.
cs_occupied.
// entry protocol
{ true }
< while (cs_occupied) skip
{ cs_occupied }
cs_occupied = true
>
{ cs_occupied }
< while (cs_occupied) skip ; cs_occupied = true >
bool test_and_set(bool & b)
< bool t = b;
b = true;
return t;
>
{ true }
while test_and_set(cs_occupied) skip
{ cs_occupied }
bool in1 = false, in2 = false
// entry protocol
while in2 skip while in1 skip
{ not in1 and not in2 } { not in1 and not in2 }
in1 = true in2 = true
{ in1 and not in2 } { not in1 and in2 }
// exit protocol
in1 = false in2 = false
bool in1 = false, in2 = false
// entry protocol
in1 = true in2 = true
while in2 skip while in1 skip
{ in1 and not in2 } { not in1 and in2 }
bool in1 = false, in2 = false int winner; // entry protocol in1 = true in2 = true winner = 2 winner = 1 while in2 and winner == 2 while in1 and winner == 1 // exit protocol in1 = false in2 = false
winner ensures mutual exclusion.
1 or 2 when in1 and in2 is true.
winner can only be 1 or 2.
in[j] fails immediately for computation i.
n-computation turn-taking requires O(n2) work.
## in_cs(i) imp tickets[i] = current ## forall i, j : 0 < i < j <= n ## : tickets[i] != tickets[j] int ticket = 1 int current = ticket int tickets[1:n] = (-1, -2, ..., -n) // entry protocol < tickets[i] = ticket ; ticket = ticket + 1 > < await tickets[i] == current > // exit protocol < current = current + 1 >
in_cs(i) imp tickets[i] = current
forall i,j : 0 < i < j <= n : tickets[i] != tickets[j]
< tickets[i] = ticket ; ticket++ > preserves uniqueness.
< await tickets[i] == current > preserves ticket entry.
< await tickets[i] == current > obeys the At-Most-Once property
and is effectively atomic.
while (tickets[i] != current) skip)
< current = current + 1 > doesn't obey the At-Most-Once property, but is
effectively atomic anyway.
< tickets[i] = ticket ; ticket++ > is a problem.
n computations, each having a ticket in int
tickets[1:n].
0.
i computes its ticket value as
tickets[i] = (max i : 1 <= i <= n : tickets[i]) + 1
## in_cs(i) imp
## tickets[i] > 0 and
## forall j : 1 <= j <= n and i != j
## : (tickets[j] = 0) or
## (tickets[i] < tickets[j])
int tickets[1:n] = ([n] 0)
// entry protocol
< tickets[i] =
(max i : 1 <= i <= n : tickets[i]) + 1
>
for [j = 1 to n st j != i]
< await (tickets[j] == 0) or
(tickets[i] < tickets[j])
>
// exit protocol
tickets[i] = 0
< tickets[i] =
(max i : 1 <= i <= n : tickets[i]) + 1
>
is too complicated for hardware atomicty, and too slow for software atomicty.
(tickets[j] == 0) or (tickets[i] < tickets[j])
doesn't obey the At-Most-Once property.
for [ j = 1 to n st j != i ] < await turn[j] == 0 or (turn[i] < turn[j]) or (turn[i] == turn[j] and i < j) >
tickets[j] = (max k : 1 <= k <= n : tickets[k]) + 1
interfere with the await guard?
tickets[j] = 0 interfere with the await guard?
// C++ class critical_section virtual void enter(unsigned tid) = 0 virtual void exit(unsigned tid) = 0 // Java interface CriticalSection void enter(int tid) void exit(int tid)
// C++
void f(critical_section & cs)
cs.enter(tid)
// whatever
cs.exit(tid)
|
// Java
void f(CriticalSection cs)
cs.enter(tid)
// whatever
cs.exit(tid)
|
& for C++; it's important.
class two_way_tie_breaker
: critical_section
two_way_tie_breaker()
in[0] = in[1] = false;
void entry(unsigned me)
assert (me == 0) or (me == 1)
assert !in[me]
const unsigned other = (me + 1) % 2
in[me] = true ; winner = other
while (in[other] and winner == other) ;
void exit(unsigned me)
assert (me == 0) or (me == 1)
assert in[me]
in[me] = false
bool in[2]
int winner
This page last modified on 25 June 2003.