Repository logo

A Separation Logic for Fictional Sequential Consistency

Accepted version


Conference Object

Change log


Pichon-Pharabod, Jean 
Sieczkowski, Filip 
Birkedal, Lars 
Svendsen, Kasper 


To improve performance, modern multiprocessors and pro- gramming 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 synchro- nization 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 cor- rectly, 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 pro- vide sufficient guarantees, the logic hides the underlying complexity and admits standard separation logic rules for reasoning about their more high-level clients.



46 Information and Computing Sciences

Journal Title

Conference Name

24th European Symposium on Programming, ESOP 2015, Queen Mary, University of London, held as part of the ETAPS Symposium

Journal ISSN


Volume Title




All rights reserved
Engineering and Physical Sciences Research Council (EP/K008528/1)