Abstract
In this article, we investigate the logical structure of memory models of theoretical and practical interest. Our main interest is in “the logic behind a fixed memory model”, rather than in “a model of any kind behind a given logical system”. As an effective language for reasoning about such memory models, we use the formalism of separation logic. Our main result is that for any concrete choice of heap-like memory model, validity in that model is undecidable even for purely propositional formulas in this language.
The main novelty of our approach to the problem is that we focus on validity in specific, concrete memory models, as opposed to validity in general classes of models.
Besides its intrinsic technical interest, this result also provides new insights into the nature of their decidable fragments. In particular, we show that, in order to obtain such decidable fragments, either the formula language must be severely restricted or the valuations of propositional variables must be constrained.
In addition, we show that a number of propositional systems that approximate separation logic are undecidable as well. In particular, this resolves the open problems of decidability for Boolean BI and Classical BI.
Moreover, we provide one of the simplest undecidable propositional systems currently known in the literature, called “Minimal Boolean BI”, by combining the purely positive implication-conjunction fragment of Boolean logic with the laws of multiplicative *-conjunction, its unit and its adjoint implication, originally provided by intuitionistic multiplicative linear logic. Each of these two components is individually decidable: the implication-conjunction fragment of Boolean logic is co-NP-complete, and intuitionistic multiplicative linear logic is NP-complete.
All of our undecidability results are obtained by means of a direct encoding of Minsky machines.
- A. Ahmed, L. Jia, and D. Walker. 2003. Reasoning about hierarchical storage. In Proceedings of LICS-18. IEEE Computer Society, 33--44. Google ScholarDigital Library
- A. V. Aho, J. E. Hopcroft, and J. D. Ullman. 1974. The Design and Analysis of Computer Algorithms. Addison-Wesley. Google ScholarDigital Library
- G. E. Andrews. 1976. The Theory of partitions. Encyclopedia of Mathematics and Its Applications. Addison-Wesley.Google Scholar
- N. P. Benton, G. M. Bierman, V. de Paiva, and M. Hyland. 1993. A term calculus for intuitionistic linear logic. In Proceedings of TLCA-1. Springer, 75--90. Google ScholarDigital Library
- J. Berdine, C. Calcagno, and P. O'Hearn. 2004. A decidable fragment of separation logic. In Proceedings of FSTTCS-24. Springer, 97--109. Google ScholarDigital Library
- R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. 2005. Permission accounting in separation logic. In Proceedings of POPL-32. 59--70. Google ScholarDigital Library
- J. Brotherston. 2012. Bunched logics displayed. Studia Logica 100, 6, 1223--1254. Google ScholarDigital Library
- J. Brotherston and C. Calcagno. 2010. Classical BI: Its semantics and proof theory. Logical Meth. Comput. Sci. 6, 3.Google ScholarCross Ref
- J. Brotherston and M. Kanovich. 2010. Undecidability of propositional separation logic and its neighbours. In Proceedings of LICS-25. IEEE Computer Society, 137--146. Google ScholarDigital Library
- J. Brotherston and J. Villard. 2014. Parametric completeness for separation theories. In Proceedings of POPL-41. ACM. 453--464. Google ScholarDigital Library
- C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. 2011. Compositional shape analysis by means of bi-abduction. J. ACM 58, 6. Google ScholarDigital Library
- C. Calcagno, P. O'Hearn, and H. Yang. 2007. Local action and abstract separation logic. In Proceedings of LICS-22. IEEE Computer Society, 366--378. Google ScholarDigital Library
- C. Calcagno, H. Yang, and P. W. O'Hearn. 2001. Computability and complexity results for a spatial assertion language for data structures. In Proceedings of FSTTCS-21. Springer, 108--119. Google ScholarDigital Library
- D. Distefano and M. Parkinson. 2008. jStar: Towards practical verification for Java. In Proceedings of OOPSLA-23. ACM, 213--226. Google ScholarDigital Library
- M. Dodds, X. Feng, M. Parkinson, and V. Vafeiadis. 2009. Deny-guarantee reasoning. In Proceedings of ESOP-18. Springer, 363--377. Google ScholarDigital Library
- D. Foulis and M. Bennett. 1994. Effect algebras and unsharp quantum logics. Found. Phys. 24, 1331--1352.Google ScholarCross Ref
- D. Galmiche and D. Larchey-Wendling. 2006. Expressivity properties of Boolean BI through relational models. In Proceedings of FSTTCS-26. Springer, 357--368. Google ScholarDigital Library
- D. Galmiche, D. Méry, and D. Pym. 2005. The semantics of BI and resource tableaux. Math. Struct. Comput. Sci. 15, 1033--1088. Google ScholarDigital Library
- P. Gardner, S. Maffeis, and G. D. Smith. 2012. Towards a program logic for JavaScript. In Proceedings of POPL-39. 31--44. Google ScholarDigital Library
- J.-Y. Girard and Y. Lafont. 1987. Linear logic and lazy computation. In Proceedings of TAPSOFT'87. Springer-Verlag, 52--66. Google ScholarDigital Library
- A. Gotsman, B. Cook, M. Parkinson, and V. Vafeiadis. 2009. Proving that non-blocking algorithms don't block. In Proceedings of POPL-36. ACM, 16--28. Google ScholarDigital Library
- S. Ishtiaq and P. W. O'Hearn. 2001. BI as an assertion language for mutable data structures. In Proceedings of POPL-28. ACM, 14--26. Google ScholarDigital Library
- E. Jipsen. 1992. Computer aided investigations of relation algebras. Ph.D. dissertation, Vanderbilt University, Nashville, Tennessee. Google ScholarDigital Library
- M. Kanovich. 1992. Horn programming in linear logic is NP-complete. In Proceedings of LICS-7. IEEE Computer Society, 200--210.Google ScholarCross Ref
- M. Kanovich. 1995. The direct simulation of Minsky machines in linear logic. In Advances in Linear Logic, London Mathematical Society Lecture Notes Series, vol. 222, Cambridge University Press, 123--145. Google ScholarDigital Library
- A. Kurucz, I. Nemeti, I. Sain, and A. Simon. 1995. Decidable and undecidable modal logics with a binary modality. J. Logic, Lang. Inf. 4, 191--206.Google ScholarCross Ref
- A. Kurucz. 1997. Decision problems in algebraic logic. Ph.D. dissertation, Hungarian Academy of Sciences.Google Scholar
- D. Larchey-Wendling and D. Galmiche. 2010. The undecidability of Boolean BI through phase semantics. In Proceedings of LICS-25. IEEE Computer Society, 140--149. Google ScholarDigital Library
- D. Larchey-Wendling and D. Galmiche. 2013. Nondeterministic phase semantics and the undecidability of Boolean BI. ACM Trans. Comput. Logic 14, 1, 6. Google ScholarDigital Library
- M. Minsky. 1967. Computation: Finite and Infinite Machines. Prentice-Hall, Inc. Google ScholarDigital Library
- T. Murata. 1989. Petri nets: Properties, analysis and applications. Proc. IEEE 77, 4, 541--580.Google ScholarCross Ref
- P. W. O'Hearn and D. J. Pym. 1999. The logic of bunched implications. Bull. Symb. Logic 5, 2, 215--244.Google ScholarCross Ref
- M. Parkinson and G. Bierman. 2008. Separation logic, abstraction and inheritance. In Proceedings of POPL-35. ACM, 75--86. Google ScholarDigital Library
- M. Parkinson, R. Bornat, and C. Calcagno. 2006. Variables as resource in Hoare logics. In Proceedings of LICS-21. IEEE Computer Society, 137--146. Google ScholarDigital Library
- J. L. Peterson. 1981. Petri Net Theory and the Modeling of Systems. Prentice-Hall. Google ScholarDigital Library
- D. Pym. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer.Google Scholar
- D. Pym, P. O'Hearn, and, H. Yang. 2004. Possible worlds and resources: The semantics of BI. Theoret. Comput. Sci. 315, 1, 257--305. Google ScholarDigital Library
- J. C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of LICS-17. IEEE Computer Society, 55--74. Google ScholarDigital Library
- R. Statman. 1979. Intuitionistic propositional logic is polynomial-space complete. Theoret. Comput. Sci. 9, 67--72.Google ScholarCross Ref
- H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. O'Hearn. 2008. Scalable shape analysis for systems code. In Proceedings of CAV-20. Springer, 385--398. Google ScholarDigital Library
Index Terms
- Undecidability of Propositional Separation Logic and Its Neighbours
Recommendations
Undecidability of Propositional Separation Logic and Its Neighbours
LICS '10: Proceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer ScienceSeparation logic has proven an effective formalism for the analysis of memory-manipulating programs. We show that the purely propositional fragment of separation logic is undecidable. In fact, for *any* choice of concrete heap-like model of separation ...
Expressive Completeness of Separation Logic with Two Variables and No Separating Conjunction
Separation logic is used as an assertion language for Hoare-style proof systems about programs with pointers, and there is an ongoing quest for understanding its complexity and expressive power. Herein, we show that first-order separation logic with one ...
A logic of separating modalities
We present a logic of separating modalities, LSM, that is based on Boolean BI. LSM's modalities, which generalize those of S4, combine, within a quite general relational semantics, BI's resource semantics with modal accessibility. We provide a range of ...
Comments