vault backup: 2025-03-31 09:35:43

Concurrent Systems/notes/9 - Consensus.md

@@ -137,3 +137,27 @@ If $p_i$ has inserted ⟨“op(par)”,sn⟩ in `LAST_OP[i]`, it cannot invoke a
 - 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⟩
+
+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