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