From 0716cad7ac1a7672c978774e9a6c7f0295d8c515 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 31 Mar 2025 10:17:33 +0200 Subject: [PATCH] vault backup: 2025-03-31 10:17:33 --- Concurrent Systems/notes/9 - Consensus.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/Concurrent Systems/notes/9 - Consensus.md b/Concurrent Systems/notes/9 - Consensus.md index fb44f05..cfe3097 100644 --- a/Concurrent Systems/notes/9 - Consensus.md +++ b/Concurrent Systems/notes/9 - Consensus.md @@ -215,10 +215,17 @@ 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) + PROP[i] <- binary_repr_h(v) # scrivo la rappresentazione binaria 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) -``` \ No newline at end of file +``` +(exercise: remove `∧ PROP[j][1..k-1]=res[1..k-1]` and 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 \ No newline at end of file