User Tools

Site Tools


projects:yieldtraces

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
projects:yieldtraces [2010/04/15 14:48]
jaeheon
projects:yieldtraces [2010/04/15 15:27] (current)
jaeheon
Line 1: Line 1:
-=== Examples of some traces for yield and determinism ​===+=== Examples of some tricky ​traces for Cooperability Checking ​===
  
-  ​- 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. <​code>​+==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. 
 +<​code>​ 
 +t0       t1 
 +fork t1 
 +wr x 
 +stop 
 +          wr x 
 +</​code>​ 
 + 
 +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. <​code>​
 t         ​u ​        v t         ​u ​        v
 beg A beg A
projects/yieldtraces.txt · Last modified: 2010/04/15 15:27 by jaeheon