Specifying Concurrent Problems: Beyond Linearizability

TL;DR

This paper introduces interval-linearizability, a generalization of linearizability, enabling the specification of concurrent problems beyond traditional task and object models, and explores their expressive power.

Contribution

It proposes the concept of interval-sequential objects and extends task definitions to encompass all interval-sequential objects, broadening the scope of specification methods.

Findings

Interval-linearizability generalizes linearizability for concurrent executions.

Not all sequential one-shot objects can be expressed as tasks.

Extended task definitions can specify any interval-sequential object.

Abstract

Tasks and objects are two predominant ways of specifying distributed problems. A task is specified by an input/output relation, defining for each set of processes that may run concurrently, and each assignment of inputs to the processes in the set, the valid outputs of the processes. An object is specified by an automaton describing the outputs the object may produce when it is accessed sequentially. Thus, tasks explicitly state what may happen only when sets of processes run concurrently, while objects only specify what happens when processes access the object sequentially. Each one requires its own implementation notion, to tell when an execution satisfies the specification. For objects linearizability is commonly used, a very elegant and useful consistency condition. For tasks implementation notions are less explored. The paper introduces the notion of interval-sequential object. The corresponding implementation notion of interval-linearizability generalizes linearizability, and allows to associate states along the interval of execution of an operation. Interval-linearizability allows to specify any task, however, there are sequential one-shot objects that cannot be expressed as tasks, under the simplest interpretation of a task. It also shows that a natural extension of the notion of a task is expressive enough to specify any interval-sequential object.