gossa_v3.tla

gossa_v3.tla

--------------------------- MODULE gossa_v3 ---------------------------

(*
To see how a state constraint can break liveness try running this spec
twice with:
- NodeCount=2:
- Use the LivenessSpec temporal formula.
- Uncomment the line '/\ generation[source] < 4' in Gossip.
  This line adds an artificial rule that will prevent convergence.
Run 1:
- Do not apply the StateConstraint and see that the liveness 
  property is violated as expected.
Run 2:
- Apply the StateConstraint this time and see that the liveness
  property is no longer violated. The state constraint broke the liveness
  property check, and silently.
*)

EXTENDS Naturals

CONSTANTS NodeCount
VARIABLES running,
          peer_status,
          generation

vars == <<running, peer_status, generation>>

Nodes == 1..NodeCount

\* Node peer states
Alive == 1
Dead == 2
          
Init ==
    /\ running     = [node \in Nodes |-> TRUE]
    /\ peer_status = [node1 \in Nodes |->
                        [node2 \in Nodes |-> 
                            [generation |-> 1,
                             status     |-> Alive]]]
    /\ generation  = [node \in Nodes |-> 1]

Highest(peer1, peer2) ==
    CASE peer1.generation > peer2.generation -> peer1
      [] peer2.generation > peer1.generation -> peer2
      [] peer1.status > peer2.status -> peer1
      [] OTHER -> peer2
    
MergePeerState(local_node, local_ps, remote_ps) ==
    [node \in Nodes |->
        CASE
          \* CASE --- This is node is a peer so we select 
          \*          the higher precedence of the two ---
             node /= local_node ->
                Highest(local_ps[node], remote_ps[node])
          \* CASE --- This node is the local node and the remote
          \*          believes it is dead so it increments its
          \*          generation --- 
          [] /\ remote_ps[node].generation = generation[node]
             /\ remote_ps[node].status = Dead ->
                [generation |-> generation[node] + 1,
                 status     |-> Alive]
          \* CASE --- This node is the local node and the remote
          \*          believes it is alive so it keeps its local
          \*          knowledge of itself ---
          [] OTHER -> 
                local_ps[node]]
            
\*****************************************************************
\* ACTIONS
\*****************************************************************

Gossip ==
    \E source, dest \in Nodes :
        LET gossip_sent      == peer_status[source]
            merged_on_dest   == MergePeerState(
                                    dest, 
                                    peer_status[dest],
                                    gossip_sent)
            gossip_replied   == merged_on_dest
            merged_on_source == MergePeerState(
                                    source,
                                    peer_status[source],
                                    gossip_replied)
            new_gen_dest     == merged_on_dest[dest].generation
            new_gen_source   == merged_on_source[source].generation
        IN
\*            /\ generation[source] < 4 \* Uncomment to see how the state constraint breaks liveness
            /\ running[source] = TRUE
            /\ running[dest] = TRUE
            /\ peer_status[source] /= peer_status[dest]
            /\ peer_status' = [peer_status EXCEPT ![dest]   = merged_on_dest,
                                                  ![source] = merged_on_source]
            /\ generation' = [generation EXCEPT ![dest]   = new_gen_dest,
                                                ![source] = new_gen_source]
            /\ UNCHANGED running

Die ==
    \E node \in Nodes :
        /\ running[node] = TRUE
        /\ running' = [running EXCEPT ![node] = FALSE]
        /\ UNCHANGED << peer_status, generation >>
        
Start ==
    \E node \in Nodes :
        /\ running[node] = FALSE
        /\ LET new_gen == generation[node] + 1
           IN  
              /\ running' = [running EXCEPT ![node] = TRUE]
              /\ generation' = [generation EXCEPT ![node] = new_gen]
              /\ peer_status' = [peer_status EXCEPT ![node][node].generation = new_gen]

CorrectlyDetectDeadNode ==
    \E local, remote \in Nodes :
        /\ local /= remote
        /\ running[local] = TRUE
        /\ running[remote] = FALSE
        /\ peer_status[local][remote].status = Alive
        /\ peer_status' = [peer_status EXCEPT ![local][remote].status = Dead]
        /\ UNCHANGED << running, generation >>
        
FalselyDetectDeadNode ==
    \E local, remote \in Nodes :
        /\ local /= remote
        /\ running[local] = TRUE
        /\ running[remote] = TRUE
        /\ peer_status[local][remote].status = Alive
        /\ peer_status' = [peer_status EXCEPT ![local][remote].status = Dead]
        /\ UNCHANGED << running, generation >>        

Next ==
    \/ Gossip
    \/ Die
    \/ CorrectlyDetectDeadNode
    \/ FalselyDetectDeadNode
    \/ Start

StateConstraint ==
    \A node \in Nodes : generation[node] < 3

\* SAFETY PROPERTIES ------------        

TypeOK ==
    /\ running \in [Nodes -> BOOLEAN]
    /\ peer_status \in [Nodes ->
                           [Nodes ->
                                [generation: Nat,
                                 status: {Alive, Dead}]]]
    /\ generation \in [Nodes -> Nat]
    
ValidGeneration ==
    ~\E node \in Nodes :
        /\ generation[node] /= peer_status[node][node].generation    

\* LIVENESS PROPERTIES ------------        

Converged ==
    ~\E local, remote \in Nodes :
       /\ running[local] = TRUE 
       /\ \/ /\ running[remote] = TRUE
             /\ \/ peer_status[local][remote].status = Dead 
                \/ peer_status[local][remote].generation /= generation[remote]
          \/ /\ running[remote] = FALSE
             /\ peer_status[local][remote].status = Alive 
    
EventuallyConverges ==
    ~Converged ~> Converged
    
Liveness ==
    WF_vars(\/ Gossip
            \/ CorrectlyDetectDeadNode)
    
\* Temporal formula    
Spec == Init /\ [][Next]_vars
LivenessSpec == Init /\ [][Next]_vars /\ Liveness    

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

init

Init ==
    /\ running     = [node \in Nodes |-> TRUE]
    /\ peer_status = [node1 \in Nodes |->
                        [node2 \in Nodes |-> 
                            [generation |-> 1,
                             status     |-> Alive]]]
    /\ generation  = [node \in Nodes |-> 1]

merge

Highest(peer1, peer2) ==
    CASE peer1.generation > peer2.generation -> peer1
      [] peer2.generation > peer1.generation -> peer2
      [] peer1.status > peer2.status -> peer1
      [] OTHER -> peer2
    
MergePeerState(local_node, local_ps, remote_ps) ==
    [node \in Nodes |->
        CASE
          \* CASE --- This is node is a peer so we select 
          \*          the higher precedence of the two ---
             node /= local_node ->
                Highest(local_ps[node], remote_ps[node])
          \* CASE --- This node is the local node and the remote
          \*          believes it is dead so it increments its
          \*          generation --- 
          [] /\ remote_ps[node].generation = generation[node]
             /\ remote_ps[node].status = Dead ->
                [generation |-> generation[node] + 1,
                 status     |-> Alive]
          \* CASE --- This node is the local node and the remote
          \*          believes it is alive so it keeps its local
          \*          knowledge of itself ---
          [] OTHER -> 
                local_ps[node]]

start

Start ==
    \E node \in Nodes :
        /\ running[node] = FALSE
        /\ LET new_gen == generation[node] + 1
           IN  
              /\ running' = [running EXCEPT ![node] = TRUE]
              /\ generation' = [generation EXCEPT ![node] = new_gen]
              /\ peer_status' = [peer_status EXCEPT ![node][node].generation = new_gen]