Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Log repair tla+ specification
---- MODULE LogRepair ----
EXTENDS TLC, Naturals
CONSTANTS Process, MaxLog
ASSUME Process \in SUBSET Nat
ASSUME MaxLog \in Nat \ {0}
VARIABLES state, missings, max_logs, logs, decisions
vars == <<state, missings, max_logs, logs, decisions>>
Init ==
/\ state = [ i \in Process |-> "Running" ]
/\ missings = [ i \in Process |-> {} ]
/\ logs = [ i \in Process |-> {} ]
/\ max_logs = [ i \in Process |-> 0 ]
/\ decisions = {}
(*******************************************************************)
(* There's a consensus on the next log_id, leader decides candidate. *)
(* If the leader fails, paxos/raft ensure that this values will always *)
(* be chosen for log_id. Since we don't model the consensus itself, *)
(* any decided value remain until the end. *)
(*******************************************************************)
Decide(p, candidate) ==
/\ state[p] = "Running"
/\ max_logs[p] + 1 = candidate
/\ logs' = [logs EXCEPT ![p] = logs[p] \union {candidate}]
/\ max_logs' = [max_logs EXCEPT ![p] = candidate]
/\ decisions' = decisions \union {candidate}
/\ UNCHANGED <<state, missings>>
(*******************************************************************)
(* Any currently running node (it thinks it is up-to-date) receives a decision result. *)
(* Either the decision is the log next value, and every keeps on going. *)
(* Or, the node is not up to date and considers itself in "Repair" state. *)
(*******************************************************************)
Learn(p, l) ==
/\ state[p] = "Running"
/\ max_logs[p] = l
/\ \E learned \in decisions:
\/ /\ learned = l
/\ max_logs' = [max_logs EXCEPT ![p] = learned]
/\ logs' = [logs EXCEPT ![p] = logs[p] \union {learned}]
/\ UNCHANGED <<state, missings, decisions>>
\/ /\ learned > l
/\ state' = [state EXCEPT ![p] = "Repair"]
/\ max_logs' = [max_logs EXCEPT ![p] = learned]
/\ missings' = [missings EXCEPT ![p] = l..learned]
/\ logs' = [logs EXCEPT ![p] = logs[p] \union {learned}]
/\ UNCHANGED <<decisions>>
(*******************************************************************)
(* Node in repair state learns (through the consensus algorithm *)
(* implementation details) some missing value. *)
(* Once the last missing value is recovered the node consider itself *)
(* running again. *)
(*******************************************************************)
Repair(p, l) ==
/\ state[p] = "Repair"
/\ l \in missings[p]
/\ \E decision \in decisions:
/\ decision = l
/\ \/ /\ missings[p] = {l}
/\ missings' = [missings EXCEPT ![p] = missings[p] \ {l}]
/\ logs' = [logs EXCEPT ![p] = logs[p] \union {l}]
/\ state' = [state EXCEPT ![p] = "Running"]
/\ UNCHANGED <<decisions, max_logs>>
\/ /\ missings[p] /= {l}
/\ missings' = [missings EXCEPT ![p] = missings[p] \ {l}]
/\ logs' = [logs EXCEPT ![p] = logs[p] \union {l}]
/\ UNCHANGED <<state, decisions, max_logs>>
----
Next ==
\/ \E l \in 1..MaxLog: \E p \in Process:
\/ Learn(p, l)
\/ Decide(p, l)
\/ Repair(p, l)
\/ UNCHANGED vars
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
----
(*******************************************************************)
(* eventually every process logged every values and is running *)
(*******************************************************************)
EveryRunningProcessLearnAllValues == <>(\A p \in Process: state[p] = "Running" /\ logs[p] = 1..MaxLog)
(*******************************************************************)
(* There is always a running node, such as progress is always garanteed *)
(* by the consensus algorithm. *)
(*******************************************************************)
AtLeastOneProcessIsRunning == [](\E s \in DOMAIN state: state[s] = "Running")
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment