Revisiting Abstraction Functions For Reasoning About Concurrency

  • Jeannette M. Wing
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


Hoare introduced abstraction functions for reasoning about abstract data types in 1972 [1]. What happens in the presence of concurrency? Reasoning about objects in a concurrent system necessitates extending the notion of abstraction functions in order to model the system’s inherent nondeterminisitic behavior. My talk presented in detail the extensions required to reason about lock-free concurrent objects, used to build linearizable systems. It also discussed briefly a different extension required to reason about atomic objects, used to build fault-tolerant distributed systems.

Much of this work is joint with Maurice Herlihy and previously published in two papers [2, 3].


Correctness Condition Concurrent Program Concurrent System Single Representation Abstract Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    C.A.R. Hoare, “Proof of Correctness of Data Representations,” Ada Informatica, Vol. 1, 1972, pp. 271–281.MATHCrossRefGoogle Scholar
  2. [2]
    M.P. Herlihy and J.M. Wing, “Linearizability: A Correctness Condition for Concurrent Objects,” ACM TOPLAS, Vol. 12, No. 3, July 1990, pp. 463–492.CrossRefGoogle Scholar
  3. [3]
    J.M. Wing, “Verifying Atomic Data Types,” International Journal of Parallel Programming, Vol. 18, No. 5, 1989, pp. 315–357.MATHCrossRefGoogle Scholar

Copyright information

© Springer-Verlag London 1992

Authors and Affiliations

  • Jeannette M. Wing
    • 1
  1. 1.School of Computer ScienceCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations