|
| 1 | +----------------------------- MODULE Sailfish ----------------------------- |
| 2 | + |
| 3 | +(**************************************************************************************) |
| 4 | +(* This is a high-level specification of the Sailfish and Sailfish++ (also called *) |
| 5 | +(* signature-free Sailfish) algorithms. At the level of abstraction of this *) |
| 6 | +(* specification, the differences between the two algorithms are not visible. *) |
| 7 | +(**************************************************************************************) |
| 8 | + |
| 9 | +EXTENDS Integers, FiniteSets, Sequences |
| 10 | + |
| 11 | +CONSTANTS |
| 12 | + N \* The set of all nodes |
| 13 | +, F \* The set of Byzantine nodes |
| 14 | +, R \* The set of rounds |
| 15 | +, IsQuorum(_) \* Whether a set is a quorum (i.e. cardinality >= n-f) |
| 16 | +, IsBlocking(_) \* Whether a set is a blocking set (i.e. cardinality >= f+1) |
| 17 | +, Leader(_) \* operator mapping each round to its leader |
| 18 | +, GST \* the first round in which the system is synchronous |
| 19 | + |
| 20 | +ASSUME \E n \in R : R = 1..n \* rounds start at 1; 0 is used as default placeholder |
| 21 | + |
| 22 | +INSTANCE BlockDag \* Import definitions related to DAGs of blocks |
| 23 | + |
| 24 | +(**************************************************************************************) |
| 25 | +(* Now we specify the algorithm in the PlusCal language. *) |
| 26 | +(**************************************************************************************) |
| 27 | +(*--algorithm Sailfish { |
| 28 | + variables |
| 29 | + vs = {Genesis}, \* the vertices of the DAG |
| 30 | + es = {}; \* the edges of the DAG |
| 31 | + define { |
| 32 | + dag == <<vs, es>> |
| 33 | + NoLeaderVoteQuorum(r, vertices, add) == |
| 34 | + LET NoLeaderVote == {v \in vertices : LeaderVertex(r-1) \notin Children(dag, v)} |
| 35 | + IN IsQuorum({Node(v) : v \in NoLeaderVote} \cup add) |
| 36 | + } |
| 37 | + process (correctNode \in N \ F) |
| 38 | + variables |
| 39 | + round = 0, \* current round; 0 means the node has not started execution |
| 40 | + log = <<>>; \* delivered log |
| 41 | + { |
| 42 | +l0: while (TRUE) { |
| 43 | + if (round = 0) { \* start the first round r=1 |
| 44 | + round := 1; |
| 45 | + vs := vs \cup {<<self, 1>>}; |
| 46 | + es := es \cup {<<<<self, 1>>, Genesis>>} |
| 47 | + } |
| 48 | + else { \* start a round r>1 |
| 49 | + with (r \in {r \in R : r > round}) |
| 50 | + with (deliveredVertices \in SUBSET {v \in vs : Round(v) = r-1}) { |
| 51 | + \* we enter a round only if we have a quorum of vertices: |
| 52 | + await IsQuorum({Node(v) : v \in deliveredVertices}); |
| 53 | + \* if this is after GST, we must have all correct vertices: |
| 54 | + await r >= GST => (N \ F) \subseteq {Node(v) : v \in deliveredVertices}; |
| 55 | + \* enter round r: |
| 56 | + round := r; |
| 57 | + \* if the r-1 leader does not reference the r-2 leader, |
| 58 | + \* then we must be sure the r-2 leader cannot commit: |
| 59 | + await LeaderVertex(r-1) \in deliveredVertices => |
| 60 | + \/ LeaderVertex(r-2) \in Children(dag, LeaderVertex(r-1)) |
| 61 | + \/ NoLeaderVoteQuorum(r-1, deliveredVertices, {}); |
| 62 | + \* if we are the leader, then we must include the r-1 leader or |
| 63 | + \* have evidence it cannot commit: |
| 64 | + if (Leader(r) = self) |
| 65 | + await \/ LeaderVertex(r-1) \in deliveredVertices |
| 66 | + \/ NoLeaderVoteQuorum(r, {v \in vs : Round(v) = r}, {self}); |
| 67 | + \* create a new vertex: |
| 68 | + with (newV = <<self, r>>) { |
| 69 | + vs := vs \cup {newV}; |
| 70 | + es := es \cup {<<newV, pv>> : pv \in deliveredVertices}; |
| 71 | + }; |
| 72 | + \* commit if there is a quorum of votes for the leader of r-2: |
| 73 | + if (r > 2) |
| 74 | + with (votesForLeader = {pv \in deliveredVertices : <<pv, LeaderVertex(r-2)>> \in es}) |
| 75 | + if (IsQuorum({Node(pv) : pv \in votesForLeader})) |
| 76 | + log := Linearize(dag, LeaderVertex(r-2)) |
| 77 | + } |
| 78 | + } |
| 79 | + } |
| 80 | + } |
| 81 | +(**************************************************************************************) |
| 82 | +(* Next comes our model of Byzantine nodes. Because the real protocol *) |
| 83 | +(* disseminates DAG vertices using reliable broadcast, Byzantine nodes cannot *) |
| 84 | +(* equivocate and cannot deviate much from the protocol (lest their messages *) |
| 85 | +(* be ignored). *) |
| 86 | +(**************************************************************************************) |
| 87 | + process (byzantineNode \in F) |
| 88 | + { |
| 89 | +l0: while (TRUE) { |
| 90 | + with (r \in R) |
| 91 | + with (newV = <<self, r>>) { |
| 92 | + when newV \notin vs; \* no equivocation |
| 93 | + if (r = 1) { |
| 94 | + vs := vs \cup {newV}; |
| 95 | + es := es \cup {<<newV, Genesis>>} |
| 96 | + } |
| 97 | + else |
| 98 | + with (delivered \in SUBSET {v \in vs : Round(v) = r-1}) { |
| 99 | + await IsQuorum({Node(v) : v \in delivered}); \* ignored otherwise |
| 100 | + vs := vs \cup {newV}; |
| 101 | + es := es \cup {<<newV, pv>> : pv \in delivered} |
| 102 | + } |
| 103 | + } |
| 104 | + } |
| 105 | + } |
| 106 | +}*) |
| 107 | +\* BEGIN TRANSLATION (chksum(pcal) = "c16dfa43" /\ chksum(tla) = "9cdbd4f5") |
| 108 | +\* Label l0 of process correctNode at line 42 col 9 changed to l0_ |
| 109 | +VARIABLES vs, es |
| 110 | + |
| 111 | +(* define statement *) |
| 112 | +dag == <<vs, es>> |
| 113 | +NoLeaderVoteQuorum(r, vertices, add) == |
| 114 | + LET NoLeaderVote == {v \in vertices : LeaderVertex(r-1) \notin Children(dag, v)} |
| 115 | + IN IsQuorum({Node(v) : v \in NoLeaderVote} \cup add) |
| 116 | + |
| 117 | +VARIABLES round, log |
| 118 | + |
| 119 | +vars == << vs, es, round, log >> |
| 120 | + |
| 121 | +ProcSet == (N \ F) \cup (F) |
| 122 | + |
| 123 | +Init == (* Global variables *) |
| 124 | + /\ vs = {Genesis} |
| 125 | + /\ es = {} |
| 126 | + (* Process correctNode *) |
| 127 | + /\ round = [self \in N \ F |-> 0] |
| 128 | + /\ log = [self \in N \ F |-> <<>>] |
| 129 | + |
| 130 | +correctNode(self) == IF round[self] = 0 |
| 131 | + THEN /\ round' = [round EXCEPT ![self] = 1] |
| 132 | + /\ vs' = (vs \cup {<<self, 1>>}) |
| 133 | + /\ es' = (es \cup {<<<<self, 1>>, Genesis>>}) |
| 134 | + /\ log' = log |
| 135 | + ELSE /\ \E r \in {r \in R : r > round[self]}: |
| 136 | + \E deliveredVertices \in SUBSET {v \in vs : Round(v) = r-1}: |
| 137 | + /\ IsQuorum({Node(v) : v \in deliveredVertices}) |
| 138 | + /\ r >= GST => (N \ F) \subseteq {Node(v) : v \in deliveredVertices} |
| 139 | + /\ round' = [round EXCEPT ![self] = r] |
| 140 | + /\ LeaderVertex(r-1) \in deliveredVertices => |
| 141 | + \/ LeaderVertex(r-2) \in Children(dag, LeaderVertex(r-1)) |
| 142 | + \/ NoLeaderVoteQuorum(r-1, deliveredVertices, {}) |
| 143 | + /\ IF Leader(r) = self |
| 144 | + THEN /\ \/ LeaderVertex(r-1) \in deliveredVertices |
| 145 | + \/ NoLeaderVoteQuorum(r, {v \in vs : Round(v) = r}, {self}) |
| 146 | + ELSE /\ TRUE |
| 147 | + /\ LET newV == <<self, r>> IN |
| 148 | + /\ vs' = (vs \cup {newV}) |
| 149 | + /\ es' = (es \cup {<<newV, pv>> : pv \in deliveredVertices}) |
| 150 | + /\ IF r > 2 |
| 151 | + THEN /\ LET votesForLeader == {pv \in deliveredVertices : <<pv, LeaderVertex(r-2)>> \in es'} IN |
| 152 | + IF IsQuorum({Node(pv) : pv \in votesForLeader}) |
| 153 | + THEN /\ log' = [log EXCEPT ![self] = Linearize(dag, LeaderVertex(r-2))] |
| 154 | + ELSE /\ TRUE |
| 155 | + /\ log' = log |
| 156 | + ELSE /\ TRUE |
| 157 | + /\ log' = log |
| 158 | + |
| 159 | +byzantineNode(self) == /\ \E r \in R: |
| 160 | + LET newV == <<self, r>> IN |
| 161 | + /\ newV \notin vs |
| 162 | + /\ IF r = 1 |
| 163 | + THEN /\ vs' = (vs \cup {newV}) |
| 164 | + /\ es' = (es \cup {<<newV, Genesis>>}) |
| 165 | + ELSE /\ \E delivered \in SUBSET {v \in vs : Round(v) = r-1}: |
| 166 | + /\ IsQuorum({Node(v) : v \in delivered}) |
| 167 | + /\ vs' = (vs \cup {newV}) |
| 168 | + /\ es' = (es \cup {<<newV, pv>> : pv \in delivered}) |
| 169 | + /\ UNCHANGED << round, log >> |
| 170 | + |
| 171 | +Next == (\E self \in N \ F: correctNode(self)) |
| 172 | + \/ (\E self \in F: byzantineNode(self)) |
| 173 | + |
| 174 | +Spec == Init /\ [][Next]_vars |
| 175 | + |
| 176 | +\* END TRANSLATION |
| 177 | + |
| 178 | +(**************************************************************************************) |
| 179 | +(* Basic type invariant: *) |
| 180 | +(**************************************************************************************) |
| 181 | +TypeOK == |
| 182 | + /\ \A v \in vs \ {<<>>} : |
| 183 | + /\ Node(v) \in N /\ Round(v) \in Nat \ {0} |
| 184 | + /\ \A c \in Children(dag, v) : Round(c) = Round(v) - 1 |
| 185 | + /\ \A e \in es : |
| 186 | + /\ e = <<e[1],e[2]>> |
| 187 | + /\ {e[1], e[2]} \subseteq vs |
| 188 | + /\ \A n \in N \ F : round[n] \in Nat |
| 189 | + |
| 190 | +(**************************************************************************************) |
| 191 | +(* Next we define the safety and liveness properties *) |
| 192 | +(**************************************************************************************) |
| 193 | + |
| 194 | +Agreement == \A n1,n2 \in N \ F : Compatible(log[n1], log[n2]) |
| 195 | + |
| 196 | +Liveness == \A r \in R : r >= GST /\ Leader(r) \notin F => |
| 197 | + \A n \in N \ F : round[n] >= r+2 => |
| 198 | + \E i \in DOMAIN log[n] : log[n][i] = LeaderVertex(r) |
| 199 | + |
| 200 | +=========================================================================== |
0 commit comments