Correctness of Self-Stabilizing Algorithms Under the Dolev Model When Adapted to Composite Atomicity Models

1. Introduction

A distributed system consists of a set of loosely connected processors that do not share a global memory. It is usually modelled by a connected simple undirected graph with each node representing a processor in the system and each edge representing the link connecting processors and Each processor has one or more shared registers and possibly some non-shared local variables, the contents of which specify the local state of the processor. Local states of all processors in the system at a certain time constitute the global configuration (or, simply, configuration) of the system at that time. The main restriction of the distributed system is that each processor in the system can only access the data (i.e., read the shared data) of its neighbors. Since a distributed algorithm is an algorithm that works in a distributed system, it cannot violate this main restriction. In this paper, we adopt the point of view in Dolev et al. (1993). Thus, an atomic step is the “largest” step that is guaranteed to be executed uninterruptedly. A distributed algorithm uses composite atomicity if some atomic step contains (at least) a read operation and a write operation. A distributed algorithm uses read/write atomicity if each atomic step contains either a single read operation or a single write operation but not both.