Advertisement

On the Complexity of Linearizability

  • Jad HamzaEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9466)

Abstract

It was shown in Alur et al. [1] that the problem of verifying finite concurrent systems through Linearizability is in \(\mathsf {EXPSPACE}\). However, there was still a complexity gap between the easy to obtain \(\mathsf {PSPACE}\) lower bound and the \(\mathsf {EXPSPACE}\) upper bound. We show in this paper that Linearizability is \(\mathsf {EXPSPACE}\)-complete.

Keywords

Turing Machine Transition Rule Regular Language Method Event Call Event 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Alur, R., McMillan, K.L., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1–2), 167–188 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Verifying concurrent programs against sequential specifications. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 290–309. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  3. 3.
    Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: a complete and automatic linearizability checker. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, pp. 330–340. ACM, New York (2010). http://doi.acm.org/10.1145/1806596.1806634
  4. 4.
    Elmas, T., Qadeer, S., Sezgin, A., Subasi, O., Tasiran, S.: Simplifying linearizability proofs with reduction and abstraction. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 296–311. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  5. 5.
    Filipovic, I., O’Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51–52), 4379–4398 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Fürer, M.: The complexity of the inequivalence problem for regular expressions with intersection. In: de Bakker, J., van Leeuwen, J. (eds.) Automata, Languages and Programming. LNCS, vol. 85, pp. 234–245. Springer, London (1980). http://dl.acm.org/citation.cfm?id=646234.682559 CrossRefGoogle Scholar
  7. 7.
    Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208–1244 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)CrossRefGoogle Scholar
  9. 9.
    Hunt, H.: The equivalence problem for regular expressions with intersection is not polynomial in tape. Department of Computer Science: Technical report, Cornell University, Department of Computer Science (1973). http://books.google.fr/books?id=52j6HAAACAAJ
  10. 10.
    Mayer, A.J., Stockmeyer, L.J.: The complexity of word problems - this time with interleaving. Inf. Comput. 115(2), 293–311 (1994). http://dx.doi.org/10.1006/inco.1994.1098 MathSciNetCrossRefGoogle Scholar
  11. 11.
    Rajamani, S.K., Walker, D. (eds.): Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, 15–17 January 2015. ACM, New York (2015). http://dl.acm.org/citation.cfm?id=2676726
  12. 12.
    Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450–464. Springer, Heidelberg (2010) CrossRefGoogle Scholar
  13. 13.
    Vechev, M., Yahav, E., Yorsh, G.: Experience with model checking linearizability. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 261–278. Springer, Heidelberg (2009) CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.LIAFAUniversité Paris DiderotParisFrance

Personalised recommendations