survey

Verifying Linearisability: A Comparative Survey

Authors:
Brijesh Dongol

Brunel University London, UK

Brunel University London, UK
View Profile

,
John Derrick

University of Sheffield, UK

University of Sheffield, UK
View Profile

Authors Info & Claims

ACM Computing Surveys Volume 48 Issue 2Article No.: 19pp 1–43https://doi.org/10.1145/2796550

Published:24 September 2015Publication History

ACM Computing Surveys

Abstract

Linearisability is a key correctness criterion for concurrent data structures, ensuring that each history of the concurrent object under consideration is consistent with respect to a history of the corresponding abstract data structure. Linearisability allows concurrent (i.e., overlapping) operation calls to take effect in any order, but requires the real-time order of nonoverlapping to be preserved. The sophisticated nature of concurrent objects means that linearisability is difficult to judge, and hence, over the years, numerous techniques for verifying lineasizability have been developed using a variety of formal foundations such as data refinement, shape analysis, reduction, etc. However, because the underlying framework, nomenclature, and terminology for each method is different, it has become difficult for practitioners to evaluate the differences between each approach, and hence, evaluate the methodology most appropriate for verifying the data structure at hand. In this article, we compare the major of methods for verifying linearisability, describe the main contribution of each method, and compare their advantages and limitations.

References

M. Abadi and L. Lamport. 1991. The existence of refinement mappings. Theor. Comput. Sci. 82, 2 (1991), 253--284. Google ScholarDigital Library
J.-R. Abrial. 2010. Modeling in Event-B—System and Software Engineering. Cambridge University Press. I--XXVI, 1--586 pages. Google ScholarDigital Library
J.-R. Abrial and D. Cansell. 2005. Formal construction of a non-blocking concurrent queue algorithm. J. Univ. Comput. Sci. 11, 5 (May 2005), 744--770.Google Scholar
S. V. Adve and K. Gharachorloo. 1996. Shared memory consistency models: A tutorial. IEEE Comp. 29, 12 (1996), 66--76. Google ScholarDigital Library
Y. Afek, G. Korland, and E. Yanovsky. 2010. Quasi-linearizability: Relaxed consistency for improved concurrency. In OPODIS (LNCS), C. Lu, T. Masuzawa, and M. Mosbah (Eds.), Vol. 6490. Springer, 395--410. Google ScholarDigital Library
D. Amit, N. Rinetzky, T. W. Reps, M. Sagiv, and E. Yahav. 2007. Comparison under abstraction for verifying linearizability. In CAV (LNCS), W. Damm and H. Hermanns (Eds.), Vol. 4590. Springer, 477--490. Google ScholarDigital Library
S. Bäumler, M. Balser, F. Nafz, W. Reif, and G. Schellhorn. 2010. Interactive verification of concurrent systems using symbolic execution. AI Commun. 23, 2--3 (2010), 285--307. Google ScholarDigital Library
S. Bäumler, G. Schellhorn, B. Tofan, and W. Reif. 2011. Proving linearizability with temporal logic. Formal Asp. Comput. 23, 1 (2011), 91--112. Google ScholarCross Ref
K. P. Birman. 1992. Maintaining consistency in distributed systems. In Proceedings of the 5th ACM SIGOPS European Workshop: MPDSS (EW 5). ACM, New York, 1--6. Google ScholarDigital Library
J. P. Bowen. 1996. Formal Specification and Documentation Using Z: A Case Study Approach. International Thomson Computer Press.Google Scholar
R. M. Burstall. 1974. Program proving as hand simulation with a little induction. In IFIP Congress. 308--312.Google Scholar
A. Cerone, A. Gotsman, and H. Yang. 2014. Parameterised linearisability. In ICALP (2) (LNCS), J. Esparza, P. Fraigniaud, T. Husfeldt, and E. Koutsoupias (Eds.), Vol. 8573. Springer, 98--109.Google Scholar
B. Chatterjee, N. Nguyen Dang, and P. Tsigas. 2014. Efficient lock-free binary search trees. In PODC, M. M. Halldórsson and S. Dolev (Eds.). ACM, 322--331. Google ScholarDigital Library
R. Colvin, S. Doherty, and L. Groves. 2005. Verifying concurrent data structures by simulation. Electr. Notes Theor. Comput. Sci. 137, 2 (2005), 93--110. Google ScholarDigital Library
R. Colvin and L. Groves. 2005. Formal verification of an array-based nonblocking queue. In ICECCS (June 2005). IEEE Computer Society, 507--516. Google ScholarDigital Library
R. Colvin, L. Groves, V. Luchangco, and M. Moir. 2006a. Formal verification of a lazy concurrent list-based set algorithm. In CAV (LNCS), T. Ball and R. B. Jones (Eds.), Vol. 4144. Springer, 475--488. Google ScholarDigital Library
R. Colvin, L. Groves, V. Luchangco, and M. Moir. 2006b. PVS proofs for Lazy Set Algorithm. (2006). http://www.mcs.vuw.ac.nz/research/SunVUW/LazyListFiles/.Google Scholar
W. P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. 2001. Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge University Press. Google ScholarDigital Library
W. P. de Roever and K. Engelhardt. 1996. Data Refinement: Model-Oriented Proof Methods and Their Comparison. Number 47 in Cambridge Tracts in Theor. Comp. Sci. Cambridge University Press.Google Scholar
J. Derrick, B. Dongol, G. Schellhorn, B. Tofan, O. Travkin, and H. Wehrheim. 2014. Quiescent consistency: Defining and verifying relaxed linearizability. In FM (LNCS), C. B. Jones, P. Pihlajasaari, and J. Sun (Eds.), Vol. 8442. Springer, 200--214.Google Scholar
J. Derrick, G. Schellhorn, and H. Wehrheim. 2011a. Mechanically verified proof obligations for linearizability. ACM Trans. Program. Lang. Syst. 33, 1 (2011), 4. Google ScholarDigital Library
J. Derrick, G. Schellhorn, and H. Wehrheim. 2011b. Verifying linearisability with potential linearisation points. In FM (LNCS), M. Butler and W. Schulte (Eds.), Vol. 6664. Springer, 323--337. Google ScholarDigital Library
J. Derrick and H. Wehrheim. 2003. Using coupled simulations in non-atomic refinement. In ZB 2003: Formal Specification and Development in Z and B (LNCS). Springer, 127--147. Google ScholarDigital Library
J. Derrick and H. Wehrheim. 2005. Non-atomic refinement in Z and CSP. In ZB (LNCS), H. Treharne, S. King, M. C. Henson, and S. A. Schneider (Eds.), Vol. 3455. Springer, 24--44. Google ScholarDigital Library
S. Doherty. 2003. Modelling and Verifying Non-Blocking Algorithms That Use Dynamically Allocated Memory. Master’s thesis. Victoria University of Wellington.Google Scholar
S. Doherty, D. Detlefs, L. Groves, C. H. Flood, V. Luchangco, P. A. Martin, M. Moir, N. Shavit, and G. Steel. 2004a. DCAS is not a silver bullet for nonblocking algorithm design. In SPAA. 216--294. Google ScholarDigital Library
S. Doherty, L. Groves, V. Luchangco, and M. Moir. 2004b. Formal verification of a practical lock-free queue algorithm. In FORTE (LNCS), D. de Frutos-Escrig and M. Núñez (Eds.), Vol. 3235. Springer, 97--114.Google Scholar
B. Dongol. 2006. Formalising progress properties of non-blocking programs. In ICFEM (LNCS), Z. Liu and J. He (Eds.), Vol. 4260. Springer, 284--303. Google ScholarDigital Library
B. Dongol. 2009. Progress-Based Verification and Derivation of Concurrent Programs. Ph.D. Dissertation. The University of Queensland.Google Scholar
B. Dongol and J. Derrick. 2013. Simplifying proofs of linearisability using layers of abstraction. ECEASST 66 (2013).Google Scholar
B. Dongol, J. Derrick, L. Groves, and G. Smith. 2015. Defining correctness conditions for concurrent objects in multicore architectures. In ECOOP (LIPIcs), J. T. Boyland (Ed.), Vol. 37. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 470--494. DOI:http://dx.doi.org/10.4230/LIPIcs.ECOOP.2015.470Google Scholar
C. Dragoi, A. Gupta, and T. A. Henzinger. 2013. Automatic linearizability proofs of concurrent objects with cooperating updates. In CAV (LNCS), N. Sharygina and H. Veith (Eds.), Vol. 8044. Springer, 174--190. Google ScholarDigital Library
R. Drexler, W. Reif, G. Schellhorn, K. Stenzel, W. Stephan, and A. Wolpers. 1993. The KIV system: A tool for formal program development. In STACS (LNCS), P. Enjalbert, A. Finkel, and K. W. Wagner (Eds.), Vol. 665. 704--705. Google ScholarDigital Library
T. Elmas. 2010. QED: A proof system based on reduction and abstraction for the static verification of concurrent software. In ICSE (2), J. Kramer, J. Bishop, P. T. Devanbu, and S. Uchitel (Eds.). ACM, 507--508. Google ScholarDigital Library
T. Elmas, S. Qadeer, A. Sezgin, O. Subasi, and S. Tasiran. 2010. Simplifying linearizability proofs with reduction and abstraction. In TACAS (LNCS), J. Esparza and R. Majumdar (Eds.), Vol. 6015. Springer, 296--311. Google ScholarDigital Library
T. Elmas, S. Qadeer, and S. Tasiran. 2009. A calculus of atomic actions. In POPL, Z. Shao and B. C. Pierce (Eds.). ACM, 2--15. Google ScholarDigital Library
I. Filipović, P. W. O’Hearn, N. Rinetzky, and H. Yang. 2010. Abstraction for concurrent objects. Theor. Comput. Sci. 411, 51--52 (2010), 4379--4398. Google ScholarDigital Library
K. Fraser and T. L. Harris. 2007. Concurrent programming without locks. ACM Trans. Comput. Syst. 25, 2 (2007). Google ScholarDigital Library
D. Friggens. 2013. On the Use of Model Checking for the Bounded and Unbounded Verification of NonBlocking Concurrent Data Structures. Ph.D. Dissertation. Victoria University of Wellington. http://hdl.handle.net/10063/2702.Google Scholar
H. Gao, Y. Fu, and W. H. Hesselink. 2009. Verification of a lock-free implementation of multiword LL/SC object. In DASC. IEEE, 31--36. Google ScholarDigital Library
H. Gao, J. F. Groote, and W. H. Hesselink. 2005. Lock-free dynamic hash tables with open addressing. Distrib. Comput. 18, 1 (2005), 21--42. Google ScholarDigital Library
H. Gao, J. F. Groote, and W. H. Hesselink. 2007. Lock-free parallel and concurrent garbage collection by mark&sweep. Sci. Comput. Program. 64, 3 (2007), 341--374. Google ScholarDigital Library
H. Gao and W. H. Hesselink. 2007. A general lock-free algorithm using compare-and-swap. Inf. Comput. 205, 2 (2007), 225--241. Google ScholarDigital Library
P. H. B. Gardiner and C. Morgan. 1993. A single complete rule for data refinement. Form. Asp. Comput. 5, 4 (1993), 367--382.Google ScholarDigital Library
A. Gotsman, B. Cook, M. J. Parkinson, and V. Vafeiadis. 2009. Proving that non-blocking algorithms don’t block. In POPL, Z. Shao and B. C. Pierce (Eds.). ACM, 16--28. DOI:http://dx.doi.org/10.1145/1480881.1480886 Google ScholarDigital Library
A. Gotsman and H. Yang. 2012. Linearizability with ownership transfer. In CONCUR (LNCS), M. Koutny and I. Ulidowski (Eds.), Vol. 7454. Springer, 256--271. Google ScholarDigital Library
A. Gotsman and H. Yang. 2013. Linearizability with ownership transfer. Log. Meth. Comput. Sci. 9, 3 (2013).Google Scholar
L. Groves. 2007. Reasoning about nonblocking concurrency using reduction. In ICECCS. IEEE Comp. Soc., 107--116. Google ScholarDigital Library
L. Groves. 2008a. Trace-based derivation of a lock-free queue algorithm. Electron. Notes Theor. Comput. Sci. 201 (2008), 69--98. Google ScholarDigital Library
L. Groves. 2008b. Verifying Michael and Scott’s lock-free queue algorithm using trace reduction. In CATS (CRPIT), J. Harland and P. Manyem (Eds.), Vol. 77. 133--142. Google ScholarDigital Library
L. Groves. 2009. Reasoning about nonblocking concurrency. JUCS 15, 1 (Jan. 2009), 72--111.Google Scholar
L. Groves and R. Colvin. 2007. Derivation of a scalable lock-free stack algorithm. Electron. Notes Theor. Comput. Sci. 187 (2007), 55--74. Google ScholarDigital Library
L. Groves and R. Colvin. 2009. Trace-based derivation of a scalable lock-free stack algorithm. Formal Asp. Comput. 21, 1--2 (2009), 187--223. Google ScholarCross Ref
R. Guerraoui and A. Schiper. 1996. Fault-tolerance by replication in distributed systems. In Reliable Software Technologies Ada-Europe ’96, Al. Strohmeier (Ed.). LNCS, Vol. 1088. Springer, 38--57. Google ScholarDigital Library
T. L. Harris. 2001. A pragmatic implementation of non-blocking linked-lists. In DISC (LNCS), J. L. Welch (Ed.), Vol. 2180. Springer, 300--314. Google ScholarDigital Library
T. L. Harris, K. Fraser, and I. A. Pratt. 2002. A practical multi-word compare-and-swap operation. In DISC (LNCS), D. Malkhi (Ed.), Vol. 2508. Springer, 265--279. Google ScholarDigital Library
I. J. Hayes, A. Burns, B. Dongol, and C. B. Jones. 2013. Comparing degrees of non-determinism in expression evaluation. Comput. J. 56, 6 (2013), 741--755. Google ScholarDigital Library
S. Heller, M. Herlihy, V. Luchangco, M. Moir, W. N. Scherer III, and N. Shavit. 2007. A lazy concurrent list-based set algorithm. Parallel Process. Lett. 17, 4 (2007), 411--424.Google ScholarCross Ref
D. Hendler, N. Shavit, and L. Yerushalmi. 2010. A scalable lock-free stack algorithm. J. Parallel Distrib. Comput. 70, 1 (2010), 1--12. Google ScholarDigital Library
T. A. Henzinger, C. M. Kirsch, H. Payer, A. Sezgin, and A. Sokolova. 2013a. Quantitative relaxation of concurrent data structures. In POPL, R. Giacobazzi and R. Cousot (Eds.). ACM, 317--328. Google ScholarDigital Library
T. A. Henzinger, A. Sezgin, and V. Vafeiadis. 2013b. Aspect-oriented linearizability proofs. In CONCUR (LNCS), P. R. D’Argenio and H. C. Melgratti (Eds.), Vol. 8052. Springer, 242--256. Google ScholarDigital Library
M. Herlihy and N. Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann. I--XX, 1--508 pages. Google ScholarDigital Library
M. Herlihy and N. Shavit. 2011. On the nature of progress. In OPODIS (LNCS), A. Fernández Anta, G. Lipari, and M. Roy (Eds.), Vol. 7109. Springer, 313--328. Google ScholarDigital Library
M. P. Herlihy and J. M. Wing. 1990. Linearizability: A correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463--492. Google ScholarDigital Library
R. Jagadeesan and J. Riely. 2014. Between linearizability and quiescent consistency—Quantitative quiescent consistency. In ICALP (LNCS), J. Esparza, P. Fraigniaud, T. Husfeldt, and E. Koutsoupias (Eds.), Vol. 8573. Springer, 220--231.Google Scholar
C. B. Jones. 1983. Tentative steps toward a development method for interfering programs. ACM Trans. Prog. Lang. Syst. 5, 4 (1983), 596--619. Google ScholarDigital Library
N. D. Jones and S. S. Muchnick. 1982. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In POPL, R. A. DeMillo (Ed.). ACM Press, 66--74. Google ScholarDigital Library
B. Jonsson. 2012. Using refinement calculus techniques to prove linearizability. Formal Asp. Comput. 24, 4--6 (2012), 537--554. Google ScholarCross Ref
L. Lamport. 1997. How to make a correct multiprocess program execute correctly on a multiprocessor. IEEE Trans. Comput. 46, 7 (1997), 779--782. Google ScholarDigital Library
H. Liang and X. Feng. 2013a. Modular Verification of Linearizability with Non-Fixed Linearization Points. Technical Report. USTC. http://kyhcs.ustcsz.edu.cn/relconcur/lin.Google Scholar
H. Liang and X. Feng. 2013b. Modular verification of linearizability with non-fixed linearization points. In PLDI, H.-J. Boehm and C. Flanagan (Eds.). ACM, 459--470. Google ScholarDigital Library
H. Liang, X. Feng, and M. Fu. 2012. A rely-guarantee-based simulation for verifying concurrent program transformations. In POPL, J. Field and M. Hicks (Eds.). ACM, 455--468. Google ScholarDigital Library
H. Liang, J. Hoffmann, X. Feng, and Z. Shao. 2013. Characterizing progress properties of concurrent objects via contextual refinements. In CONCUR (LNCS), P. R. D’Argenio and H. C. Melgratti (Eds.), Vol. 8052. Springer, 227--241. DOI:http://dx.doi.org/10.1007/978-3-642-40184-8_17 Google ScholarDigital Library
R. J. Lipton. 1975. Reduction: A method of proving properties of parallel programs. Commun. ACM 18, 12 (1975), 717--721. Google ScholarDigital Library
Y. Liu, W. Chen, Y. A. Liu, and J. Sun. 2009. Model checking linearizability via refinement. In FM (LNCS), A. Cavalcanti and D. Dams (Eds.), Vol. 5850. Springer, 321--337. Google ScholarDigital Library
Y. Liu, W. Chen, Y. A. Liu, J. Sun, S. J. Zhang, and J. Song Dong. 2013. Verifying linearizability via optimized refinement checking. IEEE Trans. Softw. Eng. 39, 7 (2013), 1018--1039. Google ScholarDigital Library
N. Lynch and M. Tuttle. 1989. An introduction to input/output automata. CWI-Quarterly 2, 3 (1989), 219--246.Google Scholar
N. A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann. Google ScholarDigital Library
N. A. Lynch and F. W. Vaandrager. 1995. Forward and backward simulations: I. Untimed systems. Inf. Comput. 121, 2 (1995), 214--233. DOI:http://dx.doi.org/10.1006/inco.1995.1134 Google ScholarDigital Library
H. Massalin and C. Pu. 1992. A lock-free multiprocessor os kernel (abstract). Op. Syst. Rev. 26, 2 (1992), 8. Google ScholarCross Ref
M. Michael and M. L. Scott. 1996. Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In PODC. 267--275. Google ScholarDigital Library
M. M. Michael. 2002. High performance dynamic lock-free hash tables and list-based sets. In SPAA. 73--82. Google ScholarDigital Library
M. Moir, D. Nussbaum, O. Shalev, and N. Shavit. 2005. Using elimination to implement scalable and lock-free FIFO queues. In SPAA, P. B. Gibbons and P. G. Spirakis (Eds.). ACM, 253--262. Google ScholarDigital Library
M. Moir and N. Shavit. 2007. Concurrent data structures. In Handbook of Data Structures and Applications, D. Metha and S. Sahni (Eds.), 47--14--47-30. Chapman and Hall/CRC Press.Google Scholar
C. Morgan and T. Vickers. 1992. On the Refinement Calculus. Springer-Verlag. Google ScholarDigital Library
B. C. Moszkowski. 1997. Compositional reasoning using interval temporal logic and tempura. In COMPOS (LNCS), W. P. de Roever, H. Langmaack, and A. Pnueli (Eds.), Vol. 1536. Springer, 439--464. Google ScholarDigital Library
B. C. Moszkowski. 2000. A complete axiomatization of interval temporal logic with infinite time. In LICS. 241--252. Google ScholarDigital Library
P. W. O’Hearn, J. C. Reynolds, and H. Yang. 2001. Local reasoning about programs that alter data structures. In CSL (LNCS), L. Fribourg (Ed.), Vol. 2142. Springer, 1--19. Google ScholarDigital Library
P. W. O’Hearn, N. Rinetzky, M. T. Vechev, E. Yahav, and G. Yorsh. 2010a. Verifying linearizability with hindsight. In PODC, A. W. Richa and R. Guerraoui (Eds.). ACM, 85--94. Google ScholarDigital Library
P. W. O’Hearn, N. Rinetzky, M. T. Vechev, E. Yahav, and G. Yorsh. 2010b. Verifying Linearizability With Hindsight. Technical Report. Queen Mary University of London.Google Scholar
R. Oshman and N. Shavit. 2013. The skiptrie: Low-depth concurrent search without rebalancing. In PODC, P. Fatourou and G. Taubenfeld (Eds.). ACM, 23--32. Google ScholarDigital Library
S. S. Owicki and D. Gries. 1976. An axiomatic proof technique for parallel programs I. Acta Inf. 6 (1976), 319--340. Google ScholarDigital Library
S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. 1996. PVS: Combining specification, proof checking, and model checking. In CAV, R. Alur and T. A. Henzinger (Eds.), Vol. 1102. Springer, 411--414. Google ScholarDigital Library
F. Pacull and A. Sandoz. 1993. R-linearizability: An extension of linearizability to replicated objects. In 4th Workshop on Future Trends of Distributed Computing Systems. 347--353.Google Scholar
K. Ramamritham and P. K. Chrysanthis. 1992. In search of acceptability citeria: Database consistency requirements and transaction correctness properties. In IWDOM, M. T. Özsu, U. Dayal, and P. Valduriez (Eds.). Morgan Kaufmann, 212--230.Google Scholar
M. Raynal. 2013. Distributed Algorithms for Message-Passing Systems. Springer, 427--446. Google ScholarDigital Library
J. C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. IEEE Computer Society, 55--74. Google ScholarDigital Library
G. Schellhorn, J. Derrick, and H. Wehrheim. 2014. A sound and complete proof technique for linearizability of concurrent data structures. ACM Trans. Comput. Logic 15, 4, Article 31 (Sept. 2014), 37 pages. Google ScholarDigital Library
G. Schellhorn, B. Tofan, G. Ernst, and W. Reif. 2011. Interleaved programs and rely-guarantee reasoning with ITL. In TIME, C. Combi, M. Leucker, and F. Wolter (Eds.). IEEE, 99--106. Google ScholarDigital Library
G. Schellhorn, H. Wehrheim, and J. Derrick. 2012. How to prove algorithms linearisable. In CAV (LNCS), P. Madhusudan and S. A. Seshia (Eds.), Vol. 7358. Springer, 243--259. Google ScholarDigital Library
C.-H. Shann, T.-L. Huang, and C. Chen. 2000. A practical nonblocking queue algorithm using compare-and-swap. In ICPADS. 470--475. Google ScholarDigital Library
M. Shapiro and B. Kemme. 2009. Eventual consistency. In Encyclopedia of Database Systems, L. Liu and M. T. Özsu (Eds.). Springer, 1071--1072.Google Scholar
N. Shavit. 2011. Data structures in the multicore age. Commun. ACM 54, 3 (2011), 76--84. Google ScholarDigital Library
G. Smith. 1999. The Object-Z Specification Language. Springer.Google Scholar
G. Smith, J. Derrick, and B. Dongol. 2014. Admit your weakness: Verifying correctness on TSO architectures. In FACS (LNCS), I. Lanese and E. Madelaine (Eds.), Vol. 8997. Springer, 364--383.Google Scholar
B. Tofan, S. Bäumler, G. Schellhorn, and W. Reif. 2010. Temporal logic verification of lock-freedom. In MPC (LNCS), C. Bolduc, J. Desharnais, and B. Ktari (Eds.), Vol. 6120. Springer, 377--396. Google ScholarDigital Library
B. Tofan, G. Schellhorn, and W. Reif. 2011. Formal verification of a lock-free stack with hazard pointers. In ICTAC (LNCS), A. Cerone and P. Pihlajasaari (Eds.), Vol. 6916. Springer, 239--255. Google ScholarDigital Library
B. Tofan, G. Schellhorn, and W. Reif. 2014. A compositional proof method for linearizability applied to a wait-free multiset. In iFM (LNCS), E. Albert and E. Sekerinski (Eds.), Vol. 8739. Springer, 357--372.Google Scholar
R. K. Treiber. 1986. Systems Programming: Coping with Parallelism. Technical Report RJ 5118. IBM Almaden Res. Ctr.Google Scholar
A. J. Turon and M. Wand. 2011. A separation logic for refining concurrent objects. In POPL, T. Ball and M. Sagiv (Eds.). ACM, 247--258. Google ScholarDigital Library
V. Vafeiadis. 2007. Modular Fine-Grained Concurrency Verification. Ph.D. Dissertation. University of Cambridge.Google Scholar
V. Vafeiadis. 2009. Shape-value abstraction for verifying linearizability. In VMCAI (LNCS), N. D. Jones and M. Müller-Olm (Eds.), Vol. 5403. Springer, 335--348. Google ScholarDigital Library
V. Vafeiadis. 2010. Automatically proving linearizability. In CAV (LNCS), T. Touili, B. Cook, and P. Jackson (Eds.), Vol. 6174. Springer, 450--464. Google ScholarDigital Library
V. Vafeiadis, M. Herlihy, T. Hoare, and M. Shapiro. 2006. Proving correctness of highly-concurrent linearisable objects. In PPOPP, J. Torrellas and S. Chatterjee (Eds.). 129--136. Google ScholarDigital Library
V. Vafeiadis and M. J. Parkinson. 2007. A marriage of rely/guarantee and separation logic. In CONCUR (LNCS), L. Caires and V. T. Vasconcelos (Eds.), Vol. 4703. Springer, 256--271. Google ScholarDigital Library
S. van Staden. 2015. On rely-guarantee reasoning. In MPC (LNCS), R. Hinze and J. Voigtländer (Eds.), Vol. 9129. Springer, 30--49. DOI:http://dx.doi.org/10.1007/978-3-319-19797-5_2Google Scholar
M. T. Vechev and E. Yahav. 2008. Deriving linearizable fine-grained concurrent objects. In PLDI, R. Gupta and S. P. Amarasinghe (Eds.). ACM, 125--135. Google ScholarDigital Library
M. T. Vechev, E. Yahav, and G. Yorsh. 2009. Experience with model checking linearizability. In SPIN (LNCS), C. S. Pasareanu (Ed.), Vol. 5578. Springer, 261--278. Google ScholarDigital Library
Z. Zhang, X. Feng, M. Fu, Z. Shao, and Y. Li. 2012. A structural approach to prophecy variables. In TAMC (LNCS), M. Agrawal, S. B. Cooper, and A. Li (Eds.), Vol. 7287. Springer, 61--71. Google ScholarDigital Library

Index Terms

Recommendations

Verifying Linearizability via Optimized Refinement Checking

Linearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: 1) All executions of concurrent operations are serializable, and 2) ...
Read More
On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models

Concurrent libraries are the building blocks for concurrency. They encompass a range of abstractions (locks, exchangers, stacks, queues, sets) built in a layered fashion: more advanced libraries are built out of simpler ones. While there has been a lot ...
Read More
A calculus of atomic actions
POPL '09

We present a proof calculus and method for the static verification of assertions and procedure specifications in shared-memory concurrent programs. The key idea in our approach is to use atomicity as a proof tool and to simplify the verification of ...
Read More

Comments

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Published in
ACM Computing Surveys Volume 48, Issue 2
November 2015
615 pages
ISSN:0360-0300
EISSN:1557-7341
DOI:10.1145/2830539
Editor:
Sartaj Sahni
Department of Computer and Information Science and Engineering/University of Florida/Gainesville, FL
Issue’s Table of Contents
Copyright © 2015 ACM
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Sponsors
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
- Published: 24 September 2015
- Accepted: 1 June 2015
- Revised: 1 January 2015
- Received: 1 December 2014
Published in csur Volume 48, Issue 2

Permissions
Request permissions about this article.
Request Permissions

Check for updates
Author Tags
Linearisability
abstraction
compositional proofs
concurrent objects
interval-based methods
mechanisation
reduction
refinement
shape analysis
Qualifiers
- survey
Conference
Funding Sources
Other Metrics
View Article Metrics

Article Metrics
- 22
  Total Citations
  View Citations
- 693
  Total Downloads
- Downloads (Last 12 months)36
- Downloads (Last 6 weeks)3
Other Metrics
View Author Metrics
Cited By
View all

PDF Format

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Verifying Linearisability: A Comparative Survey

ACM Computing Surveys

Abstract

References

Cited By

Index Terms

Recommendations

Verifying Linearizability via Optimized Refinement Checking

On library correctness under weak memory consistency: specifying and verifying concurrent libraries under declarative consistency models

A calculus of atomic actions