Revisiting Abstraction Functions For Reasoning About Concurrency
Hoare introduced abstraction functions for reasoning about abstract data types in 1972 . 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].
KeywordsCorrectness Condition Concurrent Program Concurrent System Single Representation Abstract Type
Unable to display preview. Download preview PDF.