logic is nice, but it’s the model that’s
really important.” My own prejudice
for semantics made me agree immediately. We were both beguiled by the
fact that this funky species of logic
could be described using down-to-earth computer science concepts like
RAMs and access bits.
What happened later came as a surprise. The specific heap/RAM model
gave way in importance to a more general class of nonstandard models based
on fictional rather than down-to-earth
separation. And the logic itself, particularly its proof theory, turned out to be extremely useful in automatic verification,
leading to many novel research tools
and eventually to Facebook Infer.
Still, I expect that in the long run it
will be the spirit rather than the letter of
SL that is more significant. Concepts of
frames, footprints, and separation as a
basis for modular reasoning seem to be
of fundamental importance, independently of the syntax used to describe
them. Indeed, one of the more important directions I see for further work is
in theoretical foundations that get at
the essence of scalable, modular reasoning in as formalism-independent
a way as possible. Theoretical synthesis would be extremely useful for three
reasons: To make it easier for people
to understand what has been achieved
by each new idea; to provide a simpler
jumping-off point for future work than
the union of the many specific advances; and, to suggest new, unexplored
avenues. Hoare has been advancing
an abstract, algebraic theory related to
CSL, which has components covering
semantics, proof theory, and testing,
and work along these lines is well worth
Other relevant reference points are
works on general versions of SL,
15 and work on
“separation without SL” discussed in
the appendix ( https://bit.ly/2CQD9CU).
Semantic fundamentals would be crucial to an adequate general foundation,
but I stress that proof theoretic and especially algorithmic aspects addressing
the central problem of scale should be
covered as well.
In conclusion, scalable reasoning
about code has come a long way since
the birth of SL around the turn of the
millennium, but it seems to me that
much more is possible both in funda-
mental understanding and in mecha-
nized techniques that help program-
mers in their daily work. I hope that
scientists and engineers will continue to
innovate on the fascinating problems in
Acknowledgments. This article is
dedicated to the memory of John C.
Reynolds (1935–2013). Our work to-
gether at the formative stage of sepa-
ration logic was incredibly intense,
exciting, and huge fun. I am fortunate
to have worked so closely with such
a brilliantly insightful scientist, who
was also a valued friend.
I thank my many other collaborators in the development of this
research, particularly David Pym,
Hongseok Yang, Richard Bornat, Cris-tiano Calcagno, Josh Berdine, Dino
Distefano, Steve Brookes, Matthew
Parkinson, Philippa Gardner, and
Tony Hoare. Finally, thanks to my colleagues at Facebook for our work together and for teaching me about applying logic in the real world.
1. Appel, A. W. Program Logics for Certified Compilers.
Cambridge University Press, U.K., 2014.
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.
3. Berdine, J., Cook, B. and Ishtiaq, S. SLAyer: Memory
safety for systems-level code. In Proceedings of CAV,
4. Beringer, L., Petcher, A., Ye, K.Q. and Appel, A. W. Verified
correctness and security of OpenSSL HMAC. In
Proceedings of 24th USENIX Security Symposium, 2015,
5. Biering, B., Birkedal, L. and Torp-Smith, N. BI-hyperdoctrines, higher-order separation logic, and
abstraction. ACM TOPLAS 29, 4 (2007).
6. Bornat, R. Proving pointer programs in Hoare logic.
LNCS MPC 1837 (2000) 102–126.
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.
8. Brookes, S. A semantics for concurrent separation logic.
Theor. Comput. Sci., 375, 1–3 (2007), 227–270.
9. Brookes, S. and O’Hearn, P. W. Concurrent separation
logic. SIGLOG News 3, 3 (2016), 47–65.
10. Burstall, R.M. Some techniques for proving correctness
of programs which alter data structures. Machine
Intelligence 7, 1 (1972), 23–50.
11. Calcagno, C. et al. Moving fast with software verification.
In Proceedings of NASA Formal Methods Symposium,
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.
13. Calcagno, C., O’Hearn, P. W. and Yang, H. Local action and
abstract separation logic. LICS, 2007, 366–378.
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.
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.
16. Dijkstra, E. W. Cooperating sequential processes.
Programming Languages, Academic Press, 1968,
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,
18. Dinsdale-Young, T., Dodds, M., Gardner, M., Parkinson,
M. J. and Vafeiadis, V. Concurrent abstract predicates. In
Proceedings of ECOOP, 2010, 504–528.
19. Dinsdale-Young, T., Gardner, P. and Wheelhouse, M.J.
Abstraction and refinement for local reasoning. In
Proceedings of VSTTE, 2010, 199–215.
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.
21. Floyd, R. W. Assigning meanings to programs. In
Proceedings of the Symposium on Applied Mathematics.
J. T. Schwartz, ed. AMS, 1967, 19–32.
22. Hoare, C. A.R. An axiomatic basis for computer
programming. Commun. ACM 12, 10 (1969), 576–580.
23. Hoare, C.A.R. Towards a theory of parallel
programming. Operati ng Systems Techniques.
Academic Press, 1972.
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.
25. Hobor, A. and Villard, J. The ramifications of sharing
in data structures. In Proceedings of 40th POPL, 2013,
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.
27. Jones, C.B. Specification and design of (parallel)
programs. In Proceedings of IFIP Congress, 1983,
28. Jung , R. Jourdan, J.-H., Krebbers, R. and Dreyer.
D. RustBelt: Securing the foundations of the Rust
programming language. In Proceedings of PACMPL ,
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,
30. O’Hearn, P. W. Resources, concurrency, and local
reasoning. Theor. Comput. Sci. 375, 1-3 (2007), 271–307.
31. O’Hearn, P. W and Pym, D.J. The logic of bunched
implications. Bulletin of Symbolic Logic 5, 2 (1999),
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.
33. Parkinson. M.J. Local reasoning for Java. Ph. D. thesis.
University of Cambridge, U.K., 2005.
34. Parkinson, M.J., Bornat, R. and Calcagno, C. Variables
as resource in Hoare logics. In Proceedings of 21st LIC,
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.
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.
37. Reynolds, J,C. Intuitionistic reasoning about shared
mutable data structure. Millennial Perspectives in
Computer Science, Cornerstones of Computing. Palgrave
38. Reynolds, J.C. Separation logic: A logic for shared
mutable data structures. LICS, 2002, 55–74.
39. Sergey, I., Nanevski, A. and Banerjee, A. Mechanized
verification of fine-grained concurrent programs. In
Proceedings of 36th PLDI, 2015, 77–87.
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,
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.
42. Yang, H. Local Reasoning for Stateful Programs. Ph. D.
thesis. University of Illinois, 2001.
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,
44. Yang, H. and O’Hearn, P. W. A semantic basis for local
reasoning. In Proceedings of FoSSaCS, 2002, 402–416.
Peter O’Hearn ( firstname.lastname@example.org) is a research
scientist at Facebook and professor of computer science
at University College London, U.K.
© 2019 ACM 0001-0782/19/2 $15.00