A separation logic for fictional sequential consistency

作     者：Sieczkowski, Filip Svendsen, Kasper Birkedal, Lars Pichon-Pharabod, Jean 

作者机构：Aarhus University Denmark University of Cambridge United Kingdom 

出 版 物：《Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)》 (Lect. Notes Comput. Sci.)

年 卷 期：2015年第9032卷

页      面：736-761页

核心收录：

基　　金：Engineering and Physical Sciences Research Council  EPSRC  (EP/K008528/1) 

主　　题：Locks (fasteners) 

摘      要：To improve performance, modern multiprocessors and programming languages typically implement relaxed memory models that do not require all processors/threads to observe memory operations in the same order. To relieve programmers from having to reason directly about these relaxed behaviors, languages often provide efficient synchronization primitives and concurrent data structures with stronger high level guarantees about memory reorderings. For instance, locks usually ensure that when a thread acquires a lock, it can observe all memory operations of the releasing thread, prior to the release. When used correctly, these synchronization primitives and data structures allow clients to recover a fiction of a sequentially consistent memory model. In this paper we propose a new proof system, iCAP-TSO, that captures this fiction formally, for a language with a TSO memory model. The logic supports reasoning about libraries that directly exploit the relaxed memory model to achieve maximum efficiency. When these libraries provide sufficient guarantees, the logic hides the underlying complexity and admits standard separation logic rules for reasoning about their more high-level clients. © Springer-Verlag Berlin Heidelberg 2015.