marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

vault backup: 2025-03-31 17:54:17

Browse source
This commit is contained in:
Marco Realacci 2025-03-31 17:54:17 +02:00
parent 47d014e2fb
commit 8c6ffdef76
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
Concurrent Systems/notes/9 - Consensus.md
View file

@ -225,13 +225,13 @@ bmv_propose(i,v) :=
res[k] <- BC[k].propose(b) res[k] <- BC[k].propose(b)
return value(res) return value(res)
``` ```
(exercise: remove `∧ PROP[j][1..k-1]=res[1..k-1]` and execution in which a consensus property can be broken) (exercise: remove `∧ PROP[j][1..k-1]=res[1..k-1]` and show an execution in which a consensus property can be broken)
*Proof:* *Proof:*
- Wait freedom: trivial - Wait freedom: trivial
- Integrity: trivial - Integrity: trivial
- Agreement: by agreement of the h binary consensus objects - Agreement: by agreement of the h binary consensus objects
- Validity: for all k, we prove that, if dec is the decided value, then there exists a j such that $p_j$ is participating (`PROP[j] ≠ ⊥`) and `dec[1...k] = PROP[j][1...k]` - Validity: for all k, we prove that, if `dec` is the decided value, then there exists a j such that $p_j$ is participating (`PROP[j] ≠ ⊥`) and `dec[1...k] = PROP[j][1...k]`
- by construction, P contains the k-th bits of the proposals whose first (k-1) bits coincide with the first k-1 bits decides so far: - by construction, P contains the k-th bits of the proposals whose first (k-1) bits coincide with the first k-1 bits decides so far:
- for every b ∈ P, there exists a j such that `PROP[j] ≠ ⊥`, - for every b ∈ P, there exists a j such that `PROP[j] ≠ ⊥`,
- `PROP[j][1..k-1] = dec[1..k-1]` and `PROP[j][k] = b` - `PROP[j][1..k-1] = dec[1..k-1]` and `PROP[j][k] = b`