diff --git a/Concurrent Systems/notes/9 - Consensus.md b/Concurrent Systems/notes/9 - Consensus.md index 3653b4a..db9d6ce 100644 --- a/Concurrent Systems/notes/9 - Consensus.md +++ b/Concurrent Systems/notes/9 - Consensus.md @@ -225,13 +225,13 @@ bmv_propose(i,v) := res[k] <- BC[k].propose(b) 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:* - Wait freedom: trivial - Integrity: trivial - 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: - 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`