Higher-order ghost state
- 4 September 2016
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 51 (9), 256-269
- https://doi.org/10.1145/3022670.2951943
Abstract
The development of concurrent separation logic (CSL) has sparked a long line of work on modular verification of sophisticated concurrent programs. Two of the most important features supported by several existing extensions to CSL are higher-order quantification and custom ghost state. However, none of the logics that support both of these features reap the full potential of their combination. In particular, none of them provide general support for a feature we dub "higher-order ghost state": the ability to store arbitrary higher-order separation-logic predicates in ghost variables. In this paper, we propose higher-order ghost state as a interesting and useful extension to CSL, which we formalize in the framework of Jung et al.'s recently developed Iris logic. To justify its soundness, we develop a novel algebraic structure called CMRAs ("cameras"), which can be thought of as "step-indexed partial commutative monoids". Finally, we show that Iris proofs utilizing higher-order ghost state can be effectively formalized in Coq, and discuss the challenges we faced in formalizing them.Keywords
Funding Information
- ERC (683289)
This publication has 26 references indexed in Scilit:
- Syntactic soundness proof of a type-and-capability system with hidden stateJournal of Functional Programming, 2012
- Step-Indexed Kripke Model of Separation Logic for Storable LocksElectronic Notes in Theoretical Computer Science, 2011
- The category-theoretic solution of recursive metric-space equationsTheoretical Computer Science, 2010
- A Fresh Look at Separation Algebras and Share AccountingLecture Notes in Computer Science, 2009
- Hints in UnificationLecture Notes in Computer Science, 2009
- Packaging Mathematical StructuresLecture Notes in Computer Science, 2009
- Resources, concurrency, and local reasoningTheoretical Computer Science, 2007
- An indexed model of recursive types for foundational proof-carrying codeACM Transactions on Programming Languages and Systems, 2001
- Solving reflexive domain equations in a category of complete metric spacesJournal of Computer and System Sciences, 1989
- Verifying properties of parallel programsCommunications of the ACM, 1976