diff --git a/Concurrent Systems/notes/9 - Consensus.md b/Concurrent Systems/notes/9 - Consensus.md index 2f633ca..ee3cf64 100644 --- a/Concurrent Systems/notes/9 - Consensus.md +++ b/Concurrent Systems/notes/9 - Consensus.md @@ -130,11 +130,12 @@ Let pi invoke Z.op(par); to prove the Lemma, we need to show that eventually res It suffices to prove that ∃ k s.t. `CONS[k].propose(-)` returns a list that contains ⟨“op(par)”,i⟩ and pi participates to the consensus: 1. since $p_i$ increases the sequence number of `LAST_OP[i]`, eventually all the lists proposed contain that element forever 2. eventually, $p_i$ will always find `invoc_i != ε` and participates with an increasing sequence number $k_i$ -3. let k be the first consensus where (a) holds +3. let k be the first consensus where (1) holds 4. by the properties of consensus, exec_i contains ⟨“op(par)”,i⟩ As shown before, every invocation is executed; we have to show that this cannot happen more than once. +**Lemma 2:** metti nome lemma If $p_i$ has inserted ⟨“op(par)”,sn⟩ in `LAST_OP[i]`, it cannot invoke another operation until ⟨“op(par)”,sn⟩ appears in a list chosen by the consensus - the sequence number of `LAST_OP[i]` can increase only after ⟨“op(par)”,sn⟩ has been executed