[tlaplus] Question about weak fairness in A Science of Concurrent Programs

[Andrew Helwer <andrew.helwer@xxxxxxxxx>]

I am having some trouble understanding equation 4.13 on page 94; quoting:

The first thing we observe is that for a multiprocess program described with pseudocode, weak fairness of a process’s next-state action is equivalent to the conjunction of weak fairness of all the actions described by the process’s statements. That is, if PNext(p) equals ∃i ∈ I :Ai(p) for a set I, where action Ai(p) describes the statement with label i, and v is the tuple of program variables, then:

(4.13) |= WFv (PNext(p)) ≡ ∀ i ∈ I : WFv (Ai (p))

I've always thought that weak fairness of a disjunct of various actions is different from a conjunct of weak fairness of those disjuncts; consider an action like:

Next ==

  \/ A

  \/ B

  \/ C

Then WF(Next) means that if one of A, B, and C are enabled continuously (they can swap off) then a Next step must eventually be taken. However, I feel that's different from WF(A) /\ WF(B) /\ WF(C), which states that if those specific actions are continuously enabled then they will eventually be taken.

What might be at the root of my confusion is the assumption "for a multiprocess program described with pseudocode" since perhaps that restricts the actions we are considering; in my example with Next being the disjunction of A, B, and C, they can only swap off being enabled without themselves being taken if some other non-Next action is changing the variable state. Perhaps this hypothetical is ruled out by the assumption that we're talking about a multiprocess program described with pseudocode, and while it's true that 4.13 doesn't hold in general it does hold in this case.

Andrew Helwer

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4d8538b1-7c45-4660-92c0-1576b144363cn%40googlegroups.com.