Characterizing Implementations that Preserve Properties of Concurrent Randomized Algorithms

Abstract

We show that correctness criteria of concurrent algorithms are mathematically equivalent to the existence of so-called simulations between implementations of the algorithms in a well-known framework (that of input/output automata) and simple canonical automata. This equivalence allows us to frame our proofs of correctness in a language much more amenable to machine-checking than conventional proofs. We give the first demonstration that when strongly linearizable implementations of randomized concurrent algorithms are utilized, then the distributions of a well-defined class of random variables are preserved under object substitution by non-concurrent implementations of the same algorithms. We also consider weaker conditions than strong linearizability under which implementations are still correct in the presence of randomization.