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

vault backup: 2025-03-31 12:03:39

Browse source
This commit is contained in:
Marco Realacci 2025-03-31 12:03:39 +02:00
parent a43597cd6e
commit 0338e886ea
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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: 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 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$ 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⟩ 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. 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 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 - the sequence number of `LAST_OP[i]` can increase only after ⟨“op(par)”,sn⟩ has been executed