A programming language perspective on transactional memory consistency
A programming language perspective on transactional memory consistency
复制标题
从编程语言角度看事务内存一致性
DOI：
10.1145/2484239.2484267
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
N. Rinetzky
中科院分区：
文献类型：
--
作者：
H. Attiya;Alexey Gotsman;Sandeep Hans;N. Rinetzky
交易记忆（TM）已被誉为简化并发编程的范例。尽管已经提出了几种一致性条件，但它们没有正式化原子块的直观语义，而在编程语言中使用TM的界面。
为了缩小这一差距，我们将程序员的直观期望形式化为TM实现之间的观察性改进：如果程序使用前者使用后者，则可以再现了使用前者的程序的每个用户观察行为，从而在观察上进行了精炼。这使程序员可以使用摘要TM形式的直觉语义来推论程序的行为；观察性改进关系意味着结论将在程序使用混凝土TM时延续到案例中。我们表明，对于一种特定的编程语言和可观察行为的概念，众所周知的不透明度一致性条件的变体足以观察性完善，并且其对完整历史的限制也是必要的。
我们的结果提出了一种评估和比较TM一致性条件的新方法。他们还可以减少证明TM正确实现其编程语言接口的努力，仅要求其开发人员表明其满足相应的一致性条件。
Transactional memory (TM) has been hailed as a paradigm for simplifying concurrent programming. While several consistency conditions have been suggested for TM, they fall short of formalizing the intuitive semantics of atomic blocks, the interface through which a TM is used in a programming language.
To close this gap, we formalize the intuitive expectations of a programmer as observational refinement between TM implementations: a concrete TM observationally refines an abstract one if every user-observable behavior of a program using the former can be reproduced if the program uses the latter. This allows the programmer to reason about the behavior of a program using the intuitive semantics formalized by the abstract TM; the observational refinement relation implies that the conclusions will carry over to the case when the program uses the concrete TM. We show that, for a particular programming language and notions of observable behavior, a variant of the well-known consistency condition of opacity is sufficient for observational refinement, and its restriction to complete histories is furthermore necessary.
Our results suggest a new approach to evaluating and comparing TM consistency conditions. They can also reduce the effort of proving that a TM implements its programming language interface correctly, by only requiring its developer to show that it satisfies the corresponding consistency condition.
影响因子：
1.1
作者：
Filipovic I
通讯作者：
Filipovic I