Output details

Abstraction for concurrent objects

<10>

A cross-culture paper linking concepts from programming language and concurrent algorithms communities. Linearizability, a favoured correctness condition in concurrent algorithms, is characterised in terms of observational refinement. It is the first to spell out guarantees for client programs implied by proofs of highly concurrent objects. This paper opens new lines on the long-delayed development of a theory of data abstraction for concurrency. It is the basis of Yang's research programme for finding appropriate correctness conditions for concurrent objects in realistic systems, which is pursued with researchers in IMDEA, Microsoft Research (corroboration from senior technical staff, email on file), and Cambridge.