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

Concurrent Systems/notes/9 - Consensus.md

@@ -75,7 +75,10 @@ P.S. *invoc_i*, *result_i* e *z_i* sono variabili locali.
 
 ### A wait-free construction
 - `LAST_OP[1..n]:` array of SWMR atomic R/W registers containing pairs init at ⟨⊥,0⟩ ∀i
-- `last_sn_i[1..n]:` local array of the last op by $p_i$ executed by $p_i$ init at 0 ∀i,j
+	- è condiviso e ogni processo ci infila le sue proposal
+- `last_sn_i[1..n]:` local array of the last op by $p_j$ executed by $p_i$ init at 0 ∀i,j
+	- ogni processo ha la sua copia locale
+	- `last_sn_i[j]` traccia dell'ultima operazione eseguita da j
 
 Idea: instead of just proposing my proposal, at every moment I propose all the proposals of all the processes.
 
@@ -83,4 +86,24 @@ Idea: instead of just proposing my proposal, at every moment I propose all the p
 or(arg) by p_i on Z
 	result_i <- ⊥
 	LAST_OP[i] <- ⟨op(args), last_sn_i[i]+1⟩
-```
+	wait result_i != ⊥
+	return result_i
+
+local simulation of Z by p_i
+	k <- 0
+	z_i <- Z.init()
+	while true
+		invoc_i <- 𝜀
+		∀ j = 1..n
+			if 𝜋2(LAST_OP[j])>last_sni[j] then
+			invoci.append( ⟨𝜋1(LAST_OP[j]),j⟩ )
+			if invoci ≠ 𝜀 then
+				k++
+				exec_i <- CONS[k].propose(invoci)
+				for r=1 to |execi|
+					⟨zi,res⟩ -> 𝛿(zi,𝜋1(execi[r]))
+					j <- 𝜋2(execi[r])
+					last_sni[j]++
+					if i=j then 
+						result_i <- res
+```