Functional dependencies of variables in wait-free programs

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 ρ.

• View at Publisher

Full Text ( Final Version , 935kb )