On the Lazy Set object
Abstract
The aim of this article is to employ the Lazy Set algorithm as an example for a mathematical framework for proving the linearizability of distributed systems. The proof in this approach is divided into two stages of lower and higher abstraction level. At the higher level a list of "axioms" is formulated and a proof is given that any model theoretic structure that satisfies these axioms is linearizable. At this level the algorithm is not mentioned. At the lower level, a Simpler Lazy Set algorithm is described, and it is shown that any execution of this simpler algorithm generates a model of these axioms (and is therefore linearizable). Finally the linearization of the Lazy Set algorithm is obtained by proving that any of its executions has a {\em reduct} that is an execution of the Simpler algorithm. So the reduct executions are linearizable and this entails immediately linearizability of the Lazy Set algorithm itself.
Cite
@article{arxiv.1811.00756,
title = {On the Lazy Set object},
author = {Uri Abraham},
journal= {arXiv preprint arXiv:1811.00756},
year = {2018}
}