[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Re: Check eventual consistency



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.

On Fri, Jan 6, 2023, 10:20 jayaprabhakar k <jayaprabhakar@xxxxxxxxx> wrote:
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



On Friday, January 6, 2023 at 8:47:31 AM UTC-8 hwa...@xxxxxxxxx wrote:

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

On 1/5/2023 5:42 PM, jayaprabhakar k wrote:
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? 


On Thursday, January 5, 2023 at 2:32:22 PM UTC-8 jayaprabhakar k wrote:
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?

 

--
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 on the web visit https://groups.google.com/d/msgid/tlaplus/afdae50c-9f3d-48b5-84b7-c7aa3ba561a9n%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/h4nrF-pbor4/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b8fbc1c0-b8bd-4a5d-9d07-b38e009abd7fn%40googlegroups.com.

--
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/CA%2Bt%3DSi%2BD8RXEEh7FzbcX0Wc-CeFhS3N%2BoEVivZ1VDGnYZSAXxA%40mail.gmail.com.