From 597b861a6ea2fea8f1ab28412632f0e91a4c4b94 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 31 Mar 2025 12:33:39 +0200 Subject: [PATCH] vault backup: 2025-03-31 12:33:39 --- .obsidian/workspace.json | 7 +++---- Concurrent Systems/notes/9 - Consensus.md | 2 +- 2 files changed, 4 insertions(+), 5 deletions(-) diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index 72c8d75..9234e2a 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -33,8 +33,7 @@ "title": "class 9" } } - ], - "currentTab": 1 + ] } ], "direction": "vertical" @@ -203,10 +202,10 @@ "companion:Toggle completion": false } }, - "active": "f158d16483dc1627", + "active": "aa7ed62f1bcd712a", "lastOpenFiles": [ - "Concurrent Systems/notes/9 - Consensus.md", "Concurrent Systems/slides/class 9.pdf", + "Concurrent Systems/notes/9 - Consensus.md", "Concurrent Systems/notes/2 - Fast mutex by Lamport.md", "Concurrent Systems/notes/3a - Hardware primitives & Lamport Bakery algorithm.md", "Concurrent Systems/notes/7- MUTEX-free concurrency.md", diff --git a/Concurrent Systems/notes/9 - Consensus.md b/Concurrent Systems/notes/9 - Consensus.md index d9e8ce1..93db730 100644 --- a/Concurrent Systems/notes/9 - Consensus.md +++ b/Concurrent Systems/notes/9 - Consensus.md @@ -135,7 +135,7 @@ It suffices to prove that ∃ k s.t. `CONS[k].propose(-)` returns a list that co As shown before, every invocation is executed; we have to show that this cannot happen more than once. -**Lemma 2:** metti nome lemma +**Lemma 2:** all operations invoked by processes are executed exactly once 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