LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav07_lecture_26 [2007/07/02 23:33]
feride.cetin
sav07_lecture_26 [2007/07/03 01:11]
feride.cetin
Line 163: Line 163:
   * **Happens-before relation:** Data race occurs between two accesses to a shared variable if they are not ordered by the happens-before relation.   * **Happens-before relation:** Data race occurs between two accesses to a shared variable if they are not ordered by the happens-before relation.
  
 +  * A concurrent execution δ is represented by a finite sequence
  
 +{{sav1.jpg|Figure 4}}
 +  - t<​sub>​i</​sub>​ is a thread
 +  - 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()
  
 +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