Question about weak fairness in A Science of Concurrent Programs

[Andrew Helwer]

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

[Stephan Merz]

Hi Andrew,

you can convince yourself that both of the following are true for any actions A and B (I am dropping the subscript for simplicity):

(1) If ~((ENABLED A) /\ (ENABLED B)), i.e. the actions cannot be simultaneously enabled, then WF(A \/ B) => WF(A) /\ WF(B).

(2) If both (ENABLED A) /\ ~A /\ ~B => (ENABLED A)’ and (ENABLED B) /\ ~A /\ ~B => (ENABLED B’), i.e. only the occurrence of one of the actions may disable each of them, then WF(A) /\ WF(B) => WF(A \/ B).

In the context of a "multiprocess program described with pseudo-code", the actions Ai of interest are those associated with each label of a fixed process p in the pseudo-code. This is basically the situation of a PlusCal algorithm, where each such action is described as a conjunction including the predicate pc[p] = i. This implies that the condition of (1) above holds true and therefore

WF(Next(p)) => \A i \in I : WF(Ai(p))

For the converse implication, we have to show each subaction of process p can only be disabled by the occurrence of a step of process p. This is certainly true if the enabledness condition only depends on local variables of the process. However, if it may also depend on global variables, this will not generally be true. For example, a semaphore that synchronizes access of different processes to their critical sections could be taken by a different process, disabling process p. It is not clear to me if a sufficiently strong restriction holds for the algorithms alluded to in this part of the book, or if it is really the equivalence, and not just implication, that is required.

Stephan

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4d8538b1-7c45-4660-92c0-1576b144363cn%40googlegroups.com.

[Andrew Helwer]

Thanks Stephan, it does make more sense when I break it down in each direction and try to think of a counterexample but then realize it is covered under vacuous truth. Will chew on these some more.

Andrew

[Stephan Merz]

I've been thinking about this a little more. For arbitrary actions A and B, we also have (see proof below, and again I'm leaving out variable subscripts for simplicity, but the argument also holds with them included):

(3) Assume

         (*) |= (ENABLED A) /\ ~A => ~(ENABLED B)'   [only A may enable B], 

         (**) |= (ENABLED B) /\ ~B => ~(ENABLED  A')  [same condition vice versa]

then WF(A) /\ WF(B) => WF(A \/ B)

Combining (3) with (1) from my previous post gives us the equivalence of WF(A) /\ WF(B) and WF(A \/ B), assuming the hypotheses of (3)

and that A and B are never simultaneously enabled.

In the context of "multi-process programs described with pseudo-code", we have process p's next-state relation defined as

PNext(p) == A1(p) \/ .... \/ Ak(p)

where each Ai(p) is a conjunction including the conjunct pc(p) = i for asserting that control at process resides at label i. 

(If process p may terminate, we may assume that Ak(p) specifies that control resides at a terminal label and the process stutters.)

Now, for any disjunction of the actions Ai(p) of at least two such actions, let Aj(p) be one of them and let B denote the disjunction of the remaining disjuncts.

Then we have |= ~((ENABLED Aj(p)) /\ (ENABLED B)), since the constraints on where control resides are mutually exclusive.

Similarly, |= (ENABLED Aj(p)) /\ ~Aj(p) => ~(ENABLED B)' because the control of process p doesn't change as long as Aj(p) is not taken,

and vice versa |= (ENABLED B) /\ ~B => ~(ENABLED Aj(p))'.

So we can apply (1) and (3) and deduce WF(Aj(p) \/ B) <=> WF(Aj(p)) /\ WF(B). Continuing inductively, we obtain

WF(PNext(p)) <=> WF(A1(p)) /\ ... /\ WF(Ak(p)),

which justifies claim (4.13).

Now for the proof of (3):

Assume the given hypotheses, and assume that sigma is a behavior such that

sigma |= WF(A), sigma |= WF(B), sigma |= []ENABLED(A \/ B).

We must show that sigma |= <>(A \/ B), and for a contradiction let's assume sigma |= []~(A \/ B).

Since sigma |= []ENABLED (A \/ B), we must have sigma |= ENABLED (A \/ B) and thus either A or B must be enabled.

Consider the case sigma |= ENABLED A, the other one being symmetric.

Since we assume sigma |=~(A \/ B), by (*) we obtain sigma |= ~(ENABLED B)'.

Since sigma |= []ENABLED (A \/ B), we must have sigma |= (ENABLED A)'.

Continuing inductively, we get sigma |= [](ENABLED A), and together with sigma |= WF(A), we have sigma |= <>A and reach a contradiction.

Stephan

[Andrew Helwer]

I will add a note that I read further into the book and on page 109 it expands the proof a bit.

Separately I’ve noticed that temporal logic proofs tend to use proof by contradiction quite a bit. I’m not a constructivist but I it is occasionally confusing to see a false premise slipped in at various stages of a proof. Is there some reason proof by contradiction is so effective here? I guess it’s easier to find contradictions when you convert the negation of a <> property into a [] property.

Andrew Helwer

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/cKNAyeWQP_Y/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/7df3a268-b8a2-44dc-a0bd-311acad6c65an%40googlegroups.com.