STOC Conference 2011 Conference Paper
- Wojciech M. Golab
- Lisa Higham
- Philipp Woelfel
Linearizability is the gold standard among algorithm designers for deducing the correctness of a distributed algorithm using implemented shared objects from the correctness of the corresponding algorithm using atomic versions of the same objects. We show that linearizability does not suffice for this purpose when processes can exploit randomization, and we discuss the existence of alternative correctness conditions. This paper makes the following contributions: 1. Various examples demonstrate that using well-known linearizable implementations of objects (e.g., snapshots) in place of atomic objects can change the probability distribution of the outcomes that the adversary is able to generate. In some cases, an oblivious adversary can create a probability distribution of outcomes for an algorithm with implemented, linearizable objects, that not even a strong adversary can generate for the same algorithm with atomic objects. 2. A new correctness condition for shared object implementations, called strong inearizability , is defined. We prove that a strong adversary (i.e., one that sees the outcome of each coin flip immediately) gains no additional power when atomic objects are replaced by strongly linearizable implementations. In general, no strictly weaker correctness condition suffices to ensure this. We also show that strong linearizability is a local and composable property. 3. In contrast to the situation for the strong adversary, for a natural weaker adversary (one that cannot see a process' coin flip until its next operation on a shared object) we prove that there is no correspondingly general correctness condition. Specifically, any linearizable implementation of counters called terminating. from atomic registers and load-linked/store-conditional objects, that satisfies a natural locality property, necessarily gives the weak adversary more power than it has with atomic counters.