Consensus spec safety in Paxos example

[Pavel Kalinnikov]

Hello,

I am looking at the Consensus spec in tlaplus examples repo, which specifies the single-value consensus problem.

The Init/Next spec in this file correctly specifies consensus, because it precludes the chosen set from changing after it got to contain exactly one value.

What value does the the safety invariant in lines 36-37, and the theorem that follows it, bring to this spec? 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.

Is the value of this invariant+theorem in just demonstrating an interesting property? Is it not strictly needed to be in this spec?

Is there a way to fix this invariant, so that it fully represents the consensus safety property (rather than partially, like it seems).

Thank you,

Pavel

[Pavel Kalinnikov]

Should this line

       /\ Cardinality(chosen) \leq 1

be augmented with something like:

       /\ Cardinality(chosen') \leq 1

       /\ chosen = {} \/ chosen' = chosen

[Jones Martins]

Hi Pavel,

The Voting module instantiates the Consensus module to prove that Voting's Spec implies Consensus' Spec.

The consensus specification itself is pretty abstract.

Init expresses that chosen = {} is true in the first state of every behavior.

Next expresses that if chosen = {} is true, then chosen' = { <some value> }.

This means that, when some value has been chosen, it never changes again, so the original  `Inv` invariant is strong enough.

By the way, `Inv` can't be augmented as you suggested. Invariants are state predicates, and state predicates don't contain primed variables.

Best,

Jones

[Pavel Kalinnikov]

Hi Jones,

Your explanation matches my understanding, however I think the `Inv` does not correctly represent a consensus safety property. To demonstrate that, we can change the `Next` action in such a way that the invariant will still hold. For example, if we can allow a transition from {v} back to {}, the invariant is still true, but the safety is broken.

The safety invariant here has to have a temporal aspect: once the chosen set is non-empty, it stays so.

I.e. the comment "Safety: At most one value is chosen" seems misleading here. It does express some invariant, but this invariant does not on its own guarantee safety.

Thank you,

Pavel

[Jones Martins]

Hi Pavel,

If I understood you correctly, you're saying the formula `Inv` doesn't represent a consensus safety property: this invariant is too weak, and it's satisfied by a sequence of assignments for `chosen` such as {} -> {1} -> {} -> {2} -> {2} -> etc.

That's true. In fact, there's an infinite number of possible behaviors in the universe such that `Inv` is True, but these behaviors are irrelevant. It depends on what specification described these behaviors in the first place, and that `chosen` has the same meaning in both specifications. Meaning is essential.

> To demonstrate that, we can change the `Next` action in such a way that the invariant will still hold. For example, if we can allow a transition from {v} back to {}, the invariant is still true, but the safety is broken.

Indeed, but that wouldn't be a consensus specification anymore.

> The safety invariant here has to have a temporal aspect: once the chosen set is non-empty, it stays so.

What is so elegant about TLA+ is that the “temporal aspect” you mentioned is the specification itself. In other words, Consensus' Spec expresses that “once the chosen set is non-empty, it stays so”:  action `Next` in `Consensus` selects one value, then stutters forever.

Best,

Jones

P.S. I'd expand on the true danger of false positives through bad refinement mappings, but it's late here, and I need to sleep haha

[Pavel Kalinnikov]

Hi Jones,

Yes, I agree that Init/Next on its own correctly specifies consensus, with the temporal aspect of it. Hence was my original question: what value does the `Inv` and THEOREM bring to this spec, given that it only states a necessary but not sufficient invariant for consensus? For what I see, both `Inv` and THEOREM can be removed from this file, and the spec will remain rigorous.

And the second part of my question was: can we state a more rigorous property here, instead of `Inv`, such as:

    "chosen \in chosen' /\ Cardinality(chosen') \leq 1"

and prove a THEOREM that more convincingly confirms that Init/Next spec is the right thing?

Thank you,

Pavel

[Pavel Kalinnikov]

correction to above invariant:

    chosen \subseteq chosen' /\ Cardinality(chosen') \leq 1

[Jones Martins]

Hi Pavel,

>> For what I see, both Inv and THEOREM can be removed from this file, and the spec will remain rigorous

>> what value does the Inv and THEOREM  bring to this spec, given that it only states a necessary but not sufficient invariant for consensus?

On Inv being removed:

TypeOK states that chosen is a finite subset of Value, so chosen can be a finite set of any size.

Inv states that TypeOK is true and that the cardinality of `chosen` is zero or one.

So TypeOK is weaker than Inv. Should we remove it too?

There's nothing wrong with stating that the spec satisfies “weak” properties.

On THEOREM being removed and rigor:

Some more advanced users might explain it better than I do, but here's my take on proofs and rigor:

A THEOREM statement in a TLA+ specification serves as documentation to state something you believe to be true.

TLC ignores THEOREM statements because theorems can't be proved by model checking or simulation.

TLAPS, on the other hand, does not ignore THEOREM statements. You can see in the `Consensus.tla` file that there's a proof. This proof must've been checked by TLAPS.

So, in that regard, theorem proofs are the golden standard for rigor, even if these theorems are obvious to us. 

Specifications with more proofs are more rigorous than specifications with fewer proofs.

>> can we state a more rigorous property here, instead of Inv, such as: [...]

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

The Consensus module already contains a liveness property: Success.

Success states that chosen eventually isn't empty.

You might say that it doesn't assert about chosen's cardinality, and conclude it's a “weak” property.

So let's define a stricter liveness property: “a single value is eventually chosen and stays chosen”.

StaysChosen == <>[](\E v \in Value: chosen = { v })

To check a liveness property, you must specify liveness properties for your specification.

If your spec doesn't have liveness at all, you can't guarantee something happens: something might happen in some behaviors, nothing at all might happen in others.

In this case, that means the formulas Spec => Success and Spec => StaysChosen are false because they don't have liveness.

We usually specify the liveness of a TLA+ spec by declaring fairness for sub-actions of Next or Next itself.

In this case, Next doesn't contain sub-actions, so we'd declare weak or strong fairness for Next itself.

You can see that Consensus already defines a LiveSpec formula conjoining Spec with weak fairness for Next.

By specifying liveness for Spec, both formulas LiveSpec => Success and LiveSpec => StaysChosen will be true.

Jones

[Markus Kuppe]

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.

[Jones Martins]

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.

--
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/4PvjXi0tEBA/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/B121361B-894F-421E-BA0A-E1F0156F187E%40lemmster.de.

[Pavel Kalinnikov]

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