A Constructive Proof on the Compositionality of Linearizability

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.