Abstract
Separation Algebras serve as models of Separation Logics; Share Accounting allows reasoning about concurrent-read/exclusive- write resources in Separation Logic. In designing a Concurrent Separation Logic and in mechanizing proofs of its soundness, we found previous axiomatizations of separation algebras and previous systems of share accounting to be useful but imperfect. We adjust the axioms of separation algebras; we demonstrate an operator calculus for constructing new separation algebras; we present a more powerful system of share accounting with a new, simple model; and we provide a reusable Coq development.
Supported in part by National Science Foundation grant CNS-0627650 and a Lee Kuan Yew Postdoctoral Fellowship.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL 2005: Proc. of the 32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 259–270 (2005)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003)
Brotherston, J., Calcagno, C.: Classical BI: a logic for reasoning about dualising resources. In: POPL 2009: Proc. of the 36th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 328–339 (2009)
Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS 2007: Proceedings of the 22nd IEEE Symp. on Logic in Computer Science, pp. 366–378 (2007)
Hobor, A.: Oracle Semantics. PhD thesis, Princeton University (2008)
Hobor, A., Appel, A.W., Zappa Nardelli, F.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 353–367. Springer, Heidelberg (2008)
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL 2001: Proc. of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 14–26 (2001)
Parkinson, M.: Local Reasoning for Java. PhD thesis, Univ. of Cambridge (2005)
Pym, D.J., O’Hearn, P.W., Yang, H.: Possible worlds and resources: the semantics of BI. Theor. Comput. Sci. 315(1), 257–305 (2004)
Restall, G.: An Introduction to Substructural Logics. Routledge, London (2000)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002: Proc. of the 17th Annual IEEE Symp. on Logic in Computer Science, pp. 55–74 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dockins, R., Hobor, A., Appel, A.W. (2009). A Fresh Look at Separation Algebras and Share Accounting. In: Hu, Z. (eds) Programming Languages and Systems. APLAS 2009. Lecture Notes in Computer Science, vol 5904. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10672-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-10672-9_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10671-2
Online ISBN: 978-3-642-10672-9
eBook Packages: Computer ScienceComputer Science (R0)