---
source: libtlafmt/tests/format.rs
expression: output
input_file: libtlafmt/tests/corpus/EnvironmentController.tla
---
------------------------- MODULE EnvironmentController -------------------------
(* An encoding of a parameterized and partially synchronous model of the eventually
perfect failure detectors with crash faults from:
[1] Chandra, Tushar Deepak, and Sam Toueg. "Unreliable failure detectors for
reliable distributed systems." Journal of the ACM (JACM) 43.2 (1996): 225-267.
Igor Konnov, Thanh Hai Tran, Josef Wider, 2018
This file is a subject to the license that is bundled together with this package
and can be found in the file LICENSE. *)
(* - This specification instances two other specs, Age_Channel.tla for the communication
system, and EPFailureDetector.tla for behaviors of correct processes.
- Every message sent by some process is wrapped into a box with an age which shows
how long this message have been in transit. Boxes for messages which were sent
but have not been delivered are stored in a variable inTransit.
- Messages which are delivered in the current transition are stored in a variable
inDelivery.
- The system tracks what last transition a process takes, and how long some correct
process has not taken a transition. The information are saved in variables moved
and procPause, respectively. Crashes are also tracked.
- Every process has its own local clock which is localClock[i].
- Every correct process repeatedly sends "alive" messages to other processes, and
repeatedly make predictions about failures. However, a process cannot send and
predict at the same time. A process can receive messages when it does not execute
neither the operation SEND nor the operation PREDICT.
- "alive" messages are created by calling the operator MakeAliveMsgsForAll in
EPFailureDetector, and then stored in outgoingMessages.
- In this specification, a correct process sends "alive" messages to others at every
SendPoint tick of its local clock, and makes predictions about failures at every
PredictPoint tick of its local clock. Formally, we have that
a) localClock[i] % SendPoint = 0 /\ localClock[i] % PredictPoint # 0: a process
executes the operation Send
b) localClock[i] % SendPoint # 0 /\ localClock[i] % PredictPoint = 0: a process
executes the operation Predict
c) \/ localClock[i] % SendPoint = 0 /\ localClock[i] % PredictPoint = 0
\/ localClock[i] % SendPoint # 0 /\ localClock[i] % PredictPoint # 0 : a process
executes the operation Receive
- The predictions are saved in a variable suspected. If j \in suspected[i], a process
p_i suspects that a process p_j crashed.
- Every process p_i has a waiting time, called delta[i][j], for hearing some messages
for other process p_j. Moreover, a process tracks how long it hasn't receive any
message from p_j, and stores the information in a variable fromLastHeard[i][j].
- When a process p_i executes the action Predict, if p_i hasn't received any message
from p_j for a too long period, e.g. fromLastHeard[i][j] > delta[i][j], p_i puts
p_j into its suspected list.
o The keypoints in this specification is the way we encode the environmental clock,
and local clocks of processes. This encoding technique makes our system become
a finite one, if all parameters are fixed.
1/ In this specification, instead of directly encoding the environmental clocks,
we focus on their effects on variables describing message delay, and relative
speeds of processes. The action EnvTick simulates an event of a global tick.
When the action EnvTick is executed, a box with a message inside attains a
new age, and every pause of a process p_i, named procPause[i], is increased
by 1.
2/ Every local lock in this specification has a finite domain, instead of a
infinite one. Whenever the value of its local clock is greater than SendPoint,
PredictPoint, and delta[i][j], the local clock is reset to 0. Because of the
constraints about message delay and relative speeds of different processes in
partial synchrony, the upper bound of local clocks exists.
3/ After fromLastHeard[i][j] is greated than delta[i][j], we don't need to
increase fromLastHeard[i][j].
+ We have used TLC to check the correctness of Strong Completeness and Eventually
Strong Accuracy in small instances
- Strong Completeness: Eventually every process that crashes is permanently
suspected by every correct process.
- Eventually Strong Accuracy: There is a time after which correct processes
are not suspected by any correct process.
- Case N = 3, T = 1, d0 = 2, SendPoint = 2, PredictPoint = 3, DELTA = PHI = 1:
TLC spends more than 2 hours (from 11:17 to 13:26) verifying these properties.
o PROBLEMS with TLC: I believe that PHIConstraint and PHIConstraint1 are equivalent.
However, whenever I check this specification with PHIConstraint1, TLC shows an
error: "Too many possible next states for the last state in the trace." I guess
that the reasons are from optimizations for disjunctions. *)
EXTENDS Integers, TLC
CONSTANT
N, (* The number of processes *)
T, (* The maximum number of failures *)
d0, (* The default time-out interval for all delta(p)(q) *)
SendPoint, (* Every correct process sends alive messages to others at every
SendPoint ticks of its local clock. *)
PredictPoint, (* Every correct process makes predictions about failures at every
PredictPoint ticks of its lock clock.
Assume that SendPoint # PredictPoint since a process cannot both
send alive messages and receive messages in one transition. *)
DELTA, (* For the constraint of message delay in partial synchrony. *)
PHI (* For the constraint of relative speeds of different processes in
partial synchrony. *)
(* Assumptions about the constraints in our system.
- SendPoint # PredictPoint: a process cannot both send messages and
receive messages in one transition.
- PredictPoint % SendPoint # 0 /\ SendPoint % PredictPoint # 0 :
the operation Predict cannot subsume the operation Predict and vice versa. *)
ASSUME /\ 0 < PredictPoint /\ 0 < SendPoint
/\ PredictPoint % SendPoint # 0 /\ SendPoint % PredictPoint # 0
Proc == 1..N (* A set of processes *)
VARIABLES
inTransit, inDelivery, (* For the communication system: spec Age_Channel *)
suspected, delta, fromLastHeard, (* For correct detectors: spec EPFailureDetector *)
localClock, outgoingMessages,
(* For the environment: the current spec EnvironmentController. *)
procPause, (* How long a process p_i has not taken a transition. *)
moved, (* The last transition that a process p_i take. The initial values are
INIT. After every global tick, moved'[i] is assigned "NO" for every
process. "NO" here means that a process has not taken a transition.
After a process p_i makes a transition, moved'[i] is assigned the
transition name which are SEND, RECEIVE, PREDICT, or CRASH. *)
failed, (* failed[i] = TRUE: a process p_i crashed. *)
F (* A number of current failures *)
(* A set of messages sent by correct processes *)
Messages == [from: Proc, to: Proc, type: {"alive"}]
(* Whenever a message is picked up, the communication system puts this message into
a box with an age. The age shows how long a message has been in transit. The field
"content" points to a message. *)
Boxes == [content: Messages, age: Int]
(* - maxAge is an estimated upper bound of how long a message in transit. In other
word, this constant should be a maximum age of above boxes.
- maxDelta is also an estimated upper bound of delta[i][j] for all i and j. *)
K == ((SendPoint * PredictPoint * PHI) \div DELTA) + 1
maxAge == K * (SendPoint * PredictPoint * PHI)
maxDelta == maxAge
CommChan == INSTANCE Age_Channel (* The communication system *)
Detector == INSTANCE EPFailureDetector (* Failure detectors *)
(* All variables *)
vars == << inTransit, inDelivery,
suspected, delta, fromLastHeard, localClock, outgoingMessages,
procPause, moved, failed, F >>
(* Variables for the communication system *)
chanVars == << inTransit, inDelivery >>
(* Variables for the specification EPFailureDetector which describes behaviors of
correct processes, *)
procVars == << suspected, delta, fromLastHeard, localClock, outgoingMessages >>
(* Variables for the environment *)
envVars == << procPause, moved, failed, F >>
(* All Names of processes' transitions *)
Actions == {"NO", "INIT", "SEND", "RECEIVE", "PREDICT", "CRASH"}
(* Initialization *)
Init ==
/\ CommChan!Init
/\ Detector!Init
/\ procPause = [i \in Proc |-> 0] (* No pauses *)
/\ moved = [i \in Proc |-> "INIT"] (* Every process finishes the initialization. *)
/\ failed = [i \in Proc |-> FALSE] (* No failures *)
/\ F = 0 (* No failures *)
(* A process p_i crashes. *)
Crash ==
\E i \in Proc:
/\ failed[i] = FALSE
/\ F < T
/\ failed' = [failed EXCEPT ![i] = TRUE]
/\ F' = F + 1
/\ moved' = [moved EXCEPT ![i] = "CRASH"] (* Required by SomeLocallyTicked *)
/\ procPause' = [procPause EXCEPT ![i] = - 1]
/\ UNCHANGED chanVars
/\ UNCHANGED procVars
(* At every global tick, at least one correct process makes a transition. *)
SomeLocallyTicked ==
\E p \in Proc: moved[p] /= "CRASH" /\ moved[p] /= "NO"
(* A new tick of the environmental clock.
- 1st conj: The global clock cannot have a new tick if no correct process makes
a transition in the last global tick.
- 2st conj: Every box's age increases by 1.
- 3nd conj: Reset moved. No processes have not taken a transition in this tick.
- 4rd conj: Every pause is increased by 1. If a correct process p_i makes a
transition later but still in this global tick, its procPause are
reset to 0. *)
EnvTick ==
/\ SomeLocallyTicked
/\ CommChan!AttainAge
/\ moved' = [i \in Proc |-> "NO"]
/\ procPause' = [i \in Proc |-> IF failed[i] = FALSE
THEN procPause[i] + 1
ELSE - 1]
/\ UNCHANGED << failed, F >>
/\ UNCHANGED procVars
(* Only messages sent to correct processes are picked up. *)
OnlyMessagesForCorrectProcesses(msgs) == {m \in msgs: failed[m.to] = FALSE}
(* 1st disj: Even a process crashed, the associated messages are delivered to it.
If these messages are not removed from the communication system, the ages
of these messages will increase infinitely.
2nd disj: The behaviors of correct processes.
- A process can take a transition if t doesn't take any transition in the current
global tick.
- A process p_i can makes predictions about failures.
- A process p_i can send "alive" messages to all. First, p_i creates "alive" messages
for all, and put those messages to outgoingMessages[i]. Then, the communication
system picks up those messages.
- A process p_i can receive new messages. First, the environment nondeterministically
choose some messages and put those messages into inDelivery'. Then, a process p_i
receive those messages. *)
ProcTick ==
\E i \in Proc:
\/
/\ failed[i] = TRUE
/\ UNCHANGED envVars
/\ CommChan!Deliver(i) (* Some messages are delivery to a process p_i. *)
/\ UNCHANGED procVars (* However, p_i cannot receive those messages because
p_i crashed before. *)
\/
/\ failed[i] = FALSE
/\ moved[i] = "NO"
/\ procPause' = [procPause EXCEPT ![i] = 0] (* Reset procPause'[i]*)
/\ UNCHANGED << failed, F >>
/\
\/
/\ moved' = [moved EXCEPT ![i] = "PREDICT"]
/\ Detector!Predict(i)
/\ UNCHANGED chanVars
\/
/\ moved' = [moved EXCEPT ![i] = "SEND"]
/\ Detector!SendAlive(i)
/\ CommChan!Pickup(OnlyMessagesForCorrectProcesses(outgoingMessages'[i]))
\/
/\ moved' = [moved EXCEPT ![i] = "RECEIVE"]
/\ CommChan!Deliver(i)
/\ Detector!Receive(i, inDelivery')
(* Two constraints PHIConstraint and DELTAConstraint are respectively restrictions on
message delay and relative speeds of processes in partial synchronoy. We use these
constraints to filter out executions. Only executions satisfying these constraints
are allowed in the computation model of partial synchrony.
- PHIConstraint: In any contiguous subinterval containing PHI real-time steps,
every correct processor must take at least one step. In this specification,
this constraint is violated if there is a correct process such that the associated
procPause is greater then PHI.
- DELTAConstraint: If message m is placed in p_j’s buffer by some Send(m, p_j)
at a time s_1, and if p_j executes a Receive(p_j) at a time s_2 such that
s_2 >= s_1 + DELTA, then m must be delivered to pj at time s_2 or earlier.
This restriction is captured by the 1st conjunction in DELTAConstranti.
However, this constraint doesn't mention anything about messages sent to crashed
processes which cannot execute the operation Receive. In this specification,
we assume that the maximum delay of messages sent to crashed processes are DELTA
real-time steps. In other words, the maximum ages of associated boxes in transit
are DELTA. *)
PHIConstraint ==
\A i \in Proc: (failed' [i] = FALSE => procPause' [i] <= PHI) (* No errors happen *)
(* I believe that PHIConstraint and PHIConstraint1 are equivalent. However, whenever I
check this specification with PHIConstraing1, TLC shows an error: "Too many possible
next states for the last state in the trace." I guess that the reasons are from
optimizations for disjunctions. *)
PHIConstraint1 ==
\A i \in Proc: (failed' [i] = TRUE \/ procPause' [i] <= PHI)
DELTAConstraint ==
\A i \in Proc:
/\ ((failed' [i] = FALSE /\ moved' [i] = "RECEIVE")
=> (\A m \in inTransit':
\/ m.content.to /= i
\/ m.age <= DELTA))
(*
/\ ((failed'[i] = TRUE)
=> ( \A m \in inTransit' : \/ m.content.to # i
\/ m.age <= DELTA ))
*)
(* Next transition *)
Next ==
/\
\/ Crash
\/ EnvTick
\/ ProcTick
/\ DELTAConstraint
/\ PHIConstraint
(* The specification *)
Spec ==
/\ Init
/\ [][Next]_vars
/\ WF_vars(
/\
\/ EnvTick
\/ ProcTick
/\ DELTAConstraint
/\ PHIConstraint)
(* Type invariant *)
TypeOK ==
/\ CommChan!TypeOK
/\ Detector!TypeOK
/\ procPause \in [Proc -> { - 1} \union 0..PHI]
/\ \A i \in Proc: failed[i] = TRUE <=> procPause[i] = - 1
/\ failed \in [Proc -> BOOLEAN ]
/\ moved \in [Proc -> Actions]
/\ F \in 0..T
/\ \A i, j \in Proc: 0 <= delta[i][j] /\ delta[i][j] <= maxDelta
/\ \A box \in inTransit: 0 <= box.age /\ box.age <= maxAge
/\ \A i, j \in Proc: fromLastHeard[i][j] <= maxAge
(*Two properties of an eventually perfect failure detector
- Strong Completeness: Eventually every process that crashes is permanently
suspected by every correct process.
- Eventually Strong Accuracy: There is a time after which correct processes
are not suspected by any correct process. *)
StrongCompleteness ==
<>[](\A j \in Proc: failed[j] = TRUE => (\A i \in Proc:
\/ failed[i] = TRUE
\/ j \in suspected[i]))
EventuallyStrongAccuracy ==
<>[](\A i, j \in Proc: (failed[i] = FALSE /\ failed[j] = FALSE)
=> j \notin suspected[i])
================================================================================
\* Modification History
\* Last modified Tue Jun 12 17:49:08 CEST 2018 by tthai
\* Created Mon Jun 04 13:20:35 CEST 2018 by tthai