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”.
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