From e1886f36e344549d9622a1cf6b9ec593e98dbf11 Mon Sep 17 00:00:00 2001 From: Marco Realacci Date: Mon, 31 Mar 2025 09:35:43 +0200 Subject: [PATCH] vault backup: 2025-03-31 09:35:43 --- Concurrent Systems/notes/9 - Consensus.md | 26 ++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/Concurrent Systems/notes/9 - Consensus.md b/Concurrent Systems/notes/9 - Consensus.md index 999efc9..b166f49 100644 --- a/Concurrent Systems/notes/9 - Consensus.md +++ b/Concurrent Systems/notes/9 - Consensus.md @@ -136,4 +136,28 @@ As shown before, every invocation is executed; we have to show that this cannot 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 -Let k be the minimum such that `CONS[k]` contains ⟨“op(par)”,i⟩ \ No newline at end of file +Let k be the minimum such that `CONS[k]` contains ⟨“op(par)”,i⟩ + +Every $p_{j}$ that participates in the k-th consensus increases `last_sn_j[i]` before calculating a new proposal `invoc_j` +- if `π2(LAST_OP[i])` is not changed, then the guard of the IF is false and ⟨“op(par)”,i⟩ is not appended in `invoc_j` +- otherwise, we have a new invocation from $p_{i}$ (but this can only happen after that ⟨“op(par)”,sn⟩ has been executed) + +**Lemma 3:** the local copies $s_{i}$ if all correct processes behave the same and comply with the sequential specification of Z + +*Proof:* +- the processes use CONS in the same order `(CONS[1], CONS[2], …)` +- every consensus object returns the same list to all processes +- all processes scan the returned list from head to tail + - then apply the same sequence of operations to their local copies (that started from the same initial value) + - everything works because of determinism! + +REMARK: bounded wait freedom does not hold: +... + +### Solution for non-deterministic specifications +If the specifications of Z’s operations are non-deterministic, then 𝛿 does not return one single possible pair after one invocation, but a set of possible choices. + +How to force every process to run the very same sequence of operations on their local simulations? +Three possible ways! + +1. Brute forc \ No newline at end of file