Oracle semantics for concurrent separation logic

Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli

Research output: Chapter in Book/Report/Conference proceedingConference contribution

66 Scopus citations

Abstract

We define (with machine-checked proofs in Coq) a modular operational semantics for Concurrent C minor-a language with shared memory, spawnable threads, and first-class locks. By modular we mean that one can reason about sequential control and data-flow knowing almost nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and data-flow constructs. We present a Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational semantics. Using our modularity principle, we proved the sequential C.S.L. rules (those inherited from sequential Separation Logic) simply by adapting Appel & Blazy's machine-checked soundness proofs. Our Concurrent C minor operational semantics is designed to connect to Leroy's optimizing (sequential) C minor compiler; we propose our modular semantics as a way to adapt Leroy's compiler-correctness proofs to the concurrent setting. Thus we will obtain end-to-end proofs: the properties you prove in Concurrent Separation Logic will be true of the program that actually executes on the machine.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 17th European Symposium on Programming, ESOP 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings
Pages353-367
Number of pages15
DOIs
StatePublished - Jul 21 2008
Event17th European Symposium on Programming, ESOP 2008 - Budapest, Hungary
Duration: Mar 29 2008Apr 6 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4960 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other17th European Symposium on Programming, ESOP 2008
CountryHungary
CityBudapest
Period3/29/084/6/08

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Oracle semantics for concurrent separation logic'. Together they form a unique fingerprint.

  • Cite this

    Hobor, A., Appel, A. W., & Nardelli, F. Z. (2008). Oracle semantics for concurrent separation logic. In Programming Languages and Systems - 17th European Symposium on Programming, ESOP 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings (pp. 353-367). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4960 LNCS). https://doi.org/10.1007/978-3-540-78739-6_27