projects:yieldtraces

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

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