Soundness of Data Flow Analyses for Weak Memory Models
Soundness of Data Flow Analyses for Weak Memory Models
复制标题
弱内存模型的数据流健全性分析
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Michael Tautschnig
中科院分区：
文献类型：
--
作者：
J. Alglave;D. Kroening;John Lugton;Vincent Nimal;Michael Tautschnig
现代多核微处理器实现弱内存一致性模型，这些架构的编程是一个挑战。本文解决了一个开放了十年的问题，最初由里纳德提出：我们确定了充分条件的数据流分析是健全的w.r.t.弱记忆模型我们首先确定了一类的分析是健全的，并提供了一个正式的证明，在跟踪语义的水平上的健全性。然后我们讨论如何通过定点迭代修复针对弱内存模型的不合理分析，并提供有关该方法运行时开销的实验数据。
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.