Suppose that we are given a waite-free protocol for the asynchronous, concurrent processes P1,P2,…,Pr, Q1,Q2,…,Qs, 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 X1,X2,…,Xr “belonging” to the processors P1,P2,…,Pr, respectively, are called functionally dependent for the initialization init, if for any runs ρ, ρ of the protocol, (∀i,j)(Xi[ρ,init]=Xi[σ,init]⇔Xj[ρ,init]=Xj[σ,init]). (∀i,j)(Xi[ρ,init]=Xi[σ,init]⇔Xj[ρ,init]=Xj[σ,init]). For any run ρ and any initialization init of the protocol define the evaluation mapping evalX1,X2,…,Xr(ρ, init)=(X1[ρ, init],X2[ρ, init],…,Xr[ρ, init]). We show that for any protocol as above, the variables X1,X2,…,Xr are functionally dependent for the initialization init if and only if the quantity evalX1,X2,…,Xr (ρ, init) is independent of ρ.
International Workshop on Distributed Algorithms
Centrum Wiskunde & Informatica, Amsterdam, The Netherlands

Kranakis, E. (1989). Functional dependencies of variables in wait-free programs. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 148–159). doi:10.1007/3-540-51687-5_39