[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Consensus spec safety in Paxos example
Hi Markus and Jones,
Yeah, I am talking about safety. Markus, "stays chosen" is a safety property - it states that "nothing bad happens". Liveness properties state that "a good thing happens eventually", and are irrelevant to this discussion.
To quote https://learntla.com/core/temporal-logic.html and https://learntla.com/core/action-properties.html: all invariants are safety properties, but not all safety properties are invariants. In this Consensus example, we can't fully express safety by an invariant - it should be at least an "action property".
> Note, though, that Pavel’s formula is not a legal TLA formula because it is not stuttering-insensitive
The last version I mentioned does tolerate stuttering (it allows "chosen" variable to stay unchanged): chosen \subseteq chosen' /\ Cardinality(chosen') \leq 1. But we can modify it with a box _expression_, to explicitly express stuttering.
I think the THEOREM should be proving this action property holds, i.e. something like: THEOREM Invariance == Spec => [][chosen \subseteq chosen' /\ Cardinality(chosen') \leq 1]_chosen
Maybe there is a simpler way to express this. This property might seem somewhat a tautology with what Init/Next describes, but there is a difference: Next draws a value from the Value set, so it's described more like an "algorithm". Whereas the property that I'm describing here does not depend on the Value set, and hence is more general.
Thank you,
Pavel
On Friday, May 10, 2024 at 8:00:17 PM UTC+1 Jones Martins wrote:
Thanks, Markus. I may not have been clear enough.
Pavel was worried about the value of chosen changing from one state to the next:
>> If I am interpreting it correctly, the invariant does not fully specify
the safety property: it allows a sequence in which a value is chosen,
then another value replaces it (the size of the chosen set is still 1,
so the invariant remains true). Or a value is chosen, then the set is
emptied, then another value is chosen; etc.
One way to assert that chosen doesn't change after being set is through a liveness property like StaysChosen.
What Pavel suggests (chosen = {} / chosen' = chose) is not a liveness but a safety property; its counterexample is a finite prefix of a behavior, e.g., a prefix where v1 is chosen but replaced by v2.
This property cannot be stated as an invariant, i.e., a state-level formula. The occurrence of the prime operator turns it into an action-level formula. Note, though, that Pavel’s formula is not a legal TLA formula because it is not stuttering-insensitive (see page 90 in Specifying Systems).
Regarding the original question: Note that Voting states the theorem Spec => Consensus!Spec, making the behavior formula Spec in Consensus Pavel’s desired correctness property, except for Voting. We can also say that Voting refines Consensus. For Consensus, it is probably easy enough to see that Consensus satisfies the proposed property above.
M.
> On May 10, 2024, at 10:38 AM, Jones Martins <jone...@xxxxxxxxx> wrote:
>
> Sure! What you seem to be trying to express is a liveness property instead of an invariant.
> Just be careful not to assert about values in the next state, such as chosen'.
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 on the web visit https://groups.google.com/d/msgid/tlaplus/2c3af04b-b2b8-4346-a413-d38cb0c37fa9n%40googlegroups.com.