Advertisement

Verifying Concurrent Data Structures Using Data-Expansion

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

Abstract

We present the first thread modular proof of a concurrent binary search tree. This proof tackles the problem of reasoning about complicated thread interferences using thread modular invariants. The key tool in this proof is the Data-Expansion Lemma, a novel lemma that allows us to reason about search operations in any state. We highlight the power of this lemma when combined with our generalized version of the Hindsight Lemma, which enables us to prove linearizability by reasoning about the temporal properties of the operations instead of reasoning about the linearization points directly.

The Data-Expansion Lemma provides an interesting solution to the proof blowup problem when reasoning about concurrent data structures by separating the verification of effectful and effectless operations. We show that our proof methodology is applicable to several algorithms and argue that many advanced concurrent data structures can be easy to verify using thread-modular arguments.

References

  1. 1.
    Bronson, N.G., Casper, J., Chafi, H., Olukotun, K.: A practical concurrent binary search tree. ACM Sigplan Not. 45, 257–268 (2010)CrossRefGoogle Scholar
  2. 2.
    Brown, T., Ellen, F., Ruppert, E.: A general technique for non-blocking trees. In: Proceedings of the 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2014, pp. 329–342. ACM, New York (2014)Google Scholar
  3. 3.
    Che, T.: Verifying concurrent data structures using data-expansion, Technical report. EPFL (2014)Google Scholar
  4. 4.
    Drachsler, D., Vechev, M., Yahav, E.: Practical concurrent binary search trees via logical ordering. In: Proceedings of the 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2014, pp. 343–356. ACM, New York (2014)Google Scholar
  5. 5.
    Ellen, F., Fatourou, P., Ruppert, E., van Breugel, F.: Non-blocking binary search trees. In: Proceedings of the 29th ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 131–140. ACM (2010)Google Scholar
  6. 6.
    Herlihy, M.P., Lev, Y., Luchangco, V., Shavit, N.N.: A simple optimistic skiplist algorithm. In: Prencipe, G., Zaks, S. (eds.) SIROCCO 2007. LNCS, vol. 4474, pp. 124–138. Springer, Heidelberg (2007) CrossRefGoogle Scholar
  7. 7.
    Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. (TOPLAS) 12(3), 463–492 (1990)CrossRefGoogle Scholar
  8. 8.
    Ishtiaq, S.S., O’Hearn, P.W.: Bi as an assertion language for mutable data structures. ACM SIGPLAN Not. 36, 14–26 (2001)CrossRefzbMATHGoogle Scholar
  9. 9.
    Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)Google Scholar
  10. 10.
    Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, pp. 459–470. ACM, New York (2013)Google Scholar
  11. 11.
    Natarajan, A., Mittal, N.: Fast concurrent lockfree binary search trees. In: Proceedings of the 19th ACM Symposium on Principles and Practice of Parallel Programming (2014)Google Scholar
  12. 12.
    O’Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: Proceedings of the 29th ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 85–94. ACM (2010)Google Scholar
  13. 13.
    Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6(4), 319–340 (1976)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    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

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.École Polytechnique Fédérale de LausanneLausanneSwitzerland

Personalised recommendations