skip to main content
review-article
Open Access

Separation logic

Published:28 January 2019Publication History
Skip Abstract Section

Abstract

Separation logic is a key development in formal reasoning about programs, opening up new lines of attack on longstanding problems.

Skip Supplemental Material Section

Supplemental Material

References

  1. Appel, A.W. Program Logics for Certified Compilers. Cambridge University Press, U.K., 2014. Google ScholarGoogle ScholarCross RefCross Ref
  2. Berdine, J. Calcagno, C. and O'Hearn, P.W. Smallfoot: Modular automatic assertion checking with separation logic. LNCS FMCO 4111 (2005) 115--137, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. Berdine, J., Cook, B. and Ishtiaq, S. SLAyer: Memory safety for systems-level code. In Proceedings of CAV, 2011, 178--183. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. Beringer, L., Petcher, A., Ye, K.Q. and Appel, A.W. Verified correctness and security of OpenSSL HMAC. In Proceedings of 24<sup>th</sup> USENIX Security Symposium, 2015, 207--221. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. Biering, B., Birkedal, L. and Torp-Smith, N. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM TOPLAS 29, 4 (2007). Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. Bornat, R. Proving pointer programs in Hoare logic. LNCS MPC 1837 (2000) 102--126. Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. Bornat, R., Calcagno, C., O'Hearn, P.W. and Parkinson, M.J. Permission accounting in separation logic. In Proceedings of POPL, 2005, 259--270. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. Brookes, S. A semantics for concurrent separation logic. Theor. Comput. Sci., 375, 1--3 (2007), 227--270. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. Brookes, S. and O'Hearn, P.W. Concurrent separation logic. SIGLOG News 3, 3 (2016), 47--65. Google ScholarGoogle ScholarDigital LibraryDigital Library
  10. Burstall, R.M. Some techniques for proving correctness of programs which alter data structures. Machine Intelligence 7, 1 (1972), 23--50.Google ScholarGoogle Scholar
  11. Calcagno, C. et al. Moving fast with software verification. In Proceedings of NASA Formal Methods Symposium, 2015, 3--11.Google ScholarGoogle ScholarCross RefCross Ref
  12. Calcagno, C., Distefano, D., O'Hearn, P.W. and Yang, H. Compositional shape analysis by means of bi-abduction. J. ACM 58, 6 (2011), 26. Preliminary version in Proceedings of POPL'09. Google ScholarGoogle ScholarDigital LibraryDigital Library
  13. Calcagno, C., O'Hearn, P.W. and Yang, H. Local action and abstract separation logic. LICS, 2007, 366--378. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. Chen, H., Ziegler, F., Chajed, T., Chlipala, A., Kaashoek, M.F. and Zeldovich, N. Using Crash Hoare logic for certifying the FSCQ file system. In Proceedings of SOSP, pages 18--37, 2015. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. Cousot, P. and Cousot, R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of POPL, 1977, 238--252. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. Dijkstra, E.W. Cooperating sequential processes. Programming Languages, Academic Press, 1968, 43--112.Google ScholarGoogle Scholar
  17. Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M.J. and Yang, H. Views: Compositional reasoning for concurrent programs. In Proceedings of POPL, 2013, 287--300. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. Dinsdale-Young, T., Dodds, M., Gardner, M., Parkinson, M.J. and Vafeiadis, V. Concurrent abstract predicates. In Proceedings of ECOOP, 2010, 504--528. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. Dinsdale-Young, T., Gardner, P. and Wheelhouse, M.J. Abstraction and refinement for local reasoning. In Proceedings of VSTTE, 2010, 199--215. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. Distefano, D., O'Hearn, P.W. and Yang, H. A local shape analysis based on separation logic. In Proceedings of TACAS, 2006, 287--302. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. Floyd, R.W. Assigning meanings to programs. In Proceedings of the Symposium on Applied Mathematics. J.T. Schwartz, ed. AMS, 1967, 19--32.Google ScholarGoogle ScholarCross RefCross Ref
  22. Hoare, C.A.R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (1969), 576--580. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. Hoare, C.A.R. Towards a theory of parallel programming. Operating Systems Techniques. Academic Press, 1972.Google ScholarGoogle Scholar
  24. Hoare, T., Möller, B., Struth, G. and Wehrman, I. Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program 80, 6 (2011), 266--296.Google ScholarGoogle ScholarCross RefCross Ref
  25. Hobor, A. and Villard, J. The ramifications of sharing in data structures. In Proceedings of 40<sup>th</sup> POPL, 2013, 523--536. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. Ishtiaq, S.S. and O'Hearn, P.W. BI as an assertion language for mutable data structures. In Proceedings of POPL, 2001, 14--26. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. Jones, C.B. Specification and design of (parallel) programs. In Proceedings of IFIP Congress, 1983, 321--332.Google ScholarGoogle Scholar
  28. Jung, R. Jourdan, J.-H., Krebbers, R. and Dreyer. D. RustBelt: Securing the foundations of the Rust programming language. In Proceedings of PACMPL, 2018. Google ScholarGoogle ScholarDigital LibraryDigital Library
  29. Krebbers, R., Jung, R., Bizjak, A., Jourdan, J-H, Dreyer, D. and Birkedal, L. The essence of higher-order concurrent separation logic. In Proceedings of ESOP, 2017, 696--723. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. O'Hearn, P.W. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 1--3 (2007), 271--307. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. O'Hearn, P.W and Pym, D.J. The logic of bunched implications. Bulletin of Symbolic Logic 5, 2 (1999), 215--244.Google ScholarGoogle ScholarCross RefCross Ref
  32. O'Hearn, P.W., Reynolds, J.C. and Yang, H. Local reasoning about programs that alter data structures. In Proceedings of CSL, 2001, 1--19. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. Parkinson. M.J. Local reasoning for Java. Ph.D. thesis. University of Cambridge, U.K., 2005.Google ScholarGoogle Scholar
  34. Parkinson, M.J., Bornat, R. and Calcagno, C. Variables as resource in Hoare logics. In Proceedings of 21<sup>st</sup> LIC, 2006, 137--146. Google ScholarGoogle ScholarDigital LibraryDigital Library
  35. Philippaerts, P., Mühlberg, J.T., Penninckx, W., Smans, J., Jacobs, B. and Piessens, F. Software verification with verifast: Industrial case studies. Sci. Comput. Program. 82 (2014), 77--97. Google ScholarGoogle ScholarDigital LibraryDigital Library
  36. Pym, D., O'Hearn, P. and Yang, H. Possible worlds and resources: The semantics of BI. Theoret. Comp. Sci. 315, 1 (2004), 257--305. Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. Reynolds, J,C. Intuitionistic reasoning about shared mutable data structure. Millennial Perspectives in Computer Science, Cornerstones of Computing. Palgrave Macmillan, 2000.Google ScholarGoogle Scholar
  38. Reynolds, J.C. Separation logic: A logic for shared mutable data structures. LICS, 2002, 55--74. Google ScholarGoogle ScholarDigital LibraryDigital Library
  39. Sergey, I., Nanevski, A. and Banerjee, A. Mechanized verification of fine-grained concurrent programs. In Proceedings of 36<sup>th</sup> PLDI, 2015, 77--87. Google ScholarGoogle ScholarDigital LibraryDigital Library
  40. Turing, A.M. Checking a large routine. Report of a Conference on High-Speed Automatic Calculating Machines. Univ. Math. Lab., Cambridge, U.K., 1949, 67--69.Google ScholarGoogle Scholar
  41. Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H. and Li, Z. A practical verification framework for preemptive OS kernels. In Proceedings of CAV, 2016.Google ScholarGoogle ScholarCross RefCross Ref
  42. Yang, H. Local Reasoning for Stateful Programs. Ph.D. thesis. University of Illinois, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  43. Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D. and O'Hearn, P.W. Scalable shape analysis for systems code. In Proceedings of CAV, 2008, 385--398. Google ScholarGoogle ScholarDigital LibraryDigital Library
  44. Yang, H. and O'Hearn, P.W. A semantic basis for local reasoning. In Proceedings of FoSSaCS, 2002, 402--416. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Separation logic

        Recommendations

        Reviews

        A. Squassabia

        Formal reasoning about mutable data can be difficult when concurrency is present, for instance, when attempting mutation of the same data at the same time from multiple processors; or when aliasing is present, for instance, when the same data is non-local and mutation occurs within possibly sequential but independent contexts. This paper is a cursory introduction to, and a historical overview of, separation logic: a formal framework for reasoning about mutable data under concurrency. The reader interested in a deeper treatment will be pleased with the large and encompassing set of references provided. Separation logic allows for the construction of internally consistent models that, after excluding aliasing, provide formal means for either mechanical or human-assisted verification of the correctness of code. Past attempts at formal reasoning encompassing aliasing proved to be less fruitful than separation logic, which in turn, over the last couple of decades, has evolved into software tools of practical utility. The principles backing this value insist on developments affording the ability of separation logic to constrain reasoning within a local scope; to establish artifact ownership; to generate preconditions with mechanized reasoning; and to analyze code fragments compositionally-as opposed to needing to digest an entire code base. This latter ability in particular enables analysis to scale incrementally, validating larger codes a cluster at a time. According to the authors, there are vast opportunities for further work in this field. Progress with practical applications could be a panacea. As an observation, formal verification of correct behavior under partial failure was neither excluded nor explicitly mentioned as an area of opportunity for further work.

        Access critical reviews of Computing literature here

        Become a reviewer for Computing Reviews.

        Comments

        Login options

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

        Sign in

        Full Access

        • Published in

          cover image Communications of the ACM
          Communications of the ACM  Volume 62, Issue 2
          February 2019
          112 pages
          ISSN:0001-0782
          EISSN:1557-7317
          DOI:10.1145/3310134
          Issue’s Table of Contents

          Copyright © 2019 Owner/Author

          Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the Owner/Author.

          Publisher

          Association for Computing Machinery

          New York, NY, United States

          Publication History

          • Published: 28 January 2019

          Check for updates

          Qualifiers

          • review-article
          • Popular
          • Refereed

        PDF Format

        View or Download as a PDF file.

        PDF

        eReader

        View online with eReader.

        eReader

        HTML Format

        View this article in HTML Format .

        View HTML Format