Re: [tlaplus] Strong fairness

On Wed, 13 Mar 2024 at 11:01, Stephan Merz <stephan.merz@xxxxxxxxx> 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

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 <jayaprabhakar@xxxxxxxxx> 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,

<ewd426-token-ring.png>

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:
<Screenshot 2024-03-13 at 1.57.15 AM.png>
<<
[
_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?

--
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%2B11pQwgXkCZdnB_q%3DNdS1XCVEumqd7tPLO%2B28R1%3Ddegg%40mail.gmail.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/747484B9-34E1-4FB8-BD3F-B2A58AC83A5A%40gmail.com.