Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Verification, Model Checking, and Abstract Interpretation

VMCAI 2009: Verification, Model Checking, and Abstract Interpretation pp 335–348Cite as

Shape-Value Abstraction for Verifying Linearizability

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5403))

Abstract

This paper presents a novel abstraction for heap-allocated data structures that keeps track of both their shape and their contents. By combining this abstraction with thread-local analysis and rely-guarantee reasoning, we can verify a collection of fine-grained blocking and non-blocking concurrent algorithms for an arbitrary (unbounded) number of threads. We prove that these algorithms are linearizable, namely equivalent (modulo termination) to their sequential counterparts.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Herlihy, M.P., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. ACM Trans. on Program. Languages and Systems 12(3), 463–492 (1990)

    Article  Google Scholar 

  2. Doherty, S., Groves, L., Luchangco, V., Moir, M.: Formal verification of a practical lock-free queue algorithm. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 97–114. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free dynamic hash tables with open addressing. Distributed Computing 18(1), 21–42 (2005)

    Article  MATH  Google Scholar 

  4. Colvin, R., Groves, L., Luchangco, V., Moir, M.: Formal verification of a lazy concurrent list-based set. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 473–488. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Vafeiadis, V., Herlihy, M., Hoare, T., Shapiro, M.: Proving correctness of highly-concurrent linearisable objects. In: PPoPP 2006, pp. 129–136. ACM Press, New York (2006)

    Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. Manevich, R., Lev-Ami, T., Ramalingam, G., Sagiv, M., Berdine, J.: Heap decomposition for concurrent shape analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 363–377. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

  9. Vafeiadis, V., Parkinson, M.: A marriage of rely/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)

    Google Scholar 

  11. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE Computer Society, Los Alamitos (2002)

    Google Scholar 

  12. Treiber, R.K.: Systems programming: Coping with parallelism. Technical Report RJ5118, IBM Almaden Res. Ctr. (1986)

    Google Scholar 

  13. Vafeiadis, V.: Fine-grained concurrency verification. Ph.D. dissertation, University of Cambridge (2007); Also available as Technical Report UCAM-CL-TR-726

    Google Scholar 

  14. Calcagno, C., Parkinson, M., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233–248. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  16. Michael, M., Scott, M.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC, pp. 267–275. ACM Press, New York (1996)

    Google Scholar 

  17. Harris, T.L., Fraser, K., Pratt, I.A.: A practical multi-word compare-and-swap operation. In: Malkhi, D. (ed.) DISC 2002. LNCS, vol. 2508, pp. 265–279. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  18. Wang, L., Stoller, S.D.: Static analysis of atomicity for programs with non-blocking synchronization. In: PPoPP 2005, pp. 61–71. ACM Press, New York (2005)

    Google Scholar 

  19. Yahav, E., Sagiv, M.: Automatically verifying concurrent queue algorithms. Electronic Notes in Theoretical Computer Science 89(3) (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research, Cambridge, UK

    Viktor Vafeiadis

Authors
  1. Viktor Vafeiadis
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. (Emeritus University of Copenhagen), Bukkeballevej 88, 2960, Rungsted, Denmark

    Neil D. Jones

  2. Institut für Informatik, Fachbereich Mathematik und Informatik, Westfälische Wilhelms-Universität, 48149, Münster, Germany

    Markus Müller-Olm

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vafeiadis, V. (2008). Shape-Value Abstraction for Verifying Linearizability. In: Jones, N.D., Müller-Olm, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2009. Lecture Notes in Computer Science, vol 5403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-93900-9_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-93900-9_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-93899-6

  • Online ISBN: 978-3-540-93900-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation