Check eventual consistency

[jayaprabhakar k]

Hi,

I am new to TLA+. I am trying to design a simple eventually consistent counter. 

Elements are added to a set. It could optionally, increment the counter. To ensure, the count becomes eventually consistent, there will be a separate ticker that periodically update the count.

-------------------------- MODULE EventualCounter --------------------------
EXTENDS Naturals,FiniteSets

CONSTANT MAX_ELEMENTS

VARIABLES elements, count, dirty

vars == <<elements, count, dirty>>

Init == /\ elements = {}
        /\ count = 0
        /\ dirty = 0

Add == /\ \E e \in 1..MAX_ELEMENTS:
              /\ e \notin elements
              /\ elements' = elements \union {e}
              /\ dirty' = 1
              /\ \/ count' = count + 1
                 \/ UNCHANGED count

Tick == /\ count' = Cardinality(elements)
        /\ dirty' = 0
        /\ UNCHANGED elements

ConsistencyInvariant == \/ dirty = 1
             \/ (count = Cardinality(elements))
               
             
Next == \/ Add
        \/ Tick  

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

=============================================================================

How do I add an invariant or temporal property that confirms the count will be eventually consistent with the real count?

If I simply add count = Cardinality(elements), that would fail after each Add/Insert. To pass the invariant, I added a dirty bit. But the, in this case, even if the Tick is never triggered, the invariant will pass.

What should I do to prove or verify, the count will be eventually consistent?

 

[jayaprabhakar k]

I found what to do for this simple model. Added a definition,

IsCountCorrect == (count = Cardinality(elements))

In the model I set the temporal property as `<>[]IsCountCorrect`. With this, the temporal check seems to work. Removing the Tick, ensures it works as well. I believe this correct.

Now, extending the model to Remove, breaks the model. 

Remove == /\ \E e \in elements:

              /\ elements' = elements \ {e}

              /\ dirty' = 1

              /\ UNCHANGED count

Next == Add \/ REMOVE \/ Tick 

.

Now, the temporal property is violated, because,  removing an element puts it back to an existing state, so the state is deduplicated and Tick will not run in this case.

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
 count |-> 0,
 dirty |-> 0,
 elements |-> {}
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "Add",
   location |-> "line 15, col 8 to line 20, col 32 of module EventualCounter"
 ],
 count |-> 0,
 dirty |-> 1,
 elements |-> {2}
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "Remove",
   location |-> "line 22, col 11 to line 26, col 32 of module EventualCounter"
 ],
 count |-> 0,
 dirty |-> 1,
 elements |-> {}
]
>>

---

I tried adding a seq number that keeps incrementing with Add/Remove explodes the state space and the model checker goes on for ever without ever stopping.

---

So I tried resetting seq after a Tick. And still get a similar error. 

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
 count |-> 0,
 dirty |-> 0,
 elements |-> {},
 seq |-> 0
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "Add",
   location |-> "line 15, col 8 to line 20, col 32 of module EventualCounter"
 ],
 count |-> 0,
 dirty |-> 1,
 elements |-> {3},
 seq |-> 1
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "Tick",
   location |-> "line 28, col 9 to line 31, col 29 of module EventualCounter"
 ],
 count |-> 1,
 dirty |-> 0,
 elements |-> {3},
 seq |-> 0
],
[
 _TEAction |-> [
   position |-> 4,
   name |-> "Remove",
   location |-> "line 22, col 11 to line 26, col 32 of module EventualCounter"
 ],
 count |-> 1,
 dirty |-> 1,
 elements |-> {},
 seq |-> 1
]
>>

The corresponding full code is,

-------------------------- MODULE EventualCounter --------------------------

EXTENDS Naturals,FiniteSets

CONSTANT MAX_ELEMENTS

VARIABLES elements, count, dirty, seq

vars == <<elements, count, dirty, seq>>

Init == /\ elements = {}

        /\ count = 0

        /\ dirty = 0

        /\ seq = 0

 

Add == /\ \E e \in 1..MAX_ELEMENTS:

              /\ e \notin elements

              /\ elements' = elements \union {e}

              /\ dirty' = 1

              /\ seq' = seq + 1

              /\ UNCHANGED count

Remove == /\ \E e \in elements:

              /\ elements' = elements \ {e}

              /\ dirty' = 1

              /\ seq' = seq + 1

              /\ UNCHANGED count

Tick == /\ count' = Cardinality(elements)

        /\ dirty' = 0

        /\ seq' = 0

        /\ UNCHANGED elements 

IsCountCorrect == (count = Cardinality(elements))

ConsistencyInvariant == \/ dirty = 1

                        \/ IsCountCorrect

                

EventualConsistencyInvariant == IsCountCorrect

Change == Add \/ Remove        

Next == Change \/ Tick  

Spec == Init /\ [][Next]_vars /\ SF_vars(Tick)

How do I resolve this? 

[Andrew Helwer]

Eventually-consistent systems are difficult to modelcheck in TLC because they are often monotonic - they have things like sequence counters ensuring they never return to a previous state, so their state space is infinite and thus a finite model checker will never (validly) terminate. The usual way around this is to add state constraints so state exploration is cut off at some arbitrary point, but unfortunately this means liveness checking becomes invalid.

I don't personally know a good solution here, usually I just stick with safety checking when modeling monotonic specs or try to make them finite somehow in a way which still corresponds meaningfully to reality. I haven't tried a symbolic modelchecker like Apalache yet but that also might be something to look into.

Andrew Helwer

[Hillel Wayne]

Hi,

Your problem is that <>[]IsCountCorrect says that eventually, the count is correct and never becomes incorrect again. What you actually want is []<>IsCountCorrect: the count, if incorrect, will always become correct again. Making this change (and removing seq) makes the spec pass.

H

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/afdae50c-9f3d-48b5-84b7-c7aa3ba561a9n%40googlegroups.com.

[jayaprabhakar k]

Thanks. That fixed the issue.

Trying to understand this better, related to seq.

1. If I remove seq, it still works, as long as I have either WF_vars(Tick) or SF_vars(Tick). Without it, if seq is not present, it doesn't work. 

2. Once I add WF_vars(Tick), even if I remove the Tick from next, Next == Add \/ Remove, it always passes, and never fails. Even worse, if I remove count'=Cardinality(elements) in tick, it still passes. 

For example, this code should NEVER pass because the count is never updated. However it passes. 

-------------------------- MODULE EventualCounter --------------------------

EXTENDS Naturals,FiniteSets

CONSTANT MAX_ELEMENTS, BUFFER_SIZE

VARIABLES elements, count, seq

vars == <<elements, count, seq>>

Init == /\ elements = {}

        /\ count = 0

        /\ seq = 0

Add == /\ \E e \in 1..MAX_ELEMENTS:

              /\ e \notin elements

         \*     /\ seq < BUFFER_SIZE

              /\ elements' = elements \union {e}

              /\ seq' =  1

              /\ UNCHANGED count

Remove == /\ \E e \in elements:

                 /\ Cardinality(elements) > 0

          \*       /\ seq < BUFFER_SIZE

                 /\ elements' = elements \ {e}

                 /\ seq' =  1

                 /\ UNCHANGED count

Tick == /\ seq' = 0      \* NOT UPDATING THE COUNT

        /\ UNCHANGED <<elements,count>>

ConsistencyInvariant == \/ seq > 0

             \/ (count = Cardinality(elements))

               

IsCountCorrect == (count = Cardinality(elements))

             

Next == \/ Add

        \/ Remove

      \*  \/ Tick  

Spec == Init /\ [][Next]_vars /\ WF_vars(Next) /\ WF_vars(Tick)

THEOREM Spec => []<>IsCountCorrect

[jayaprabhakar k]

So what does the WF and SF do? I thought it is more like nudging to ensure some steps always happens and not stuck with stuttering.

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/h4nrF-pbor4/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/b8fbc1c0-b8bd-4a5d-9d07-b38e009abd7fn%40googlegroups.com.

[Hillel Wayne]

You're running into a fairly niche issue called "Machine Closure", where the action in your fairness condition isn't a subset of your Next formula. WF(Tick) says that if []ENABLED Tick, then Tick eventually happens. Since Tick doesn't have any unprimed variables in it, it's always enabled, but since it's not part of Next, it can never happen. So the Spec formula evaluates to false. You should see that no initial states are generated in the output.

It's a bit unintuitive, I know; see section 8.9 of Specifying Systems for a formal treatment.

H

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b8fbc1c0-b8bd-4a5d-9d07-b38e009abd7fn%40googlegroups.com.

[jayaprabhakar k]

Thanks. I'll try to read Specifying Systems. In any case, I assume I should not add WF_vars(Tick). To make things work, I removed the WF_vars(Tick), made the correct tick. And used a seq < BUFFER_SIZE as a precondition to  Add/Remove. Then it all worked. 

I assume that is the correct way to model. For the record, this is my final working model. Please correct me if I'm wrong.

-------------------------- MODULE EventualCounter --------------------------

EXTENDS Naturals,FiniteSets

CONSTANT MAX_ELEMENTS, BUFFER_SIZE

VARIABLES elements, count, seq

vars == <<elements, count, seq>>

Init == /\ elements = {}

        /\ count = 0

        /\ seq = 0

Add == /\ \E e \in 1..MAX_ELEMENTS:

              /\ e \notin elements

              /\ seq < BUFFER_SIZE

              /\ elements' = elements \union {e}

              /\ seq' =  seq + 1

              /\ UNCHANGED count

                                

Remove == /\ \E e \in elements:

                 /\ seq < BUFFER_SIZE

                 /\ seq > 0

                 /\ elements' = elements \ {e}

                 /\ seq' =  seq + 1

                 /\ UNCHANGED count

Tick == /\ count' = Cardinality(elements)

        /\ seq' = 0

        /\ UNCHANGED <<elements>>

ConsistencyInvariant == \/ seq > 0

             \/ (count = Cardinality(elements))

               

IsCountCorrect == (count = Cardinality(elements))

             

Next == \/ Add

        \/ Remove

        \/ Tick  

Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

THEOREM Spec => []<>IsCountCorrect

-

On Fri, 6 Jan 2023 at 14:37, Hillel Wayne <hwa...@gmail.com> wrote:

You're running into a fairly niche issue called "Machine Closure", where the action in your fairness condition isn't a subset of your Next formula. WF(Tick) says that if []ENABLED Tick, then Tick eventually happens. Since Tick doesn't have any unprimed variables in it, it's always enabled, but since it's not part of Next, it can never happen. So the Spec formula evaluates to false. 

You should see that no initial states are generated in the output.

I actually see Init state generated.

 

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8068e6ef-e001-29c3-0554-5a668366e6fd%40gmail.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8068e6ef-e001-29c3-0554-5a668366e6fd%40gmail.com.

[jayaprabhakar k]

One clarification, to see if my understanding is correct.

In the final model, I used WF_vars(Next)as the liveness condition.  For this design to be implemented correctly, the system should guarantee the Next conditions are always eventually triggered. That means, either a new element must be added, removed or a tick has to be called. However, since guaranteeing a new element added/removed may not be possible because it depends on the user actions, the fairness condition should only be a Tick (WF_vars(Tick)). The next question is, what should go on vars? Tick doesn't update elements. So, should that just be WF_<<count,seq>>(Tick)? Or even, just WF_<<count>>(Tick) , because the only variable the implementation cares about is count. 

To should the difference, I tried,

Tick == \/ /\ count' = Cardinality(elements)

           /\ seq' = 0

           /\ UNCHANGED <<elements>>

        \/ /\ seq' = 0

           /\ UNCHANGED <<elements,count>>

        \/ /\ count' = Cardinality(elements)

           /\ UNCHANGED <<elements,seq>>

That is, even seq and count aren't guaranteed to be updated atomically. In that case, WF_<<count>>(Tick) works but WF_<<seq>>(Tick) doesn't.

Is my understanding on practical use of TLA+ design to be used for implementation? 

[Stephan Merz]

Hello,

if you think of Add and Remove as user-triggered actions you should indeed assume fairness of them only if you believe that the users of your system are diligent.

I am not sure I understand the new definition of Tick: it allows a behavior where, say, actions Add and the second disjunct of Tick alternate. So users keep adding elements but then seq is reset without updating the count variable. Such a behavior satisfies WF_seq(Tick) but count will never (again) be correct. The same behavior (a fortiori) satisfies WF_vars(Tick).

When you write WF_count(Tick) you force the first or third conjuncts of Tick to eventually occur, so count will be updated.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CA%2Bt%3DSiKB8D-PWX7jD7GrwTei4cUC4D4Um3geEG6%2BEUtPJR8k%2BA%40mail.gmail.com.

[jayaprabhakar k]

Thanks Stephan. Yes, you are right. The new definition of Tick, was only to demonstrate my understanding of WF/SF rules. I was just playing to understand how the fairness thing works. So, I was trying to change the variables list and the action list, and based on the results, I think I now understand. Since the Tick is the only one system controlled (kind of cron job), we can only assume fairness on them and the only thing we care about is count, only that should be listed, instead of blindly saying WF_vars(Next), BTB, how to read this statement `WF_<<count>>(Tick)` in plain english? 

[Stephan Merz]

I'd read it as "WF sub count Tick".

Also, if you really want to allow for these different subactions of Tick, it would probably make sense to define them as separate actions and then assume fairness conditions only for the relevant subaction(s). This will probably avoid subtle differences between the meanings of WF_vars(Tick1) and WF_x(Tick1) for individual variables x.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a37ec448-8d04-46e8-8640-565eec4fa0f1n%40googlegroups.com.