nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Proving Linearizability Using Partial Orders

verfasst von : Artem Khyzha, Mike Dodds, Alexey Gotsman, Matthew Parkinson

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Linearizability is the commonly accepted notion of correctness for concurrent data structures. It requires that any execution of the data structure is justified by a linearization—a linear order on operations satisfying the data structure’s sequential specification. Proving linearizability is often challenging because an operation’s position in the linearization order may depend on future operations. This makes it very difficult to incrementally construct the linearization in a proof.

We propose a new proof method that can handle data structures with such future-dependent linearizations. Our key idea is to incrementally construct not a single linear order of operations, but a partial order that describes multiple linearizations satisfying the sequential specification. This allows decisions about the ordering of operations to be delayed, mirroring the behaviour of data structure implementations. We formalise our method as a program logic based on rely-guarantee reasoning, and demonstrate its effectiveness by verifying several challenging data structures: the Herlihy-Wing queue, the TS queue and the Optimistic set.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

Nächstes Kapitel The Power of Non-determinism in Higher-Order Implicit Complexity

For technical convenience, our notion of a history is different from the one in the classical linearizability definition [11], which uses separate events to denote the start and the end of an operation. We require that \(R\) be an interval order, we ensure that our notion is consistent with an interpretation of events as segments of time during which the corresponding operations are executed, with \(R\) ordering \(i_1\) before \(i_2\) if \(i_1\) finishes before \(i_2\) starts [5].

Recall that the randomness is required to reduce contention.

Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504–528. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14107-2_24CrossRef

Dodds, M., Haas, A., Kirsch, C.M.: A scalable, correct time-stamped stack. In: POPL (2015)

Dongol, B., Derrick, J.: Verifying linearizability: a comparative survey. arXiv CoRR, 1410.6268 (2014)

Filipovic, I., O’Hearn, P.W., Rinetzky, N., Yang, H.: Abstraction for concurrent objects. Theor. Comput. Sci. 411(51–52), 4379–4398 (2010)MathSciNetCrossRef

Fishburn, P.C.: Intransitive indifference with unequal indifference intervals. J. Math. Psychol. 7, 144–149 (1970)MathSciNetCrossRef

Gotsman, A., Yang, H.: Linearizability with ownership transfer. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 256–271. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32940-1_19CrossRef

Haas, A.: Fast concurrent data structures through timestamping. Ph.D. thesis, University of Salzburg (2015)

Heller, S., Herlihy, M., Luchangco, V., Moir, M., Scherer, W.N., Shavit, N.: A lazy concurrent list-based set algorithm. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol. 3974, pp. 3–16. Springer, Heidelberg (2006). doi:10.1007/11795490_3CrossRef

Hemed, N., Rinetzky, N., Vafeiadis, V.: Modular verification of concurrency-aware linearizability. In: Moses, Y. (ed.) DISC 2015. LNCS, vol. 9363, pp. 371–387. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48653-5_25CrossRef

10.

Henzinger, T.A., Sezgin, A., Vafeiadis, V.: Aspect-oriented linearizability proofs. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 242–256. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40184-8_18CrossRef

11.

Herlihy, M., Wing, J.M.: Linearizability: a correctness condition for concurrent objects. In: ACM TOPLAS (1990)

12.

Hoffman, M., Shalev, O., Shavit, N.: The baskets queue. In: Tovar, E., Tsigas, P., Fouchal, H. (eds.) OPODIS 2007. LNCS, vol. 4878, pp. 401–414. Springer, Heidelberg (2007). doi:10.1007/978-3-540-77096-1_29CrossRef

13.

Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress (1983)

14.

Khyzha, A., Dodds, M., Gotsman, A., Parkinson, M.: Proving linearizability using partial orders (extended version). arXiv CoRR, 1701.05463 (2017)

15.

Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: PLDI (2013)

16.

Morrison, A., Afek, Y.: Fast concurrent queues for x86 processors. In: PPoPP (2013)

17.

O’Hearn, P.W., Rinetzky, N., Vechev, M.T., Yahav, E., Yorsh, G.: Verifying linearizability with hindsight. In: PODC (2010)

18.

Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319–340 (1976)MathSciNetCrossRef

19.

Schellhorn, G., Derrick, J., Wehrheim, H.: A sound and complete proof technique for linearizability of concurrent data structures. ACM TOCL 15(4), 31 (2014)MathSciNetCrossRef

20.

Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP (2013)

21.

Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: POPL (2013)

22.

Vafeiadis, V.: Modular fine-grained concurrency verification. Ph.D. thesis, University of Cambridge, UK (2008). Technical report UCAM-CL-TR-726

Titel: Proving Linearizability Using Partial Orders
verfasst von: Artem Khyzha
Mike Dodds
Alexey Gotsman
Matthew Parkinson
Verlag: Springer Berlin Heidelberg
Buch: Programming Languages and Systems
Print ISBN: 978-3-662-54433-4

Electronic ISBN: 978-3-662-54434-1

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-662-54434-1_24

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"