Higher-Order Linearisability

TL;DR

This paper extends the concept of linearisability to higher-order libraries where methods can be passed as arguments and returned as values, enabling verification of more complex concurrent systems.

Contribution

It introduces a generalized notion of linearisability for higher-order settings, allowing verification of libraries with higher-order methods and demonstrating its correctness on several examples.

Findings

Successfully extended linearisability to higher-order libraries

Proved correctness of several higher-order example libraries

Enhanced verification techniques for complex concurrent systems

Abstract

Linearisability is a central notion for verifying concurrent libraries: a given library is proven safe if its operational history can be rearranged into a new sequential one which, in addition, satisfies a given specification. Linearisability has been examined for libraries in which method arguments and method results are of ground type, including libraries parameterised with such methods. In this paper we extend linearisability to the general higher-order setting: methods can be passed as arguments and returned as values. A library may also depend on abstract methods of any order. We use this generalised notion to show correctness of several higher-order example libraries.