User Tools

Site Tools


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
          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
projects/yieldtraces.txt · Last modified: 2010/04/15 15:27 by jaeheon