Axioms for concurrent objects

ABSTRACT

Specification and verification techniques for abstract data types that have been successful for sequential programs can be extended in a natural way to provide the same benefits for concurrent programs. We propose an approach to specifying and verifying concurrent objects based on a novel correctness condition, which we call “linearizability.” Linearizability provides the illusion that each operation takes effect instantaneously at some point between its invocation and its response, implying that the meaning of a concurrent object's operations can still be given by pre- and post-conditions. In this paper, we will define and discuss linearizability, and then give examples of how to reason about concurrent objects and verify their implementations based on their (sequential) axiomatic specifications.

REFERENCES

• 1: J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright. Abstract Data Types as Initial Algebras and Correctness of Data Representations. In Proceedings from the Conference of Computer Graphics, Pattern Recognition and Data Structures, pages 89-93. ACM, May, 1975.
• 2: Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
• 3: G. Birkhoff and J.D. Lipson. Heterogeneous Algebras. Journal of Combinatorial Theory 8:115-133, 1970.
• 4: R.M. Burstalt and J.A. Goguen. Putting Theories Together to Make Specifications. in Fifth international joint Conference on Artificial Intelligence, pages 1045-1058, August, 1977. Invited paper.
• 5: H.-D. Ehrich. Extensions and Implementations of Abstract Data Type Specifications. Lecture Notes in Computer Science. Volume ~a4.Mathematical Foundations of Computer Science 1978 Proceedings. $pringer-Vedag, Poland, 1978, pages 155-164. 7th Symposium.
• 6: Hartmut Ehrig , B. Mahr, Fundamentals of Algebraic Specification I, Springer-Verlag New York, Inc., Secaucus, NJ, 1985
• 7: Allan Gottlieb , Boris D. Lubachevsky , Larry Rudolph, Basic Techniques for the Efficient Coordination of Very Large Numbers of Cooperating Sequential Processors, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.164-189, April 1983 [doi>10.1145/69624.357206]
• 8: J.V. Guffag. The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto, Toronto, Canada, September, 1975.
• 9: John V. Guttag , Ellis Horowitz , David R. Musser, Abstract data types and software validation, Communications of the ACM, v.21 n.12, p.1048-1064, Dec. 1978 [doi>10.1145/359657.359666]
• 10: J.V. Guttag, J.J. Homing, and j.M. Wing. Larch in Five Easy Pieces. Technical Report 5, DEC Systems Research Center, july, 1985.
• 11: J.V. Guttag, J.J. Homing, and J.M. Wing. The Larch Family of Specification Languages. IEEE Software 2(5):24-36, September, 1985.
• 12: B.T. Hailpern and S. Owicki. Verifying Network Protocols Using Temporal Logic. In Proceedings Trends and Applications 1980: Computer Network Protocols, pages 18-28. IEEE Computer Society, 1980.
• 13: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 14: C.A.R. Hoare. Proof of Correctness of Data Representations. Acta Informatica 1(1):271-281,1972.
• 15: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 16: Samuel Kamin, Final Data Types and Their Specification, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.1, p.97-121, Jan. 1983 [doi>10.1145/357195.357202]
• 17: L. Lamport. How to Make a Multiprocessor Computer That Correctly Executes Muttiprocess Programs. IEEE Transactions on Computers C-28(9):690, September, 1979.
• 18: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 19: L. Lamport. On Interprocess Communication. Technical Report 8, DEC Systems Research Center, 1985. To appear in Distributed Computing.
• 20: Barbara Liskov, Abstraction and specification in program development, MIT Press, Cambridge, MA, 1986
• 21: Z Manna , Amir Pnueli, Verification of concurrent programs, Part I: The temporal framework, Stanford University, Stanford, CA, 1981
• 22: J. Misra, Axioms for memory access in asynchronous hardware systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.1, p.142-153, Jan. 1986 [doi>10.1145/5001.5007]
• 23: S. Owicki and D. Gries. An Axiomatic Proof Technique for Parallel Programs. Actalnformatica 6(4):319-340, 1976,
• 24: Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
• 25: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 26: Christos H. Papadimitriou, The serializability of concurrent database updates, Journal of the ACM (JACM), v.26 n.4, p.631-653, Oct. 1979 [doi>10.1145/322154.322158]
• 27: A. Pnueli. The Temporal Logic of Programs. In 18th Annua/ Symposium on Foundations of Computer Science, pages 46.57. Providence, RI, Oct. 31 ~ Nov. 2, 1977.
• 28: M. Wand. Final Algebra Semantics and Data Type Extensions. Journal of Computer and System Sciences 19(1 ):27-44, August, 1979.
• 29: S.N. Zilles. Abstract Specifications for Data Types. IBM Research Laboratory, San Jose, CA, 1975.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions

General Terms:
Algorithms, Languages, Theory, Verification