research-article

Open access

MoSeL: a general, extensible modal framework for interactive proofs in separation logic

Authors:

Robbert Krebbers,

Jacques-Henri Jourdan,

Joseph Tassarotti,

Jan-Oliver Kaiser,

Arthur Charguéraud,

Derek DreyerAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue ICFP

Article No.: 77, Pages 1 - 30

https://doi.org/10.1145/3236772

Published: 30 July 2018 Publication History

Abstract

A number of tools have been developed for carrying out separation-logic proofs mechanically using an interactive proof assistant. One of the most advanced such tools is the Iris Proof Mode (IPM) for Coq, which offers a rich set of tactics for making separation-logic proofs look and feel like ordinary Coq proofs. However, IPM is tied to a particular separation logic (namely, Iris), thus limiting its applicability.

In this paper, we propose MoSeL, a general and extensible Coq framework that brings the benefits of IPM to a much larger class of separation logics. Unlike IPM, MoSeL is applicable to both affine and linear separation logics (and combinations thereof), and provides generic tactics that can be easily extended to account for the bespoke connectives of the logics with which it is instantiated. To demonstrate the effectiveness of MoSeL, we have instantiated it to provide effective tactical support for interactive and semi-automated proofs in six very different separation logics.

Supplementary Material

WEBM File (a77-krebbers.webm)

Download
85.31 MB

References

[1]

Andrew W. Appel. 2006. Tactics for separation logic. Available at http://www.cs.princeton.edu/~appel/papers/septacs.pdf .

[2]

Robert Atkey. 2011. Amortised resource analysis with separation logic. LMCS 7, 2 (2011).

[3]

Jesper Bengtson, Jonas Braband Jensen, and Lars Birkedal. 2012. Charge! - A framework for higher-order separation logic in Coq. In ITP (LNCS), Vol. 7406. 315–331.

[4]

Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2004. A decidable fragment of separation logic. In FSTTCS. 97–109.

Digital Library

[5]

Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO. 115–137.

Digital Library

[6]

Aleš Bizjak and Lars Birkedal. 2018. On models of higher-order separation logic. ENTCS 336 (2018), 57–78.

[7]

Stephen Brookes. 2007. A semantics for concurrent separation logic. TCS 375, 1-3 (2007), 227–270.

Digital Library

[8]

Cristiano Calcagno, Peter W. O’Hearn, and Hongseok Yang. 2007. Local action and abstract separation logic. In LICS. 366–378.

Digital Library

[9]

Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. 2018. VST-Floyd: A separation logic tool to verify correctness of C programs. JAR 61, 1-4 (2018), 367–422.

Digital Library

[10]

Qinxiang Cao, Santiago Cuellar, and Andrew W. Appel. 2017. Bringing order to the separation logic jungle. In APLAS (LNCS), Vol. 10695. 190–211.

[11]

Arthur Charguéraud. 2011. Characteristic formulae for the verification of imperative programs. In ICFP. 418–430.

[12]

Arthur Charguéraud. 2018. CFML 2.0. http://www.chargueraud.org/softs/cfml/ .

[13]

Arthur Charguéraud and François Pottier. 2017. Temporary read-only permissions for separation logic. In ESOP (LNCS), Vol. 10201. 260–286.

[14]

Haogang Chen, Daniel Ziegler, Tej Chajed, Adam Chlipala, M. Frans Kaashoek, and Nickolai Zeldovich. 2015. Using Crash Hoare logic for certifying the FSCQ file system. In SOSP. 18–37.

Digital Library

[15]

Adam Chlipala. 2013. The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In ICFP. 391–402.

Digital Library

[16]

Jean-René Courtault, Didier Galmiche, and David J. Pym. 2016. A logic of separating modalities. TCS 637 (2016), 30–58.

Digital Library

[17]

Pedro da Rocha Pinto, Thomas Dinsdale-Young, and Philippa Gardner. 2014. TaDA: A logic for time and data abstraction. In ECOOP (LNCS), Vol. 8586. 207–231.

Digital Library

[18]

David Delahaye. 2000. A tactic language for the system Coq. In LPAR (LNCS), Vol. 1955. 85–95.

Digital Library

[19]

Robert Dockins, Andrew W. Appel, and Aquinas Hobor. 2008. Multimodal separation logic for reasoning about operational semantics. In MFPS.

Digital Library

[20]

Robert Dockins, Aquinas Hobor, and Andrew W. Appel. 2009. A fresh look at separation algebras and share accounting. In APLAS (LNCS), Vol. 5904. 161–177.

Digital Library

[21]

François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. 2009. Packaging mathematical structures. In TPHOLs (LNCS), Vol. 5674. 327–342.

Digital Library

[22]

Aquinas Hobor and Jules Villard. 2013. The ramifications of sharing in data structures. In POPL. 523–536.

Digital Library

[23]

Jonas Braband Jensen, Nick Benton, and Andrew Kennedy. 2013. High-level separation logic for low-level code. In POPL. 301–314.

Digital Library

[24]

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2018a. Rustbelt: Securing the foundations of the Rust programming language. PACMPL 2, POPL, 66:1–66:34.

Digital Library

[25]

Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256–269.

Digital Library

[26]

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal, and Derek Dreyer. 2018b. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Accepted for publication in JFP (2018).

[27]

Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal, and Derek Dreyer. 2015. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL. 637–650.

Digital Library

[28]

Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP (LIPIcs), Vol. 74. 17:1–17:29.

[29]

Robbert Krebbers. 2015. The C standard formalized in Coq. Ph.D. Dissertation. Radboud University.

[30]

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, and Derek Dreyer. 2018. Coq repository for MoSeL. http://iris- project.org/mosel/ .

[31]

Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal. 2017a. The essence of higher-order concurrent separation logic. In ESOP (LNCS), Vol. 10201. 696–723.

Digital Library

[32]

Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017b. Interactive proofs in higher-order concurrent separation logic. In POPL. 205–217.

Digital Library

[33]

Daniel J. Lehmann, Amir Pnueli, and Jonathan Stavi. 1981. Impartiality, justice and fairness: The ethics of concurrent termination. In Automata, Languages and Programming. 264–277.

Digital Library

[34]

Andrew McCreight. 2009. Practical tactics for separation logic. In TPHOLs (LNCS), Vol. 5674. 343–358.

Digital Library

[35]

Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. 2010. Structuring the verification of heap-manipulating programs. In POPL. 261–274.

Digital Library

[36]

Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. TCS 375, 1 (2007), 271–307.

Digital Library

[37]

Peter W. O’Hearn and David J. Pym. 1999. The logic of bunched implications. Bulletin of Symbolic Logic 5, 2 (1999), 215–244.

[38]

Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local reasoning about programs that alter data structures. In CSL (LNCS), Vol. 2142. 1–18.

Digital Library

[39]

François Pottier. 2013. Syntactic soundness proof of a type-and-capability system with hidden state. JFP 23, 1 (2013), 38–144.

Digital Library

[40]

David J. Pym. 2002. The semantics and proof theory of the logic of bunched implications. Springer.

[41]

David J. Pym, Peter W. O’Hearn, and Hongseok Yang. 2004. Possible worlds and resources: the semantics of BI. TCS 315, 1 (2004), 257–305.

Digital Library

[42]

John C. Reynolds. 2000. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science. 303–321.

[43]

John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. 55–74.

Digital Library

[44]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015a. Mechanized verification of fine-grained concurrent programs. In PLDI. 77–87.

Digital Library

[45]

Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015b. Specifying and verifying concurrent algorithms with histories and subjectivity. In ESOP. 333–358.

Digital Library

[46]

Matthieu Sozeau and Nicolas Oury. 2008. First-class type classes. In TPHOLs (LNCS), Vol. 5170. 278–293.

Digital Library

[47]

Bas Spitters and Eelis van der Weegen. 2011. Type classes for mathematics in type theory. MSCS 21, 4 (2011), 795–825.

[48]

David Swasey, Deepak Garg, and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. PACMPL 1, OOPSLA (2017), 89:1–89:26.

Digital Library

[49]

Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A higher-order logic for concurrent termination-preserving refinement. In ESOP (LNCS), Vol. 10201. 909–936.

Digital Library

[50]

Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, and Lars Birkedal. 2018. A logical relation for monadic encapsulation of state: Proving contextual equivalences in the presence of runST. PACMPL 2, POPL (2018), 64:1–64:28.

Digital Library

[51]

Harvey Tuch, Gerwin Klein, and Michael Norrish. 2007. Types, bytes, and separation logic. In POPL. 97–108.

Digital Library

[52]

Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. In ICFP. 377–390.

Digital Library

[53]

Viktor Vafeiadis and Matthew J. Parkinson. 2007. A marriage of rely/guarantee and separation logic. In CONCUR (LNCS), Vol. 4703. 256–271.

Digital Library

Cited By

Carnier DPottier FKeuchel S(2024)Type Inference LogicsProceedings of the ACM on Programming Languages10.1145/36897868:OOPSLA2(2125-2155)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689786
Hinrichsen JJacobs JKrebbers R(2024)Multris: Functional Verification of Multiparty Message Passing in Separation LogicProceedings of the ACM on Programming Languages10.1145/36897628:OOPSLA2(1446-1474)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689762
Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Show More Cited By

Index Terms

MoSeL: a general, extensible modal framework for interactive proofs in separation logic
1. Theory of computation
  1. Logic
    1. Logic and verification
    2. Separation logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
Interactive proofs in higher-order concurrent separation logic
POPL '17

When using a proof assistant to reason in an embedded logic -- like separation logic -- one cannot benefit from the proof contexts and basic tactics of the proof assistant. This results in proofs that are at a too low level of abstraction because they ...
A modal logic internalizing normal proofs

In the proof-theoretic study of logic, the notion of normal proof has been understood and investigated as a metalogical property. Usually we formulate a system of logic, identify a class of proofs as normal proofs, and show that every proof in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue ICFP

September 2018

1133 pages

EISSN:2475-1421

DOI:10.1145/3243631

Issue’s Table of Contents

Copyright © 2018 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 July 2018

Published in PACMPL Volume 2, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

French National Research Agency
European Research Council
Flemish Research Fund

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

46
Total Citations
View Citations
607
Total Downloads

Downloads (Last 12 months)120
Downloads (Last 6 weeks)18

Reflects downloads up to 17 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Carnier DPottier FKeuchel S(2024)Type Inference LogicsProceedings of the ACM on Programming Languages10.1145/36897868:OOPSLA2(2125-2155)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689786
Hinrichsen JJacobs JKrebbers R(2024)Multris: Functional Verification of Multiparty Message Passing in Separation LogicProceedings of the ACM on Programming Languages10.1145/36897628:OOPSLA2(1446-1474)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689762
Haselwarter PLi Kde Medeiros MGregersen SAguirre ATassarotti JBirkedal L(2024)Tachis: Higher-Order Separation Logic with Credits for Expected CostsProceedings of the ACM on Programming Languages10.1145/36897538:OOPSLA2(1189-1218)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689753
Somers TKrebbers R(2024)Verified Lock-Free Session Channels with LinkingProceedings of the ACM on Programming Languages10.1145/36897328:OOPSLA2(588-617)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689732
Timany AKrebbers RDreyer DBirkedal L(2024)A Logical Approach to Type SoundnessJournal of the ACM10.1145/367695471:6(1-75)Online publication date: 11-Nov-2024
https://dl.acm.org/doi/10.1145/3676954
Park SKim JMulder IJung JLee JKrebbers RKang J(2024)A Proof Recipe for Linearizability in Relaxed Memory Separation LogicProceedings of the ACM on Programming Languages10.1145/36563848:PLDI(175-198)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656384
Jacobs JHinrichsen JKrebbers R(2024)Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message PassingProceedings of the ACM on Programming Languages10.1145/36328898:POPL(1385-1417)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632889
Moine AWestrick SBalzer S(2024)DisLog: A Separation Logic for DisentanglementProceedings of the ACM on Programming Languages10.1145/36328538:POPL(302-331)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632853
Mansky WDu K(2024)An Iris Instance for Verifying CompCert C ProgramsProceedings of the ACM on Programming Languages10.1145/36328488:POPL(148-174)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632848
Jacobs JHinrichsen JKrebbers R(2023)Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)Proceedings of the ACM on Programming Languages10.1145/36078567:ICFP(768-795)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607856
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents