vault backup: 2025-03-31 10:12:33

This commit is contained in:
Marco Realacci 2025-03-31 10:12:33 +02:00
parent 0656872fa4
commit 74c66937d7

View file

@ -199,4 +199,26 @@ why wait forever? Because we want to prove that it is wait free, but not because
- every $p_i$ that participates to the consensus reads the other proposals after that it has written `PROP[i]` - every $p_i$ that participates to the consensus reads the other proposals after that it has written `PROP[i]`
- all participants starts their for loops after $p_x$ has written its proposal - all participants starts their for loops after $p_x$ has written its proposal
- every $p_i$ that participates to the consensus finds `PROP[x] != ⊥` in their for loop - every $p_i$ that participates to the consensus finds `PROP[x] != ⊥` in their for loop
- `BC[x]` o - `BC[x]` only receives proposals equal to 1
- because of validity of binary consensus, `BC[x]` returns 1
- every $p_i$ that participates to the consensus receives 1 at most in its x-th iteration of the for
- let y (<= x) be the first index such that `BC[y]` returns 1
- `BC[z] = 0` for all $z < y$
- since all participating process invoke the binary consensus in the same order, they all decide the value proposed by $p_y$ and terminate.
##### Multivalued consensus (with bounded values)
Let k be the number of possible proposals and $h = \lceil \log k \rceil$ be the number of bits needed to binary represent them (this value is known to all processes).
IDEA: decide bit by bit the final outcome
```
PROP[1..n][1..h] array of n h-bits proposals, all init at ⊥ BC[1..h] array of h binary consensus objects
bmv_propose(i,v) :=
PROP[i] <- binary_repr_h(v)
for k=1 to h do
P <- {PROP[j][k] | PROP[j] PROP[j][1..k-1]=res[1..k-1]}
let b be an element of P
res[k] <- BC[k].propose(b)
return value(res)
```