Proof Outline of Copy Problem
From Foundations of Multithreaded, Parallel, and
Distributed Programming
By Greg Andrews, 2000, Chapt. 2
Global Invariant:
PC: c <= p <= c+1 and
a[0:n-1] == A[0:n-1]
and
(p == c+1)
=> (buf == A[p-1]),
where, A[i] are logical values
Copy Problem with Assertions:
int, buf, p = 0, c = 0
{PC}
process Producer{
int
a[n]; all a[i] are initialized to A[i]
{IP: PC and p<=n}
while (p<n) {
{PC and p<n}
<await (p==c);> delay until buf
empty
{PC and p<n and p == c}
buf
= a[p];
{PC and p<n and p==c and buf == A[p]}
p = p+1;
{IP}
}
{PC and p == n}
}
process Consumer{
int
b[n];
{IC: PC and c<=n and b[0:c-1]
== A[0:c-1]}
while (c < n){
{IC and c <n}
<await(p>
c); >
{IC and c < n and p>c}
b[c] = buf;
{IC and c<n and p>c and b[c] == A[c]}
c = c+1;
{IC}
}
{PC and c==n}
}
Final Program State Satisfies:
PC ^ p==n ^ IC ^ c == n