×

Strict linearizability and abstract atomicity. (English) Zbl 1458.68135

Summary: Linearizability is a commonly accepted consistency condition for concurrent objects. Filipović et al. show that linearizability is equivalent to observational refinement. However, linearizability does not permit concurrent objects to share memory spaces with their client programs. We show that linearizability (or observational refinement) can be broken even though a client program of an object accesses the shared memory spaces without interleaving with the methods of the object. In this paper, we present strict linearizability which lifts this limitation and can ensure client-side traces and final-states equivalence even in a relaxed program model allowing clients to directly access the internal states of concurrent objects. We also investigate several important properties of strict linearizability. At a high level of abstraction, a concurrent object can be viewed as a concurrent implementation of an abstract data type (ADT). We also present a correctness criterion for relating an ADT and its concurrent implementation, which is the combination of linearizability and data abstraction and can ensure observational equivalence. We also investigate its relationship with strict linearizability.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

Atomizer
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Henzinger, T. A., Sezgin, A. and Vafeiadis, V., Aspect-oriented linearizability proofs, In CONCUR (2013), pp. 242-256. · Zbl 1390.68213
[2] C. Flanagan and S. Qadeer, Types for atomicity, In TLDI (2003). · Zbl 1271.68086
[3] Jonsson, B., Using refinement calculus techniques to prove linearizability, Formal Asp. Comput.24(4-6) (2012) 537-554. · Zbl 1259.68128
[4] Farzan, A. and Madhusudan, P., Monitoring atomicity in concurrent programs, Computer Aided Verification (2008) 52-65. · Zbl 1155.68365
[5] O. Shacham, E. Yahav, G. Gueta, A. Aiken, N. Bronson, M. Sagiv, and M. Vechev, Verifying atomicity via data independence, ISSTA (2014).
[6] Afek, Y., Korland, G. and Yanovsky, E., Quasi-linearizability: Relaxed consistency for improved concurrency, International Conference on Principles of Distributed Systems (2010), pp. 395-410.
[7] Cerone, A., Gotsman, A. and Yang, H., Parameterised linearisability, International Colloquium on Automata, Languages, and Programming (2014). · Zbl 1409.68068
[8] Herlihy, M. and Wing, J., Linearizability: A correctness condition for concurrent objects, ACM TOPLAS12(3) (1990) 463-492.
[9] S. Qadeer, A. Sezgin and S. Tasiran, Back and forth: Prophecy variables for static verification of concurrent programs, Tech Report.
[10] V. Vafeiadis, Modular fine-grained concurrency verification, PhD thesis, University of Cambridge (2008).
[11] H. Liang and X. Feng, Modular verification of linearizability with non-fixed linearization points, In PLDI (2013).
[12] T. A. Henzinger, C. M. Kirsch, H. Payer, A. Sezgin and A. Sokolova, Quantitative relaxation of concurrent data structures, In POPL (2013). · Zbl 1301.68176
[13] Vogels, W., Eventually consistent, Commun. ACM52(1) (2009) 40-44.
[14] M. Herlihy and N. Shavit, The art of multiprocessor programming, Morgan Kaufmann, Apr. 2008.
[15] Hoare, C. A. R., Proof of correctness of data representation, Acta Informatica1 (1972) 271-281. · Zbl 0244.68009
[16] Lipton, R. J., Reduction: A method of proving properties of parallel programs, Communications of the ACM18(12) (1975) 717-721. · Zbl 0316.68015
[17] Filipović, I., O’Hearn, P. W., Rinetzky, N. and Yang, H., Abstraction for concurrent objects, Theor. Comput. Sci.411(51-52) (2010) 4379-4398. · Zbl 1209.68156
[18] M. M. Michael and M. L. Scott, Simple, fast, and practical nonblocking and blocking concurrent queue algorithms. In PODC’96.
[19] S. Heller, M. Herlihy, V. Luchangco, M. Moir, W. N. Scherer and N. Shavit, A lazy concurrent list-based set algorithm, in OPODIS (2005).
[20] T. L. Harris, K. Fraser and I. A. Pratt, A practical multi-word compare-and-swap operation, In DISC’02. · Zbl 1029.68525
[21] C. Flanagan and S. Qadeer, A type and effect system for atomicity, In PLDI (2003). · Zbl 1271.68086
[22] E. Cohen and L. Lamport, Reduction in TLA, In CONCUR (1998).
[23] Flanagan, C. and Freund, S. N., Atomizer: A dynamic atomicity checker for multithreaded programs, ACM SIGPLAN Notices39(1) (2004) 256-267. · Zbl 1325.68064
[24] Derrick, J., Schellhorn, G. and Wehrheim, H., Mechanically verified proof obligations for linearizability, ACM Trans. Program. Lang. Syst.33(1) (2011) 4.
[25] A. Bouajjani, M. Emmi, C. Enea and J. Hamza, On reducing linearizability to state reachability, In ICALP (2015). · Zbl 1395.68089
[26] Papadimitriou, C. H., The serializability of concurrent database updates, J. ACM26(4) (1979) 631-653. · Zbl 0419.68036
[27] Lamport, L., How to write a 21st century proof, Journal of Fixed Point Theory and Applications11(1) (2012) 43-63. · Zbl 1271.03082
[28] Brookes, S., A semantics for concurrent separation logic, Theoretical Computer Science375(1) (2007) 227-270. · Zbl 1111.68021
[29] Lamport, L., How to make a multiprocessor computer that correctly executes multiprocess programs, IEEE Trans. Comput.C-28(9) (1979) 690-691. · Zbl 0419.68045
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.