Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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 ==
 
sav07_lecture_26.txt · Last modified: 2007/07/03 01:11 by feride.cetin
 
© EPFL 2018 - Legal notice