Skip to main content
SpringerLink
Log in

Complexity Analysis of Tree Share Structure

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11275))

Included in the following conference series:

  • 575 Accesses

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 to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. 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

    Chapter  MATH  Google Scholar 

  2. Appel, A.W., et al.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)

    Book  Google Scholar 

  3. Appel, A.W., Dockins, R., Hobor, A.: Mechanized semantic library (2009)

    Google Scholar 

  4. Berman, L.: The complexity of logical theories. Theor. Comput. Sci. 11(1), 71–77 (1980)

    Article  MathSciNet  Google Scholar 

  5. Blumensath, A.: Automatic structures. Ph.D. thesis, RWTH Aachen (1999)

    Google Scholar 

  6. Blumensath, A., Grade, E.: Finite presentations of infinite structures: automata and interpretations. Theory Comput. Syst. 37, 641–674 (2004)

    Article  MathSciNet  Google Scholar 

  7. Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL, pp. 259–270 (2005)

    Google Scholar 

  8. 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

    Chapter  Google Scholar 

  9. Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)

    Article  MathSciNet  Google Scholar 

  10. Colcombet, T., Löding, C.: Transforming structures by set interpretations. Log. Methods Comput. Sci. 3(2) (2007)

    Google Scholar 

  11. Compton, K.J., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. In: APAL (1990)

    Google Scholar 

  12. The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project, version 8.0 (2004)

    Google Scholar 

  13. 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

    Chapter  Google Scholar 

  14. Dohrau, J., Summers, A.J., Urban, C., Münger, S., Müller, P.: Permission inference for array programs. In: CAV (2018)

    Google Scholar 

  15. 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

    Chapter  Google Scholar 

  16. Gherghina, C.A.: Efficiently verifying programs with rich control flows. Ph.D. thesis, National University of Singapore (2012)

    Google Scholar 

  17. Grädel, E.: Simple interpretations among complicated theories. Inf. Process. Lett. 35(5), 235–238 (1990)

    Article  MathSciNet  Google Scholar 

  18. 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

    Chapter  Google Scholar 

  19. Hobor, A.: Oracle semantics. Ph.D. thesis, Princeton University, Department of Computer Science, Princeton, NJ, October 2008

    Google Scholar 

  20. Hobor, A., Gherghina, C.: Barriers in concurrent separation logic: now with tool support! Log. Methods Comput. Sci. 8(2) (2012)

    Google Scholar 

  21. 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

    Chapter  Google Scholar 

  22. Jez, A.: Recompression: a simple and powerful technique for word equations. J. ACM 63(1), 4:1–4:51 (2016)

    Article  MathSciNet  Google Scholar 

  23. Klarlund, N., Møller, A.: MONA version 1.4 User Manual. BRICS, Department of Computer Science, Aarhus University, January 2001

    Google Scholar 

  24. Le, D.-K., Chin, W.-N., Teo, Y.M.: Threads as resource for concurrency verification. In: PEPM, pp. 73–84 (2015)

    Google Scholar 

  25. 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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  27. Le, X.-B., Hobor, A., Lin, A.W.: Decidability and complexity of tree shares formulas. In: FSTTCS (2016)

    Google Scholar 

  28. 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

    Chapter  Google Scholar 

  29. Makanin, G.S.: The problem of solvability of equations in a free semigroup. In: Mat. Sbornik, pp. 147–236 (1977)

    Article  MathSciNet  Google Scholar 

  30. Marriott, K., Odersky, M.: Negative Boolean constraints. Theor. Comput. Sci. 160, 365–380 (1996)

    Article  MathSciNet  Google Scholar 

  31. O’Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375(1–3), 271–307 (2007)

    Article  MathSciNet  Google Scholar 

  32. Parkinson, M.: Local reasoning for Java. Ph.D. thesis, University of Cambridge (2005)

    Google Scholar 

  33. Parkinson, M.J., Bornat, R., O’Hearn, P.W.: Modular verification of a non-blocking stack. In: POPL 2007, pp. 297–302 (2007)

    Article  Google Scholar 

  34. 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

    Chapter  Google Scholar 

  35. Stockmeyer, L.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, M.I.T. (1974)

    Google Scholar 

  36. To, A.W.: Model checking infinite-state systems: generic and specific approaches. Ph.D. thesis, LFCS, School of Informatics, University of Edinburgh (2010)

    Google Scholar 

  37. Villard, J.: Heaps and Hops. Ph.D. thesis, Laboratoire Spécification et Vérification, École Normale Supérieure de Cachan, France, February 2011

    Google Scholar 

  38. Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper: automatic verification for fine-grained concurrency. In: ESOP 2017 (2017)

    Google Scholar 

Download references

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

  1. University of Oxford, Oxford, UK

    Xuan-Bach Le & Anthony W. Lin

  2. Yale-NUS College, Singapore, Singapore

    Aquinas Hobor

  3. National University of Singapore, Singapore, Singapore

    Aquinas Hobor

Authors
  1. Xuan-Bach Le
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aquinas Hobor
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Anthony W. Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Xuan-Bach Le .

Editor information

Editors and Affiliations

  1. Korea Advanced Institute of Science and Technology, Daejeon, Korea (Republic of)

    Sukyoung Ryu

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.

Fig. 1.
figure 1

The transformation of tree share formula in Sect. 5.2 into equivalent WS2S formula.

Full size image

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

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)

Publish with us

Policies and ethics

Search

Navigation