Functional dependencies of variables in wait-free programs

Abstract

Suppose that we are given a waite-free protocol for the asynchronous, concurrent processes P ₁,P ₂,...,P _r , Q ₁,Q ₂,...,Q _s , with r≥2, s≥0. For any run (or interleaving) ρ of the protocol and any initialization init of all the protocol variables let X[ρ, init] be the value of the variable X at the end of the run ρ. The variables X ₁,X ₂,...,X _r "belonging" to the processors P ₁,P ₂,...,P _r , respectively, are called functionally dependent for the initialization init, if for any runs ρ, ρ of the protocol,

$$(\forall i,j)(X_i [\rho ,init] = X_i [\sigma ,init] \Leftrightarrow X_j [\rho ,init] = X_j [\sigma ,init]).$$

For any run ρ and any initialization init of the protocol define the evaluation mapping eval _{X 1},X ₂,...,X _r (ρ, init)=(X ₁[ρ, init],X ₂[ρ, init],...,X _r [ρ, init]). We show that for any protocol as above, the variables X ₁,X ₂,...,X _r are functionally dependent for the initialization init if and only if the quantity eval _{X 1},X ₂,...,X _r (ρ, init) is independent of ρ.