Abstract
The tree share structure proposed by Dockins et al. is an elegant model for tracking disjoint ownership in concurrent separation logic, but decision procedures for tree shares are hard to implement due to a lack of a systematic theoretical study. We show that the first-order theory of the full Boolean algebra of tree shares (that is, with all tree-share constants) is decidable and has the same complexity as of the first-order theory of Countable Atomless Boolean Algebras. We prove that combining this additive structure with a constant-restricted unary multiplicative “relativization” operator has a non-elementary lower bound. We examine the consequences of this lower bound and prove that it comes from the combination of both theories by proving an upper bound on a generalization of the restricted multiplicative theory in isolation.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_14
Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)
Appel, A.W., Dockins, R., Hobor, A.: Mechanized semantic library (2009)
Berman, L.: The complexity of logical theories. Theor. Comput. Sci. 11(1), 71–77 (1980)
Blumensath, A.: Automatic structures. Ph.D. thesis, RWTH Aachen (1999)
Blumensath, A., Grade, E.: Finite presentations of infinite structures: automata and interpretations. Theory Comput. Syst. 37, 641–674 (2004)
Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259–270 (2005)
Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 55–72. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44898-5_4
Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)
Colcombet, T., Löding, C.: Transforming structures by set interpretations. Log. Methods Comput. Sci. 3(2) (2007)
Compton, K.J., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. In: APAL (1990)
The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project, version 8.0 (2004)
Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 161–177. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-10672-9_13
Dohrau, J., Summers, A.J., Urban, C., Münger, S., Müller, P.: Permission inference for array programs. In: CAV (2018)
Doko, M., Vafeiadis, V.: Tackling real-life relaxed concurrency with FSL++. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 448–475. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_17
Gherghina, C.A.: Efficiently verifying programs with rich control flows. Ph.D. thesis, National University of Singapore (2012)
Grädel, E.: Simple interpretations among complicated theories. Inf. Process. Lett. 35(5), 235–238 (1990)
Hobor, A., Gherghina, C.: Barriers in concurrent separation logic. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 276–296. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19718-5_15
Hobor, A.: Oracle semantics. Ph.D. thesis, Princeton University, Department of Computer Science, Princeton, NJ, October 2008
Hobor, A., Gherghina, C.: Barriers in concurrent separation logic: now with tool support! Log. Methods Comput. Sci. 8(2) (2012)
Jain, S., Khoussainov, B., Stephan, F., Teng, D., Zou, S.: Semiautomatic structures. In: Hirsch, E.A., Kuznetsov, S.O., Pin, J.É., Vereshchagin, N.K. (eds.) CSR 2014. LNCS, vol. 8476, pp. 204–217. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06686-8_16
Jez, A.: Recompression: a simple and powerful technique for word equations. J. ACM 63(1), 4:1–4:51 (2016)
Klarlund, N., Møller, A.: MONA version 1.4 User Manual. BRICS, Department of Computer Science, Aarhus University, January 2001
Le, D.-K., Chin, W.-N., Teo, Y.M.: Threads as resource for concurrency verification. In: PEPM, pp. 73–84 (2015)
Le, X.B., Gherghina, C., Hobor, A.: Decision procedures over sophisticated fractional permissions. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 368–385. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35182-2_26
Le, X.-B., Hobor, A.: Logical reasoning for disjoint permissions. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 385–414. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_14
Le, X.-B., Hobor, A., Lin, A.W.: Decidability and complexity of tree shares formulas. In: FSTTCS (2016)
Le, X.-B., Nguyen, T.-T., Chin, W.-N., Hobor, A.: A certified decision procedure for tree shares. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 226–242. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68690-5_14
Makanin, G.S.: The problem of solvability of equations in a free semigroup. In: Mat. Sbornik, pp. 147–236 (1977)
Marriott, K., Odersky, M.: Negative Boolean constraints. Theor. Comput. Sci. 160, 365–380 (1996)
O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)
Parkinson, M.: Local reasoning for Java. Ph.D. thesis, University of Cambridge (2005)
Parkinson, M.J., Bornat, R., O’Hearn, P.W.: Modular verification of a non-blocking stack. In: POPL 2007, pp. 297–302 (2007)
Rybina, T., Voronkov, A.: Upper bounds for a theory of queues. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 714–724. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45061-0_56
Stockmeyer, L.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, M.I.T. (1974)
To, A.W.: Model checking infinite-state systems: generic and specific approaches. Ph.D. thesis, LFCS, School of Informatics, University of Edinburgh (2010)
Villard, J.: Heaps and Hops. Ph.D. thesis, Laboratoire Spécification et Vérification, École Normale Supérieure de Cachan, France, February 2011
Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper: automatic verification for fine-grained concurrency. In: ESOP 2017 (2017)
Acknowledgement
We would like to thank anonymous referees for their constructive reviews. Le and Lin are partially supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement no 759969). Le and Hobor are partially supported under Yale-NUS College grant R-607-265-322-121.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
A Appendix
A Appendix
Figure 1 contains the MONA WS2S encoding of the following tree share formula
where lower case letters are for variables of binary strings and upper case letters are for second-order monadic predicates. The last three lines in the code are the formulas with a number of macros defined in the previous lines. Essentially, each tree share is represented by a second-order variable whose elements are antichains that describes a single path to one of its black leaves. Roughly speaking, the \(\texttt {eqt}\) predicate checks whether two tree shares are equal, \(\texttt {leftMul}\) and \(\texttt {rightMul}\) correspond to the multiplicative predicates respectively, and \(\texttt {uniont}\) computes the additive operator \(\oplus \). Other additional predicates are necessary for the consistent representation of the tree shares. In detail, \(\texttt {singleton(X)}\) means that \(\texttt {X}\) has exactly one element, \(\texttt {ant}\) makes sure any two antichains in the same tree are neither prefix of the other, \(\texttt {maxt(X,Y)}\) enforces that \(\texttt {X}\) is the maximal antichain of \(\texttt {Y}\), \(\texttt {roott(x,X)}\) asserts \(\texttt {x}\) is the root of \(\texttt {X}\), \(\texttt {subt}\) is a subset-like relation betweens two trees, while \(\texttt {mint}\) specifies the canonical form. Lastly, we have \(\texttt {sub0}\) and \(\texttt {sub1}\) as the intermediate predicates for the multiplicative predicates.
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Le, XB., Hobor, A., Lin, A.W. (2018). Complexity Analysis of Tree Share Structure. In: Ryu, S. (eds) Programming Languages and Systems. APLAS 2018. Lecture Notes in Computer Science(), vol 11275. Springer, Cham. https://doi.org/10.1007/978-3-030-02768-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-02768-1_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02767-4
Online ISBN: 978-3-030-02768-1
eBook Packages: Computer ScienceComputer Science (R0)