Examples of some tricky traces for Cooperability Checking
Yield-free and cooperable trace does not imply determinism
We previously conjectured that any yield-free cooperable trace is deterministic.
The following trace is cooperative, and hence cooperable. It is also yield-free. However, it is not deterministic, since there are alternative, non-cooperable traces that are not equivalent, and so this example refutes this conjecture.
t0 t1
fork t1
wr x
stop
wr x
New conjecture: if all possible traces of a program are yield-free and cooperable, then the program is deterministic.
This conjecture suggests that there may be interesting opportunities in “cooperability prediction”.
A join does not record all expected interference
We run into some difficulty with the following property: “If A and B are adjacent epochs by thread t and B starts with join(t,u) then for all epochs C with A → C and tid(C) != u, we also have that B → C.” We might call it the “join's expected interference” property. The following trace has epoch E which does not follow this property: Epoch E is epoch-after epoch A (due to fork edges) and tid(E) != u, but we do not have B → E.
t u v
beg A
fork u
end A
beg C
fork v
end C
beg E
…
end E
beg D
join u,v
end D
beg B
join t,u
end B
