Top

Published in:

2017 | OriginalPaper | Chapter

Bringing Order to the Separation Logic Jungle

Authors : Qinxiang Cao, Santiago Cuellar, Andrew W. Appel

Published in: Programming Languages and Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Research results from so-called “classical” separation logics are not easily ported to so-called “intuitionistic” separation logics, and vice versa. Basic questions like, “Can the frame rule be proved independently of whether the programming language is garbage-collected?” “Can amortized resource analysis be ported from one separation logic to another?” should be straightforward. But they are not. Proofs done in a particular separation logic are difficult to generalize. We argue that this limitation is caused by incompatible semantics. For example, emp sometimes holds everywhere and sometimes only on units.

In this paper, we introduce a unifying semantics and build a framework that allows to reason parametrically over all separation logics. Many separation algebras in the literature are accompanied, explicitly or implicitly, by a preorder. Our key insight is to axiomatize the interaction between the join relation and the preorder. We prove every separation logic to be sound and complete with respect to this unifying semantics. Further, our framework enables us to generalize the sound0.ness proofs for the frame rule and CSL. It also reveals a new world of meaningful intermediate separation logics between “intuitionistic” and “classical”.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Decision Procedure for Entailment of Symbolic Heaps with Arrays

next chapter Programming and Proving with Classical Types

Pottier also adds a passive execution order which constitutes what he calls a monotonic separation algebra. The idea is similar but goes in a different direction, aiming for a type system and not a separation logic.

Coq development: https://github.com/QinxiangCao/UnifySL. Appendix: http://www.cs.princeton.edu/~appel/papers/bringing-order-appendix.pdf.

Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers, Cambridge (2014)

Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657–683 (2001)CrossRef

Appel, A.W., Melliès, P.-A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2007)

Atkey, R.: Amortised resource analysis with separation logic. Logical Methods Comput. Sci. 7(2) (2011)

Bengtson, J., Jensen, J.B., Sieczkowski, F., Birkedal, L.: Verifying object-oriented programs with higher-order separation logic in Coq. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 22–38. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22863-6_5 CrossRef

Birkedal, L., Reus, B., Schwinghammer, J., Støvring, K., Thamsborg, J., Yang, H.: Step-indexed Kripke models over recursive worlds. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2011)

Brookes, S.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 16–34. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_2 CrossRef

Brotherston, J., Kanovich, M.: Undecidability of propositional separation logic and its neighbours. In: 2010 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 130–139. IEEE (2010)

Brotherston, J., Villard, J.: Parametric completeness for separation theories. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2014)

10.

Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007, pp. 366–378, Washington, DC, USA. IEEE Computer Society (2007)

11.

Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash hoare logic for certifying the FSCQ file system. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, 4–7 October 2015, pp. 18–37. ACM (2015)

12.

Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J., Yang, H.: Views: compositional reasoning for concurrent programs. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2013)

13.

Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 161–177. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10672-9_13 CrossRef

14.

Galmiche, D., Larchey-Wendling, D.: Expressivity properties of Boolean BI through relational models. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 357–368. Springer, Heidelberg (2006). https://doi.org/10.1007/11944836_33 CrossRef

15.

Galmiche, D., Méry, D., Pym, D.J.: The semantics of BI and resource tableaux. Mathe. Struct. Comput. Sci. 15(6), 1033–1088 (2005)MathSciNetCrossRefMATH

16.

Gotsman, A., Berdine, J., Cook, B.: Precision and the conjunction rule in concurrent separation logic. Electr. Notes Theor. Comput. Sci. 276, 171–190 (2011)MathSciNetCrossRefMATH

17.

Hobor, A., Dockins, R., Appel, A.W.: A theory of indirection via approximation. In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2010)

18.

Hur, C.-K., Dreyer, D., Vafeiadis, V.: Separation logic in the presence of garbage collection. In: Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, 21–24 June 2011, Toronto, Ontario, Canada, pp. 247–256 (2011)

19.

Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2001)

20.

Jensen, J.B.: Techniques for model construction in separation logic. Ph.D. thesis, IT University of Copenhagen, March 2014

21.

Jensen, J.B., Birkedal, L.: Fictional separation logic. In: Programming Languages and Systems - 21st European Symposium on Programming (2012)

22.

Jung, R., Swasey, D., Sieczkowski, F., Svendsen, K., Turon, A., Birkedal, L., Dreyer, D.: Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (2015)

23.

Kripke, S.A.: Semantical analysis of intuitionistic logic i. Studies Logic Found. Mathe. 50, 92–130 (1965)MathSciNetCrossRefMATH

24.

Larchey-Wendling, D., Galmiche, D.: Exploring the relation between intuitionistic BI and boolean BI: an unexpected embedding. Mathe. Struct. Comput. Sci. 19(3), 435–500 (2009)MathSciNetCrossRefMATH

25.

O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bull. Symbolic Logic 5(2), 215–244 (1999)MathSciNetCrossRefMATH

26.

O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, 14–16 January 2004, pp. 268–280 (2004)

27.

Parkinson, M.: The next 700 separation logics. In: Leavens, G.T., O’Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 169–182. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15057-9_12 CrossRef

28.

Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 439–458. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_23 CrossRef

29.

Pilkiewicz, A., Pottier, F.: The essence of monotonic state. In: Proceedings of TLDI 2011: 2011 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 73–86 (2011)

30.

Pottier, F.: Syntactic soundness proof of a type-and-capability system with hidden state. J. Funct. Program. 23(1), 38–144 (2013)MathSciNetCrossRefMATH

31.

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)MathSciNetCrossRefMATH

32.

Reynolds, J.C.: Intuitionistic reasoning about shared mutable data structure. In: Millennial Perspectives in Computer Science, pp. 303–321. Palgrave (2000)

33.

Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic. Technical report, University of Edinburgh, College of Science and Engineering, School of Informatics (1994)

Title: Bringing Order to the Separation Logic Jungle
Authors: Qinxiang Cao
Santiago Cuellar
Andrew W. Appel
Publisher: Springer International Publishing
Book: Programming Languages and Systems
Print ISBN: 978-3-319-71236-9

Electronic ISBN: 978-3-319-71237-6

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-71237-6_10

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner