Advertisement

Abstract

Linearizability is a well-established consistency and correctness criterion for concurrent data types. An important feature of linearizability is Herlihy and Wing’s locality principle, which says that a concurrent system is linearizable if and only if all of its constituent parts (so-called objects) are linearizable. This paper presents P-compositionality, which generalizes the idea behind the locality principle to operations on the same concurrent data type. We implement P-compositionality in a novel linearizability checker. Our experiments with over nine implementations of concurrent sets, including Intel’s TBB library, show that our linearizability checker is one order of magnitude faster and/or more space efficient than the state-of-the-art algorithm.

Keywords

Model Check Decision Procedure Concurrent System Locality Principle Sequential History 
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.
    Herlihy, M.P., Wing, J.M.: Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12(3), 463–492 (1990)CrossRefGoogle Scholar
  2. 2.
    Gilbert, S., Lynch, N.: Brewer’s conjecture and the feasibility of consistent, available, partition-tolerant web services. SIGACT News 33(2), 51–59 (2002)CrossRefGoogle Scholar
  3. 3.
    Gibbons, P.B., Korach, E.: Testing shared memories. SIAM J. Comput. 26(4), 1208–1244 (1997)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Wing, J.M., Gong, C.: Testing and verifying concurrent objects. J. Parallel Distrib. Comput. 17(1-2), 164–182 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  5. 5.
    Lowe, G.: Testing for linearizability. In: PODC 2015 (2015) (Under submission), http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/
  6. 6.
    Bouajjani, A., Emmi, M., Enea, C., Hamza, J.: Tractable refinement checking for concurrent objects. In: POPL 2015, pp. 651–662. ACM (2015)Google Scholar
  7. 7.
    Rabinovitch, I.: The dimension of semiorders. Journal of Combinatorial Theory, Series A 25(1), 50–61 (1978)CrossRefzbMATHMathSciNetGoogle Scholar
  8. 8.
    Okasaki, C.: Purely Functional Data Structures. Cambridge University Press (1998)Google Scholar
  9. 9.
    Kingsbury, K.: Computational techniques in Knossos (May 2014), https://aphyr.com/posts/314-computational-techniques-in-knossos
  10. 10.
    ISO: International Standard ISO/IEC 14882:2011(E) Programming Language C++. International Organization for Standardization (2011)Google Scholar
  11. 11.
    Aiyer, A., Alvisi, L., Bazzi, R.A.: On the availability of non-strict quorum systems. In: Fraigniaud, P. (ed.) DISC 2005. LNCS, vol. 3724, pp. 48–62. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  12. 12.
    Wang, L., Stoller, S.D.: Static analysis of atomicity for programs with non-blocking synchronization. In: PPoPP 2005, pp. 61–71. ACM (2005)Google Scholar
  13. 13.
    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
  14. 14.
    Alur, R., McMillan, K., Peled, D.: Model-checking of correctness conditions for concurrent objects. Inf. Comput. 160(1-2), 167–188 (2000)CrossRefzbMATHMathSciNetGoogle Scholar
  15. 15.
    Colvin, R., Doherty, S., Groves, L.: Verifying concurrent data structures by simulation. Electron. Notes Theor. Comput. Sci. 137(2), 93–110 (2005)CrossRefGoogle Scholar
  16. 16.
    Derrick, J., Schellhorn, G., Wehrheim, H.: Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33(1), 4:1–4:43 (2011)Google Scholar
  17. 17.
    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
  18. 18.
    Burckhardt, S., Dern, C., Musuvathi, M., Tan, R.: Line-up: A complete and automatic linearizability checker. SIGPLAN Not. 45(6), 330–340 (2010)CrossRefGoogle Scholar
  19. 19.
    Černý, P., Radhakrishna, A., Zufferey, D., Chaudhuri, S., Alur, R.: Model checking of linearizability of concurrent list implementations. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 465–479. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  20. 20.
    Liu, Y., Chen, W., Liu, Y.A., Sun, J., Zhang, S.J., Dong, J.S.: Verifying linearizability via optimized refinement checking. IEEE Trans. Softw. Eng. 39(7), 1018–1039 (2013)CrossRefGoogle Scholar
  21. 21.
    Amit, D., Rinetzky, N., Reps, T., Sagiv, M., Yahav, E.: Comparison under abstraction for verifying linearizability. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 477–490. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  22. 22.
    Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread quantification for concurrent shape analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 399–413. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  23. 23.
    Vafeiadis, V.: Shape-value abstraction for verifying linearizability. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 335–348. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  24. 24.
    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
  25. 25.
    Anderson, E., Li, X., Shah, M.A., Tucek, J., Wylie, J.J.: What consistency does your key-value store actually provide? In: HotDep 2010, pp. 1–16. USENIX Association (2010)Google Scholar
  26. 26.
    Shacham, O., Bronson, N., Aiken, A., Sagiv, M., Vechev, M., Yahav, E.: Testing atomicity of composed concurrent operations. SIGPLAN Not. 46(10), 51–64 (2011)CrossRefGoogle Scholar
  27. 27.
    Fonseca, P., Li, C., Rodrigues, R.: Finding complex concurrency bugs in large multi-threaded applications. In: EuroSys 2011, pp. 215–228. ACM (2011)Google Scholar
  28. 28.
    Pradel, M., Gross, T.R.: Fully automatic and precise detection of thread safety violations. SIGPLAN Not. 47(6), 521–530 (2012)Google Scholar
  29. 29.
    Pradel, M., Gross, T.R.: Automatic testing of sequential and concurrent substitutability. In: ICSE 2013, pp. 282–291. IEEE Press (2013)Google Scholar
  30. 30.
    Golab, W., Hurwitz, J., Li, X.S.: On the k-atomicity-verification problem. In: ICDCS 2013, pp. 591–600. IEEE Computer Society (2013)Google Scholar
  31. 31.
    Elmas, T., Tasiran, S., Qadeer, S.: VYRD: Verifying concurrent programs by runtime refinement-violation detection. SIGPLAN Not. 40(6), 27–37 (2005)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2015

Authors and Affiliations

  1. 1.University of OxfordOxfordUK

Personalised recommendations