Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav07_lecture_26 [2007/07/03 00:06] feride.cetin |
sav07_lecture_26 [2007/07/03 01:11] (current) feride.cetin |
||
---|---|---|---|
Line 169: | Line 169: | ||
- s<sub>i</sub> is a program state | - s<sub>i</sub> is a program state | ||
- α<sub>i</sub> is one of the following actions: acq(), rel (), read(), write(), fork (), join(), and alloc() | - α<sub>i</sub> is one of the following actions: acq(), rel (), read(), write(), fork (), join(), and alloc() | ||
+ | |||
+ | The happens-before relation hb for δ is the smallest transitively-closed relation on the set {1,2,...,n} such that for any k and l, we have k hb l if 1 < = k < = l < = n and one of the following holds: | ||
+ | - t<sub>k</sub> = t<sub>l</sub> | ||
+ | - α<sub>k</sub> = rel(o) and α<sub>l</sub> = acq(o) | ||
+ | - α<sub>k</sub> = write(o) and α<sub>l</sub> = read(o) | ||
+ | - α<sub>k</sub> = fork(t<sub>l</sub>) | ||
+ | - α<sub>l</sub> = join(t<sub>k</sub>) | ||
+ | |||
+ | * Goldilocks uses the happens-before relation to define data-race free executions. | ||
+ | * The execution δ is race-free on data variable (o; d) if for all k; l such that α<sub>k</sub>, α<sub>l</sub> are elements of {read(o; d); write(o; d)}, we have k hb l or l hb k. | ||
+ | |||
+ | == Extended version of Goldilocks == | ||
+ | * Described in Goldilocks: a race and transaction-aware java runtime | ||
+ | * Does Static Analysis before Dynamic Analysis -> much faster | ||
+ | * Throws a DataRaceException when a data race is about to occur | ||
+ | * Applicable to both locks and transactions | ||
+ | |||
== References == | == References == |