Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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