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].




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