Robbert Krebbers
Amin Timany
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
- Andrew W. Appel. 2006. Tactics for separation logic. Available at http://www.cs.princeton.edu/~appel/papers/septacs.pdf .Google Scholar
- Robert Atkey. 2011. Amortised resource analysis with separation logic. LMCS 7, 2 (2011).Google Scholar
- 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.Google Scholar
- Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2004. A decidable fragment of separation logic. In FSTTCS. 97–109. Google ScholarDigital Library
- Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO. 115–137. Google ScholarDigital Library
- Aleš Bizjak and Lars Birkedal. 2018. On models of higher-order separation logic. ENTCS 336 (2018), 57–78.Google ScholarCross Ref
- Stephen Brookes. 2007. A semantics for concurrent separation logic. TCS 375, 1-3 (2007), 227–270. Google ScholarDigital Library
- Cristiano Calcagno, Peter W. O’Hearn, and Hongseok Yang. 2007. Local action and abstract separation logic. In LICS. 366–378. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Qinxiang Cao, Santiago Cuellar, and Andrew W. Appel. 2017. Bringing order to the separation logic jungle. In APLAS (LNCS), Vol. 10695. 190–211.Google Scholar
- Arthur Charguéraud. 2011. Characteristic formulae for the verification of imperative programs. In ICFP. 418–430.Google Scholar
- Arthur Charguéraud. 2018. CFML 2.0. http://www.chargueraud.org/softs/cfml/ .Google Scholar
- Arthur Charguéraud and François Pottier. 2017. Temporary read-only permissions for separation logic. In ESOP (LNCS), Vol. 10201. 260–286.Google Scholar
- 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. Google ScholarDigital Library
- Adam Chlipala. 2013. The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In ICFP. 391–402. Google ScholarDigital Library
- Jean-René Courtault, Didier Galmiche, and David J. Pym. 2016. A logic of separating modalities. TCS 637 (2016), 30–58. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- David Delahaye. 2000. A tactic language for the system Coq. In LPAR (LNCS), Vol. 1955. 85–95. Google ScholarDigital Library
- Robert Dockins, Andrew W. Appel, and Aquinas Hobor. 2008. Multimodal separation logic for reasoning about operational semantics. In MFPS. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. 2009. Packaging mathematical structures. In TPHOLs (LNCS), Vol. 5674. 327–342. Google ScholarDigital Library
- Aquinas Hobor and Jules Villard. 2013. The ramifications of sharing in data structures. In POPL. 523–536. Google ScholarDigital Library
- Jonas Braband Jensen, Nick Benton, and Andrew Kennedy. 2013. High-level separation logic for low-level code. In POPL. 301–314. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Ralf Jung, Robbert Krebbers, Lars Birkedal, and Derek Dreyer. 2016. Higher-order ghost state. In ICFP. 256–269. Google ScholarDigital Library
- 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).Google Scholar
- 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. Google ScholarDigital Library
- 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.Google Scholar
- Robbert Krebbers. 2015. The C standard formalized in Coq. Ph.D. Dissertation. Radboud University.Google Scholar
- 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/ .Google Scholar
- 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. Google ScholarDigital Library
- Robbert Krebbers, Amin Timany, and Lars Birkedal. 2017b. Interactive proofs in higher-order concurrent separation logic. In POPL. 205–217. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Andrew McCreight. 2009. Practical tactics for separation logic. In TPHOLs (LNCS), Vol. 5674. 343–358. Google ScholarDigital Library
- Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. 2010. Structuring the verification of heap-manipulating programs. In POPL. 261–274. Google ScholarDigital Library
- Peter W. O’Hearn. 2007. Resources, concurrency, and local reasoning. TCS 375, 1 (2007), 271–307. Google ScholarDigital Library
- Peter W. O’Hearn and David J. Pym. 1999. The logic of bunched implications. Bulletin of Symbolic Logic 5, 2 (1999), 215–244.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- François Pottier. 2013. Syntactic soundness proof of a type-and-capability system with hidden state. JFP 23, 1 (2013), 38–144. Google ScholarDigital Library
- David J. Pym. 2002. The semantics and proof theory of the logic of bunched implications. Springer.Google Scholar
- 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. Google ScholarDigital Library
- John C. Reynolds. 2000. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science. 303–321.Google Scholar
- John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. 55–74. Google ScholarDigital Library
- Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015a. Mechanized verification of fine-grained concurrent programs. In PLDI. 77–87. Google ScholarDigital Library
- Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. 2015b. Specifying and verifying concurrent algorithms with histories and subjectivity. In ESOP. 333–358. Google ScholarDigital Library
- Matthieu Sozeau and Nicolas Oury. 2008. First-class type classes. In TPHOLs (LNCS), Vol. 5170. 278–293. Google ScholarDigital Library
- Bas Spitters and Eelis van der Weegen. 2011. Type classes for mathematics in type theory. MSCS 21, 4 (2011), 795–825.Google Scholar
- David Swasey, Deepak Garg, and Derek Dreyer. 2017. Robust and compositional verification of object capability patterns. PACMPL 1, OOPSLA (2017), 89:1–89:26. Google ScholarDigital Library
- Joseph Tassarotti, Ralf Jung, and Robert Harper. 2017. A higher-order logic for concurrent termination-preserving refinement. In ESOP (LNCS), Vol. 10201. 909–936. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Harvey Tuch, Gerwin Klein, and Michael Norrish. 2007. Types, bytes, and separation logic. In POPL. 97–108. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Viktor Vafeiadis and Matthew J. Parkinson. 2007. A marriage of rely/guarantee and separation logic. In CONCUR (LNCS), Vol. 4703. 256–271. Google ScholarDigital Library
Index Terms
- MoSeL: a general, extensible modal framework for interactive proofs in separation logic
Recommendations
Interactive proofs in higher-order concurrent separation logic
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesWhen 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 '17When 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