A separation logic for fictional sequential consistency

Autor: Lars Birkedal, Jean Pichon-Pharabod, Filip Sieczkowski, Kasper Svendsen
Přispěvatelé: Vitek , Jan
Jazyk: angličtina
Rok vydání: 2015
Předmět:
Zdroj: Sieczkowski, F, Svendsen, K, Birkedal, L & Pichon-Pharabod, J 2015, A separation logic for fictional sequential consistency . in J Vitek (ed.), Programming Languages and Systems : 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 . Springer, Lecture Notes in Computer Science, vol. 9032, pp. 736-761, European Symposium on Programming, London, United Kingdom, 11/04/2015 . https://doi.org/10.1007/978-3-662-46669-8_30
Programming Languages and Systems ISBN: 9783662466681
ESOP
Popis: 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.
Databáze: OpenAIRE
Externí odkaz: