research-article

Open access

Undecidability of Propositional Separation Logic and Its Neighbours

Authors:

James Brotherston,

Max KanovichAuthors Info & Claims

Journal of the ACM (JACM), Volume 61, Issue 2

Article No.: 14, Pages 1 - 43

https://doi.org/10.1145/2542667

Published: 24 April 2014 Publication History

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.

References

[1]

A. Ahmed, L. Jia, and D. Walker. 2003. Reasoning about hierarchical storage. In Proceedings of LICS-18. IEEE Computer Society, 33--44.

Digital Library

[2]

A. V. Aho, J. E. Hopcroft, and J. D. Ullman. 1974. The Design and Analysis of Computer Algorithms. Addison-Wesley.

Digital Library

[3]

G. E. Andrews. 1976. The Theory of partitions. Encyclopedia of Mathematics and Its Applications. Addison-Wesley.

[4]

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.

Digital Library

[5]

J. Berdine, C. Calcagno, and P. O'Hearn. 2004. A decidable fragment of separation logic. In Proceedings of FSTTCS-24. Springer, 97--109.

Digital Library

[6]

R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. 2005. Permission accounting in separation logic. In Proceedings of POPL-32. 59--70.

Digital Library

[7]

J. Brotherston. 2012. Bunched logics displayed. Studia Logica 100, 6, 1223--1254.

Digital Library

[8]

J. Brotherston and C. Calcagno. 2010. Classical BI: Its semantics and proof theory. Logical Meth. Comput. Sci. 6, 3.

[9]

J. Brotherston and M. Kanovich. 2010. Undecidability of propositional separation logic and its neighbours. In Proceedings of LICS-25. IEEE Computer Society, 137--146.

Digital Library

[10]

J. Brotherston and J. Villard. 2014. Parametric completeness for separation theories. In Proceedings of POPL-41. ACM. 453--464.

Digital Library

[11]

C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. 2011. Compositional shape analysis by means of bi-abduction. J. ACM 58, 6.

Digital Library

[12]

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.

Digital Library

[13]

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.

Digital Library

[14]

D. Distefano and M. Parkinson. 2008. jStar: Towards practical verification for Java. In Proceedings of OOPSLA-23. ACM, 213--226.

Digital Library

[15]

M. Dodds, X. Feng, M. Parkinson, and V. Vafeiadis. 2009. Deny-guarantee reasoning. In Proceedings of ESOP-18. Springer, 363--377.

Digital Library

[16]

D. Foulis and M. Bennett. 1994. Effect algebras and unsharp quantum logics. Found. Phys. 24, 1331--1352.

[17]

D. Galmiche and D. Larchey-Wendling. 2006. Expressivity properties of Boolean BI through relational models. In Proceedings of FSTTCS-26. Springer, 357--368.

Digital Library

[18]

D. Galmiche, D. Méry, and D. Pym. 2005. The semantics of BI and resource tableaux. Math. Struct. Comput. Sci. 15, 1033--1088.

Digital Library

[19]

P. Gardner, S. Maffeis, and G. D. Smith. 2012. Towards a program logic for JavaScript. In Proceedings of POPL-39. 31--44.

Digital Library

[20]

J.-Y. Girard and Y. Lafont. 1987. Linear logic and lazy computation. In Proceedings of TAPSOFT'87. Springer-Verlag, 52--66.

Digital Library

[21]

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.

Digital Library

[22]

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.

Digital Library

[23]

E. Jipsen. 1992. Computer aided investigations of relation algebras. Ph.D. dissertation, Vanderbilt University, Nashville, Tennessee.

Digital Library

[24]

M. Kanovich. 1992. Horn programming in linear logic is NP-complete. In Proceedings of LICS-7. IEEE Computer Society, 200--210.

[25]

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.

Digital Library

[26]

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.

[27]

A. Kurucz. 1997. Decision problems in algebraic logic. Ph.D. dissertation, Hungarian Academy of Sciences.

[28]

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.

Digital Library

[29]

D. Larchey-Wendling and D. Galmiche. 2013. Nondeterministic phase semantics and the undecidability of Boolean BI. ACM Trans. Comput. Logic 14, 1, 6.

Digital Library

[30]

M. Minsky. 1967. Computation: Finite and Infinite Machines. Prentice-Hall, Inc.

Digital Library

[31]

T. Murata. 1989. Petri nets: Properties, analysis and applications. Proc. IEEE 77, 4, 541--580.

[32]

P. W. O'Hearn and D. J. Pym. 1999. The logic of bunched implications. Bull. Symb. Logic 5, 2, 215--244.

[33]

M. Parkinson and G. Bierman. 2008. Separation logic, abstraction and inheritance. In Proceedings of POPL-35. ACM, 75--86.

Digital Library

[34]

M. Parkinson, R. Bornat, and C. Calcagno. 2006. Variables as resource in Hoare logics. In Proceedings of LICS-21. IEEE Computer Society, 137--146.

Digital Library

[35]

J. L. Peterson. 1981. Petri Net Theory and the Modeling of Systems. Prentice-Hall.

Digital Library

[36]

D. Pym. 2002. The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logic Series. Kluwer.

[37]

D. Pym, P. O'Hearn, and, H. Yang. 2004. Possible worlds and resources: The semantics of BI. Theoret. Comput. Sci. 315, 1, 257--305.

Digital Library

[38]

J. C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of LICS-17. IEEE Computer Society, 55--74.

Digital Library

[39]

R. Statman. 1979. Intuitionistic propositional logic is polynomial-space complete. Theoret. Comput. Sci. 9, 67--72.

[40]

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.

Digital Library

Cited By

Mulder IKrebbers R(2023)Proof Automation for Linearizability in Separation LogicProceedings of the ACM on Programming Languages10.1145/35860437:OOPSLA1(462-491)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586043
Jipsen PLitak T(2021)An Algebraic Glimpse at Bunched Implications and Separation LogicHiroakira Ono on Substructural Logics10.1007/978-3-030-76920-8_5(185-242)Online publication date: 14-Dec-2021
https://doi.org/10.1007/978-3-030-76920-8_5
Chen XTrinh MRodrigues NPeña LRoşu G(2020)Towards a unified proof framework for automated fixpoint reasoning using matching logicProceedings of the ACM on Programming Languages10.1145/34282294:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428229
Show More Cited By

Index Terms

Undecidability of Propositional Separation Logic and Its Neighbours
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Theorem proving algorithms
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning
      1. Assertions

Recommendations

Undecidability of Propositional Separation Logic and Its Neighbours
LICS '10: Proceedings of the 2010 25th Annual IEEE Symposium on Logic in Computer Science

Separation 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 61, Issue 2

April 2014

206 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/2605175

Issue’s Table of Contents

Copyright © 2014 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: 24 April 2014

Accepted: 01 November 2013

Revised: 01 February 2013

Received: 01 April 2012

Published in JACM Volume 61, Issue 2

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Engineering and Physical Sciences Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
642
Total Downloads

Downloads (Last 12 months)67
Downloads (Last 6 weeks)17

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Mulder IKrebbers R(2023)Proof Automation for Linearizability in Separation LogicProceedings of the ACM on Programming Languages10.1145/35860437:OOPSLA1(462-491)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586043
Jipsen PLitak T(2021)An Algebraic Glimpse at Bunched Implications and Separation LogicHiroakira Ono on Substructural Logics10.1007/978-3-030-76920-8_5(185-242)Online publication date: 14-Dec-2021
https://doi.org/10.1007/978-3-030-76920-8_5
Chen XTrinh MRodrigues NPeña LRoşu G(2020)Towards a unified proof framework for automated fixpoint reasoning using matching logicProceedings of the ACM on Programming Languages10.1145/34282294:OOPSLA(1-29)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428229
Demri SFervari R(2019)The power of modal separation logicsJournal of Logic and Computation10.1093/logcom/exz019Online publication date: 19-Dec-2019
https://doi.org/10.1093/logcom/exz019
Hóu ZClouston RGoré RTiu A(2018)Modular Labelled Sequent Calculi for Abstract Separation LogicsACM Transactions on Computational Logic10.1145/319738319:2(1-35)Online publication date: 28-Apr-2018
https://dl.acm.org/doi/10.1145/3197383
Docherty SPym D(2018)A Stone-type Duality Theorem for Separation Logic Via its Underlying Bunched LogicsElectronic Notes in Theoretical Computer Science10.1016/j.entcs.2018.03.018336(101-118)Online publication date: Apr-2018
https://doi.org/10.1016/j.entcs.2018.03.018
Hóu ZSanán DTiu ALiu Y(2017)Proof Tactics for Assertions in Separation LogicInteractive Theorem Proving10.1007/978-3-319-66107-0_19(285-303)Online publication date: 26-Sep-2017
https://dl.acm.org/doi/10.1007/978-3-319-66107-0_19
Demri SDeters M(2016)Expressive Completeness of Separation Logic with Two Variables and No Separating ConjunctionACM Transactions on Computational Logic10.1145/283549017:2(1-44)Online publication date: 7-Jan-2016
https://dl.acm.org/doi/10.1145/2835490
Hóu ZTiu A(2016)Completeness for a First-Order Abstract Separation LogicProgramming Languages and Systems10.1007/978-3-319-47958-3_23(444-463)Online publication date: 9-Oct-2016
https://doi.org/10.1007/978-3-319-47958-3_23
Demri SDeters M(2015)Two-Variable Separation Logic and Its Inner CircleACM Transactions on Computational Logic10.1145/272471116:2(1-36)Online publication date: 21-Apr-2015
https://dl.acm.org/doi/10.1145/2724711
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

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

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents