gossa_v4.tla

gossa_v4.tla

--------------------------- MODULE gossa_v4 ---------------------------

(*
This version uses enabling conditions to limit the state space
while preserving the ability of TLC to effectively check
the liveness properties.
The constant MaxGeneration defines the inclusive maximum 
generation value that can be reached by any given node. The
limit is applied on Start because even though this is a recovery
action, it doesn't affect the lone liveness property of this
spec and I want to be as liberal as possible with node deaths.
It is also applied to FalselyDetectDeadNode to which is a
perturbation that causes many follow on actions to converge
on the true state of the falsely accused.
You can also try uncommenting the lines:
/\ new_gen_dest < MaxGeneration
/\ new_gen_source < MaxGeneration
in Gossip to see the affect on liveness of limiting a
recovery action.
*)

EXTENDS Naturals

CONSTANTS NodeCount, MaxGeneration
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
            /\ running[source] = TRUE
            /\ running[dest] = TRUE
\*            /\ new_gen_dest < MaxGeneration    \* <----- Uncomment to break liveness
\*            /\ new_gen_source < MaxGeneration  \* <----- Uncomment to break liveness
            /\ 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
        /\ generation[node] < MaxGeneration \* <----- Limit generation
        /\ 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
        /\ generation[remote] < MaxGeneration \* <--- Limit generation
        /\ peer_status' = [peer_status EXCEPT ![local][remote].status = Dead]
        /\ UNCHANGED << running, generation >>        

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

\* 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    

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

limit_falsely_detect

FalselyDetectDeadNode ==
    \E local, remote \in Nodes :
        /\ local /= remote
        /\ running[local] = TRUE
        /\ running[remote] = TRUE
        /\ generation[remote] <= 2 \* <--- Limit generation
        ...

limit_gossip

Gossip ==
    \E source, dest \in Nodes :
        LET gossip_sent      == peer_status[source]
            ...
            new_gen_dest     == merged_on_dest[dest].generation
            new_gen_source   == merged_on_source[source].generation
        IN
            /\ running[source] = TRUE
            /\ running[dest] = TRUE
            /\ new_gen_dest <= 2     \* <----- limit generation on dest
            /\ new_gen_source <= 2   \* <----- limit generation on source
            /\ peer_status[source] /= peer_status[dest]
            ...

limit_start

Start ==
    \E node \in Nodes :
        /\ running[node] = FALSE
        /\ generation[node] <= 2 \* <----- Limit generation
        /\ 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]