Strong fairness

[jayaprabhakar k]

Hi,

I am trying out Dijkstra's Self Stabilizing for Token ring algorithm.

https://muratbuffalo.blogspot.com/2022/10/checking-statistical-properties-of.html

The spec has two actions - CreateToken and PassToken. The spec as given, fails liveness property if N < M - 1. The trace looks reasonable.  

Looking at the state space, making these two actions as Strong Fair should fix the liveness issue, but it doesn't seem to.

Listing out all the states,

There are two cycles. The unstabilized cycle at the top in black and the stabilized cycle at the bottom in green.

1. Once the stable (green) nodes are reached, there is no way to reach an unstable (black) node.

2. From any unstable node, there is always a next state to the green node.
And, from every action here is Strong Fair, the link should be enabled infinitely often, and so one of the transitions should happen eventually.

The code is:
---

Init ==

    /\ c \in [ Node -> 0 .. M-1 ]

CreateToken ==

    (* Node 0 executes this action to inject new value into system *)

    /\ c [0] = c [N-1]

    /\ c' = [ c EXCEPT ![0] = (c[N-1]+ 1) % M ]

PassToken(i) ==

    (* Other nodes just copy value of the predecessor *)

    /\ i # 0

    /\ c [i] # c [i-1]

    /\ c' = [ c EXCEPT ![i] = c[i-1]]    

PassTokens ==

    \E i \in Node \ {0} : PassToken(i)

PassToken1 == c [1] # c [0] /\ c' = [ c EXCEPT ![1] = c[0]] 

PassToken2 == c [2] # c [1] /\ c' = [ c EXCEPT ![2] = c[1]] 

PassToken3 == c [3] # c [2] /\ c' = [ c EXCEPT ![3] = c[2]]

---------------------------------------------------------------------------------------

Next == 

    \/ CreateToken

    \/ PassToken1

    \/ PassToken2

    \/ PassToken3

Spec == Init /\ [][Next]_vars /\ SF_vars(PassToken1) /\ SF_vars(PassToken2) /\ SF_vars(PassToken3)  /\ SF_vars(CreateToken)    

---------------------------------------------------------------------------------------

UniqueToken ==

    \E i \in 0 .. N :                           \* unique token at i (or i=N => token is at 0)

       /\ \A j \in 0..i-1: c[j]= c[0]           \* before i all c equals c[0] 

       /\ \A j \in i..N-1: c[j]= (c[0]-1) % M   \* after i all c following c[0]

(* Stabilization property *)

Stab  == <>[]UniqueToken

---

The error trace:

<<
[
 _TEAction |-> [
   position |-> 1,
   name |-> "Initial predicate",
   location |-> "Unknown location"
 ],
c |-> (0 :> 0 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 0)
],
[
 _TEAction |-> [
   position |-> 2,
   name |-> "CreateToken",
   location |-> "line 30, col 5 to line 31, col 47 of module TokenRing"
 ],
c |-> (0 :> 1 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 0)
],
[
 _TEAction |-> [
   position |-> 3,
   name |-> "PassToken3",
   location |-> "line 44, col 15 to line 44, col 59 of module TokenRing"
 ],
c |-> (0 :> 1 @@ 1 :> 0 @@ 2 :> 1 @@ 3 :> 1)
],
[
 _TEAction |-> [
   position |-> 4,
   name |-> "PassToken2",
   location |-> "line 43, col 15 to line 43, col 59 of module TokenRing"
 ],
c |-> (0 :> 1 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 1)
],
[
 _TEAction |-> [
   position |-> 5,
   name |-> "PassToken1",
   location |-> "line 42, col 15 to line 42, col 59 of module TokenRing"
 ],
c |-> (0 :> 1 @@ 1 :> 1 @@ 2 :> 0 @@ 3 :> 1)
],
[
 _TEAction |-> [
   position |-> 6,
   name |-> "CreateToken",
   location |-> "line 30, col 5 to line 31, col 47 of module TokenRing"
 ],
c |-> (0 :> 0 @@ 1 :> 1 @@ 2 :> 0 @@ 3 :> 1)
],
[
 _TEAction |-> [
   position |-> 7,
   name |-> "PassToken3",
   location |-> "line 44, col 15 to line 44, col 59 of module TokenRing"
 ],
c |-> (0 :> 0 @@ 1 :> 1 @@ 2 :> 0 @@ 3 :> 0)
],
[
 _TEAction |-> [
   position |-> 8,
   name |-> "PassToken2",
   location |-> "line 43, col 15 to line 43, col 59 of module TokenRing"
 ],
c |-> (0 :> 0 @@ 1 :> 1 @@ 2 :> 1 @@ 3 :> 0)
]
>>

What am I missing here? 

[divyanshu ranjan]

Looking at the state trace, it seems to me that M = 2 and N = 3 which does n't satisfy M >= N requirement.

--
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/CA%2Bt%3DSi%2B11pQwgXkCZdnB_q%3DNdS1XCVEumqd7tPLO%2B28R1%3Ddegg%40mail.gmail.com.

[jayaprabhakar k]

Yes, (Actually M=2 and N = 4) But the requirement that M >= N -1 is not a liveness temporal property set in the spec anywhere. It's just the model checking fails for those cases.

I am trying to understand why, because with strong fairness on all the actions, this cycle with unstable states should be broken and jump into the stable states. 

For example, from the init state [0, 0, 1, 0], which is part of the cycle, if the PassToken2 or PassToken3 were executed, the system would have reached either [0, 0, 0, 0] or [0, 0, 1, 1] both are stable. Since both these are Strong Fair, and the action gets enabled infinitely often (because of the cycle), it should have taken at least once.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAL9hw27Wg%3Dz7gJOQGQ_tt%3Dcr_Lnnw-mVHgbSqanURbzxcR4jcA%40mail.gmail.com.

[divyanshu ranjan]

Ah. Off by one error.

In your state trace, you can see that in the mentioned cycle, each of Next action is infinitely often enabled

and that step infinitely often occurs. So it satisfies all strong fairness requirements.

As about diagram with two cycle, It does n't have to break away from unstable cycle to satisfy all strong

fairness requirement as shown in the error trace. For example in state [0, 0, 1, 0] Passtoken2 is enabled

and it gets satisfied in transition [1,0,1,1] to [1,0,0,1].   

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

[Stephan Merz]

Thanks for the nice visualization, which allows one to understand what’s going on.

Each of the actions CreateToken, PassToken(1), PassToken(2), and PassToken(3) is taken along the counter-example that TLC produces, so clearly your strong fairness hypotheses are satisfied in the counter-example, while stabilization does not occur.

If you’d like to ensure that the black subgraph is left eventually, you’ll certainly need a stronger fairness assumption. If I understand correctly, the green states correspond to those in which UniqueToken holds. This suggests defining

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

which requires that stabilization will occur given that it is "often enough" possible to achieve stabilization in a single step. Of course, it is entirely unclear how you would implement such a fairness condition. The beauty of Dijkstra’s algorithm is that it ensures that for M ≥ N-1, a simple progress assumption (i.e., WF_vars(Next)) is enough to ensure stabilization.

Stephan

On Mar 13, 2024, at 09:58, jayaprabhakar k <jayapr...@gmail.com> wrote:

Hi,

I am trying out Dijkstra's Self Stabilizing for Token ring algorithm.

https://muratbuffalo.blogspot.com/2022/10/checking-statistical-properties-of.html

The spec has two actions - CreateToken and PassToken. The spec as given, fails liveness property if N < M - 1. The trace looks reasonable.  

Looking at the state space, making these two actions as Strong Fair should fix the liveness issue, but it doesn't seem to.

Listing out all the states,

---

The error trace:

[Stephan Merz]

I should add two points:

1. In addition to the strong fairness condition that I indicated, you'll also need WF_vars(Next) in order to rule out behaviors that stutter in a state where immediate stabilization is impossible.

2. I suspect that for larger values of M or N, the fairness condition will not be sufficient because stabilization may require more than one step – i.e., the "green cycle" may be further away from the "black cycle(s)". The point was really just to emphasize that I don't see how to state the relevant fairness hypotheses in a way that the conditions can be checked locally by some node.

Stephan

[jayaprabhakar k]

On Wed, 13 Mar 2024 at 11:01, Stephan Merz <stepha...@gmail.com> wrote:

Thanks for the nice visualization, which allows one to understand what’s going on.

Each of the actions CreateToken, PassToken(1), PassToken(2), and PassToken(3) is taken along the counter-example that TLC produces, so clearly your strong fairness hypotheses are satisfied in the counter-example, while stabilization does not occur.

Thanks for the clarification.  I was incorrectly assuming that fairness would be considered for each state the system can be in, and that doesn't seem to be the case. Instead, it looks like for fairness, it only matters whether the action is executed at least once in the cycle. 

 

If you’d like to ensure that the black subgraph is left eventually, you’ll certainly need a stronger fairness assumption. If I understand correctly, the green states correspond to those in which UniqueToken holds. This suggests defining

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

which requires that stabilization will occur given that it is "often enough" possible to achieve stabilization in a single step. Of course, it is entirely unclear how you would implement such a fairness condition.

True, in practice, I don't think we could implement a guarantee SF_vars(Next /\ UniqueToken’). That said, I am thinking through how to guarantee strong fairness in general. But it looks like, in most practical solutions, adding a random delay/jitter to these operations to avoid timing attacks, and that will ensure eventually these links will be taken. I understand, TLA+ doesn't support modeling these.

Thanks for the explanation, it's really helpful

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/747484B9-34E1-4FB8-BD3F-B2A58AC83A5A%40gmail.com.