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

On Wed, Nov 20, 2024 at 6:14 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:

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

On Tuesday, November 19, 2024 at 12:49:24 AM UTC+1 andrew...@xxxxxxxxx wrote:
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

On Monday, November 18, 2024 at 9:51:45 AM UTC-5 Stephan Merz wrote:
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

On 17 Nov 2024, at 20:05, Andrew Helwer <andrew...@xxxxxxxxx> wrote:

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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/7df3a268-b8a2-44dc-a0bd-311acad6c65an%40googlegroups.com.