Repository logo
 

A Separation Logic for Fictional Sequential Consistency

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

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

Abstract

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.

Description

Keywords

46 Information and Computing Sciences

Journal Title

Lecture Notes in Computer Science

Conference Name

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

Journal ISSN

0302-9743
1611-3349

Volume Title

Publisher

Springer

Rights

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