From Broadcast to Consensus

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
// Code for process i

echo = False
vote = False
reliableDeliver = False

upon broadcast(m)
   send <BROADCAST, m>ᵢ to all processes

upon receiving <BROADCAST, m>ⱼ from j 
   if echo == False
      trigger deliver(j, m)
      send <ECHO, <BROADCAST, m>ⱼ>ᵢ to all processes
      echo = True

upon receiving {<ECHO, <BROADCAST, m>ⱼ>ₖ | k ∈ Q} = M from a quorum Q
   if vote == False
      trigger consistentDeliver(j, m)
      send <VOTE, <BROADCAST, m>ⱼ>ᵢ to all processes
      vote = True

upon receiving {<VOTE, <BROADCAST, m>ⱼ>ₖ} from f+1 processes
   if vote == False
      trigger consistentDeliver(j, m)
      send <VOTE, <BROADCAST, m>ⱼ>ᵢ to all processes
      vote = True

upon receiving {<VOTE, <BROADCAST, m>ⱼ>ₖ | k ∈ Q} = M from a quorum Q
   if reliableDeliver == False
      trigger reliableDeliver(j, m)
      reliableDeliver = True

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
// Code for process i

upon newView(v)
   currView = v
   voted = False
   send <NewLeader, curView, preparedView, preparedVal, cert>ᵢ to leader(v)

upon receiving {<NewLeader, v, viewⱼ, valⱼ, certⱼ>ⱼ | j ∈ Q} = M from a quorum Q
   pre: currView == v ∧ i = leader(v) ∧ (∀ m ∈ M: validNewLeader(m))
   if ∃ j: viewⱼ = max{viewₖ | k ∈ Q} != 0
      Brb_cast(<Propose, v, valⱼ, M>ᵢ)
   else 
      broadcast(<Propose, v, myVal(), M>ᵢ)

upon consistentDeliver(j, <Propose, v, val, M>ⱼ = m)
   pre: currView == v ∧ voted = False ∧ safeProposal(m)
   currVal = val
   voted = True
   send <Propose, v, myVal(), M>ᵢ