data buffer
process producer process consumer
while true while true
buffer = p() c(buffer)
p() is consumed by c().
Inv: dseq_p = dseq_c ordseq_p = dseq_c + buffer
dseq_p = dseq_c = empty.
producer can overwrite data in the buffer.
consumer can re-read old data in the buffer.
buffer is either ready to read (full) or ready to write
(empty).
data buffer
bool empty = true
process producer process consumer
while true while true
while !empty skip while empty skip
{ empty } { !empty }
buffer = p() c(buffer)
empty = false; empty = true
p() and c()
statements see to that.
while empty skip
{ !empty }
c(buffer)
await B blocks the executing thread until B is
true.
B eventually be true.
await and Atomicityawait B ; S , B may be interfered with after falling
out of await B.
B must reference at least one write-set variable.
{ P and B } S { Q }
holds, then the Await Rule lets us conclude that the triple
{ P } < await B ; S > { Q }
holds too.
{ P and B } can't be interfered with in< await B { P and B } S >.
{ P } can be interfered with, though.
< await B ; S > is not executed until B is true.
{ Pi } Si { Qi } hold for 1
<= i <= n and are interference free then the
co Statement Rule
{ P1 and P2 and ... and Pn }
co S1 || S2 || ... || Sn oc
{ Q1 and Q2 and ... and Qn }
holds too.
Si in the co statement.
and elimination to get back the
original precondition.
co x = x + 1 || x = x + 1 oc
is equivalent to
co < x = x + 1 > || < x = x + 1 > oc
and the latter co statement has only two equivalent sequential executions:
x1 = x1 + 1 ; x2 = x2 + 1 or
x2 = x2 + 1 ; x1 = x1 + 1
| C++ | x86 assembly | pseudo-code |
| x = x + 1 | movl %esp, %ebp subl $4, %esp leal -4(%ebp), %eax incl (%eax) |
move r0 x add r0 1 move x r0 |
co x = x + 1 || x = x + 1 oc
has (2*4)!/4!2 = 40320/576 = 70 possible sequential executions.
move r1 x move r2 x add r1 1 add r2 1 move x r1 move x r2 |
This is assembly language sequence equivalent to executing
x = x + 1
|
<> around each statement isn't a good
idea.
S appears to be atomic if it accesses only read-set
shared variables.
S executes.
co x = y + 1 || y = z + 1 oc .
x = y + 1 either reads the old or new value of y.
co x = y + 1 || y = z + 1 oc
is equivalent to executing
co < x = y + 1 > || < y = z + 1 > oc
co x = y + y || y = z + 1 oc .
x = y + y has two critical references.
x = y + y can read both the old and new values of y.
co x = x + 1 || x = x + 1 oc ?
x = x + 1 has one critical reference to x, but it also modifies
the read-set variable x.
S obeys the
At-Most-Once property if
S contains at most one critical reference and doesn't modify a
read-set shared variable, or
S contains no critical references.
In the second case, S may write a read-set variable.
| C++ code | Sparc assembly |
|---|---|
std::pair<int, int> i, j; i = j; |
ld [%fp-32], %o0 st %o0, [%fp-24] ld [%fp-28], %o0 st %o0, [%fp-20] |
co buffer = p() || c(buffer) oc
may not be equivalent to either of the sequential executions
buffer = p() ; c(buffer)
or
c(buffer) ; buffer = p()
This page last modified on 12 June 2003.