Abstract
Linearisability is a central notion for verifying concurrent
libraries: a library is proven correct if its operational history can
be rearranged into a sequential one that satisfies a given
specification. Until now, linearisability has been examined for
libraries in which method arguments and method results were of ground
type. In this paper we extend linearisability to the general
higher-order setting, where methods of arbitrary type can be passed as
arguments and returned as values, and establish its soundness. This is
joint work with Nikos Tzevelekos (Queen Mary University of London)
presented at CONCUR'17.
Last modified: Fri Oct 13 14:29:46 CEST 2017