A Constructive Proof on the Compositionality of Linearizability

TL;DR

This paper provides a new constructive proof for the compositionality of linearizability, introducing a hierarchical model and an efficient algorithm for linearization in distributed systems.

Contribution

It presents a novel hierarchical system model and a constructive proof that leads to an efficient linearization algorithm for linearizability.

Findings

Constructs a hierarchical model for shared memory and message passing systems.

Provides a constructive proof of the compositionality theorem for linearizability.

Develops an algorithm with O(N*logP) time complexity for linearization.

Abstract

Linearizability is the strongest correctness property for both shared memory and message passing systems. One of its useful features is the compositionality: a history (execution) is linearizable if and only if each object (component) subhistory is linearizable. In this paper, we propose a new hierarchical system model to address challenges in modular development of cloud systems. Object are defined by induction from the most fundamental atomic Boolean registers, and histories are represented as countable well-ordered structures of events to deal with both finite and infinite executions. Then, we present a new constructive proof on the compositionality theorem of linearizability inspired by Multiway Merge. This proof deduces a theoretically efficient algorithm which generates linearization in O(N*logP) running time with O(N) space, where P and N are process/event numbers respectively.