Name
Abstract | ||
|---|---|---|
Modern multi-core microprocessors implement weak memory consistency models; programming for these architectures is a challenge. This paper solves a problem open for ten years, and originally posed by Rinard: we identify sufficient conditions for a data flow analysis to be sound w.r.t. weak memory models. We first identify a class of analyses that are sound, and provide a formal proof of soundness at the level of trace semantics. Then we discuss how analyses unsound with respect to weak memory models can be repaired via a fixed point iteration, and provide experimental data on the runtime overhead of this method. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/978-3-642-25318-8_21 | APLAS |
Keywords | Field | DocType |
sufficient condition,formal proof,weak memory consistency model,weak memory model,modern multi-core microprocessors,runtime overhead,fixed point iteration,experimental data,data flow analysis,sound w | Sequential consistency,Computer science,Fixed-point iteration,Data-flow analysis,Theoretical computer science,Memory model,Consistency model,Soundness,Formal proof,Data flow diagram | Conference |
Citations | PageRank | References |
9 | 0.56 | 27 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jade Alglave | 1 | 608 | 26.53 |
| Daniel Kroening | 2 | 3084 | 187.60 |
| John Lugton | 3 | 9 | 0.56 |
| Vincent Nimal | 4 | 75 | 2.51 |
| Michael Tautschnig | 5 | 425 | 25.84 |