vault backup: 2025-03-31 08:50:43

Concurrent Systems/notes/9 - Consensus.md

@@ -41,7 +41,7 @@ Universality of consensus holds as folows:
 ### First attempt (non wait-free)
 Let us first concentrate on obj's with deterministic specifications (we will see how to handle non-determinism later on)
 
-Process $p_i$ wants to invoke operation op of object Z with arguments args, locally runs:
+A process $p_i$ that wants to invoke operation op of object Z with arguments args locally runs:
 ```
 result_i <- ⊥
 invoc_i <- ⟨op(args) , i⟩
@@ -49,3 +49,24 @@ wait result_i != ⊥
 return result_i
 ```
 
+Every process locally runs also a simulation of Z (stored in the local variable $Z_i$) such that:
+- $Z_{i}$ is initialized at the initial value of Z
+- every process performs on $Z_i$ all the operations performed in Z by all processes, in the same order
+	- need of consensus
+
+Let CONS be an unbounded array of consensus objects and 𝜋1 and 𝜋2 respectively denote the first and the second element of a given pair (aka the first and second *projection*)
+
+The local simulation of Z by $p_i$ is
+
+```
+k <- 0
+z_i <- Z.init()
+while true
+	if invoc_i ≠ ⊥ then # pros
+		k++
+		exec_i <- CONS[k].propose(invoc_i)
+		⟨zi , res⟩ <- 𝛿(zi , 𝜋1(exec_i))
+		if 𝜋2(exec_i) = i then
+			invoc_i <- ⊥
+			result_i <- res
+```