×

On the almighty wand. (English) Zbl 1262.03051

This paper studies separation logic with one selector. Separation logic is a formalism for reasoning on linked lists. While a list will generally need two selectors, one to point to the next link and one for the data element, separation logic with one selector considers only the next link. Intuitively, in separation logic with one selector one reasons only on the list’s structure and not on the list’s content.
Separation logic with two selectors is known to be undecidable [C. Calcagno et al., Lect. Notes Comput. Sci. 2245, 108–119 (2001; Zbl 1052.68590)]. The authors address decidability, complexity, expressive power and minimality of first-order separation logic with one selector.
Separation logic (SL) is interpreted over a memory state, which represents the memory state of a program manipulating lists. Formally, Loc is a countably infinite set of locations, which represents the set of addresses. The program variables are represented by a countably infinite set of variables Var. A memory state is then a pair \((s,h)\) (store and heap) such that \(s:\mathrm{Var}\to \mathrm{Loc}\) is a total function and \(h:\mathrm{Loc}\rightharpoonup \mathrm{Loc}\) a partial function with finite domain. Intuitively, Var represents the programming variables and \(s\) the variables’ contents. Furthermore, the domain of \(h\) represents the set of addresses of allocated cells, while \(h(l)\) is the value held by the cell at address \(l\).
Two heaps \(h_1, h_2\) are said to be disjoint if their domains are disjoint. In that case \(h_1*h_2\) represents the disjoint union of these two heaps.
Formulas in first-order separation logic with one selector (SL) are built using the Boolean connectors, first-order quantification, equality and three further connectors denoted by \(\hookrightarrow\), \(*\) and \(-\!*\). SL is interpreted on memory states. For instance \((s,h)\) satisfies \(x\hookrightarrow y\) if \(h(s(x))=s(y)\). Furthermore \((s,h)\) satisfies \(\varphi_1*\varphi_2\) if there are two heaps \(h_1\), \(h_2\) such that \(h=h_1*h_2\), \((s,h_1)\models \varphi_1\) and \((s,h_2)\models \varphi_2\) hold. Finally \((s,h)\) satisfies \(\varphi_1-\!*\varphi_2\) if for every heap \(h'\) disjoint from \(h\), if \((s,h')\models \varphi_1\) then \((s,h'*h)\models \varphi_2\). The \(*\) connector is called the separating conjunction, while \(-\!*\) is known as the separating implication and also as the magic wand.
Furthermore, two fragments of SL are also considered: SL(\(*\)) and SL(\(-\!*\)), which are, respectively, the restrictions of SL without \(-\!*\) and without \(*\).
The authors finally consider second-order logic with second-order quantification on Loc. Besides Boolean connectors and first-order quantification, their second-order logic (SO) contains equality and the connective \(\hookrightarrow\). Two restrictions of this logic are considered: MSO, where second-order quantification is restricted to monadic (unary) variables, and DSO, where this quantification is restricted to binary second-order variables.
The major results of this paper are the following. SL’s satisfiability problem is undecidable. Furthermore, there is equivalence in expressive power between SL(\(-\!*\)), SL, SO and DSO by logarithmic-space translations. The authors also show how to adapt their proofs to separation logic with \(k>1\) selectors.
On the other hand, the authors show that for SL(\(*\)) satisfiability is decidable, but with non-elementary recursive complexity (by reduction from the first-order theory of finite words). They furthermore also exhibit larger decidable fragments by restricting the use of \(-\!*\).

MSC:

03B70 Logic in computer science
03B25 Decidability of theories and sets of sentences
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)

Citations:

Zbl 1052.68590

Software:

TVLA
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Antonopoulos, T.; Dawar, A., Separating graph logic from MSO, (FOSSACSʼ09. FOSSACSʼ09, Lecture Notes in Comput. Sci., vol. 5504 (2009), Springer), 63-77 · Zbl 1234.03022
[2] Bansal, K.; Brochenin, R.; Lozes, E., Beyond shapes: Lists with ordered data, (FOSSACSʼ09. FOSSACSʼ09, Lecture Notes in Comput. Sci., vol. 5504 (2009), Springer), 425-439 · Zbl 1234.68083
[3] Berdine, J.; Calcagno, C.; OʼHearn, P., A decidable fragment of separation logic, (FST&TCSʼ04. FST&TCSʼ04, Lecture Notes in Comput. Sci., vol. 3328 (2004), Springer), 97-109 · Zbl 1117.03337
[4] Börger, E.; Grädel, E.; Gurevich, Y., The Classical Decision Problem. Perspectives in Mathematical Logic. (1997), Springer
[5] Bouajjani, A.; Habermehl, P.; Moro, P.; Vojnar, T., Verifying programs with dynamic 1-selector-linked structured in regular model-checking, (TACASʼ05. TACASʼ05, Lecture Notes in Comput. Sci., vol. 3440 (2005), Springer), 13-29 · Zbl 1087.68585
[6] Bozga, M.; Iosif, R.; Lakhnech, Y., On logics of aliasing, (SASʼ04. SASʼ04, Lecture Notes in Comput. Sci., vol. 3148 (2004), Springer), 344-360 · Zbl 1104.68016
[7] Bozga, M.; Iosif, R.; Perarnau, S., Quantitative separation logic and programs with lists, (IJCARʼ08. IJCARʼ08, Lecture Notes in Comput. Sci., vol. 5195 (2008), Springer), 34-49 · Zbl 1165.03329
[8] Brochenin, R.; Demri, S.; Lozes, E., On the almighty wand, (CSLʼ08. CSLʼ08, Lecture Notes in Comput. Sci., vol. 5213 (2008), Springer), 322-337 · Zbl 1157.03010
[9] R. Brochenin, S. Demri, E. Lozes, On the almighty wand, Tech. Rep., LSV, ENS de Cachan, 2008.; R. Brochenin, S. Demri, E. Lozes, On the almighty wand, Tech. Rep., LSV, ENS de Cachan, 2008. · Zbl 1157.03010
[10] Brochenin, R.; Demri, S.; Lozes, E., Reasoning about sequences of memory states, Ann. Pure Appl. Logic, 161, 3, 305-323 (2009) · Zbl 1225.68068
[11] J. Brotherston, M.I. Kanovich, Undecidability of propositional separation logic and its neighbours, in: LICSʼ10, 2010, pp. 130-139.; J. Brotherston, M.I. Kanovich, Undecidability of propositional separation logic and its neighbours, in: LICSʼ10, 2010, pp. 130-139. · Zbl 1295.68166
[12] J. Büchi, On a decision method in restricted second-order arithmetic, in: Logic, Methodology, and Philosophy of Science, 1960, pp. 1-11.; J. Büchi, On a decision method in restricted second-order arithmetic, in: Logic, Methodology, and Philosophy of Science, 1960, pp. 1-11.
[13] C. Calcagno, P. Gardner, U. Zarfaty, Context logic as modal logic: completeness and parametric inexpressivity, in: POPLʼ07, 2007, pp. 123-134.; C. Calcagno, P. Gardner, U. Zarfaty, Context logic as modal logic: completeness and parametric inexpressivity, in: POPLʼ07, 2007, pp. 123-134. · Zbl 1295.68079
[14] C. Calcagno, H. Yang, P. OʼHearn, Computability and complexity results for a spatial assertion language, in: APLASʼ01, 2001, pp. 289-300.; C. Calcagno, H. Yang, P. OʼHearn, Computability and complexity results for a spatial assertion language, in: APLASʼ01, 2001, pp. 289-300.
[15] Calcagno, C.; Yang, H.; OʼHearn, P., Computability and complexity results for a spatial assertion language for data structures, (FST&TCSʼ01. FST&TCSʼ01, Lecture Notes in Comput. Sci., vol. 2245 (2001), Springer), 108-119 · Zbl 1052.68590
[16] Cook, B.; Haase, C.; Ouaknine, J.; Parkinson, M.; Worrell, J., Tractable reasoning in a fragment of separation logic, (CONCURʼ11. CONCURʼ11, Lecture Notes in Comput. Sci., vol. 6901 (2011)), 235-249 · Zbl 1300.03017
[17] Dawar, A.; Gardner, P.; Ghelli, G., Adjunct elimination through games in static ambient logic, (FST&TCSʼ04. FST&TCSʼ04, Lecture Notes in Comput. Sci., vol. 3328 (2004), Springer), 211-223 · Zbl 1117.03338
[18] Dawar, A.; Gardner, P.; Ghelli, G., Expressiveness and complexity of graph logic, Inform. and Comput., 205, 3, 263-310 (2007) · Zbl 1114.03028
[19] Etessami, K.; Vardi, M.; Wilke, T., First-order logic with two variables and unary temporal logic, Inform. and Comput., 179, 2, 279-295 (2002) · Zbl 1096.03013
[20] Galmiche, D.; Méry, D., Tableaux and resource graphs for separation logic, J. Logic Comput., 20, 1, 189-231 (2010) · Zbl 1193.03061
[21] Gorogiannis, N.; Kanovich, M.; OʼHearn, P., The complexity of abduction for separated heap abstractions, (SASʼ11. SASʼ11, Lecture Notes in Comput. Sci., vol. 6887 (2011)), 25-42
[22] S. Ishtiaq, P. OʼHearn, BI as an assertion language for mutable data structures, in: POPLʼ01, 2001, pp. 14-26.; S. Ishtiaq, P. OʼHearn, BI as an assertion language for mutable data structures, in: POPLʼ01, 2001, pp. 14-26. · Zbl 1323.68077
[23] Jensen, J.; Jorgensen, M.; Klarlund, N.; Schwartzbach, M., Automatic verification of pointer programs using monadic second-order logic, (PLDIʼ97 (1997), ACM), 226-236
[24] J. Kamp, Tense logic and the theory of linear order, PhD thesis, UCLA, USA, 1968.; J. Kamp, Tense logic and the theory of linear order, PhD thesis, UCLA, USA, 1968.
[25] Klaedtke, F.; Rueb, H., Monadic second-order logics with cardinalities, (ICALPʼ03. ICALPʼ03, Lecture Notes in Comput. Sci., vol. 2719 (2003), Springer), 681-696 · Zbl 1039.03004
[26] V. Kuncak, M. Rinard, On spatial conjunction as second-order logic, Tech. Rep., MIT CSAIL, October 2004.; V. Kuncak, M. Rinard, On spatial conjunction as second-order logic, Tech. Rep., MIT CSAIL, October 2004. · Zbl 1104.68021
[27] D. Larchey-Wendling, D. Galmiche, The undecidability of Boolean BI through phase semantics, in: LICSʼ10, 2010, pp. 140-149.; D. Larchey-Wendling, D. Galmiche, The undecidability of Boolean BI through phase semantics, in: LICSʼ10, 2010, pp. 140-149. · Zbl 1343.03022
[28] Lev-Ami, T.; Sagiv, M., TVLA: A system for implementing static analyses, (SASʼ00. SASʼ00, Lecture Notes in Comput. Sci., vol. 1824 (2000), Springer), 280-301 · Zbl 0966.68580
[29] Löding, C.; Rohde, P., Model checking and satisfiability for sabotage modal logic, (FST&TCSʼ03. FST&TCSʼ03, Lecture Notes in Comput. Sci., vol. 2914 (2003), Springer), 302-313 · Zbl 1205.68222
[30] E. Lozes, Separation logic preserves the expressive power of classical logic, in: 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACEʼ04), 2004.; E. Lozes, Separation logic preserves the expressive power of classical logic, in: 2nd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACEʼ04), 2004.
[31] Lozes, E., Elimination of spatial connectives in static spatial logics, Theoret. Comput. Sci., 330, 3, 475-499 (2005) · Zbl 1078.68098
[32] Magill, S.; Berdine, J.; Clarke, E.; Cook, B., Arithmetic strengthening for shape analysis, (SASʼ07. SASʼ07, Lecture Notes in Comput. Sci., vol. 4634 (2007), Springer), 419-436 · Zbl 1211.68094
[33] Rabin, M., Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc., 41, 1-35 (1969) · Zbl 0221.02031
[34] Ranise, S.; Zarba, C., A theory of singly-linked lists and its extensible decision procedure, (SEFMʼ06 (2006), IEEE), 206-215
[35] Reynolds, J., Separation logic: a logic for shared mutable data structures, (LICSʼ02 (2002), IEEE), 55-74
[36] L. Stockmeyer, The complexity of decision problems in automata theory and logic, PhD thesis, Department of Electrical Engineering, MIT, 1974.; L. Stockmeyer, The complexity of decision problems in automata theory and logic, PhD thesis, Department of Electrical Engineering, MIT, 1974.
[37] Trakhtenbrot, B., The impossibility of an algorithm for the decision problem for finite models, Dokl. Akad. Nauk SSSR. Dokl. Akad. Nauk SSSR, Amer. Math. Soc. Transl. Ser. 2, 23, 1-6 (1963), English translation in: · Zbl 0121.01507
[38] van Benthem, J., An essay on sabotage and obstruction, (Mechanizing Mathematical Reasoning. Essays in Honor of Jorg Siekmann on the Occasion of his 69th Birthday (2005), Springer-Verlag), 268-276 · Zbl 1098.68632
[39] Yorsh, G.; Rabinovich, A. M.; Sagiv, M.; Meyer, A.; Bouajjani, A., A logic of reachable patterns in linked data structures, (FOSSACSʼ05. FOSSACSʼ05, Lecture Notes in Comput. Sci., vol. 3441 (2005), Springer), 94-110 · Zbl 1180.68131
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.