Sciweavers

APLAS
2011
ACM

Soundness of Data Flow Analyses for Weak Memory Models

12 years 10 months ago
Soundness of Data Flow Analyses for Weak Memory Models
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.
Jade Alglave, Daniel Kroening, John Lugton, Vincen
Added 12 Dec 2011
Updated 12 Dec 2011
Type Journal
Year 2011
Where APLAS
Authors Jade Alglave, Daniel Kroening, John Lugton, Vincent Nimal, Michael Tautschnig
Comments (0)