vault backup: 2025-04-01 09:04:49

Concurrent Systems/notes/10 - Consensus Implementation.md

@@ -46,3 +46,17 @@ p(C’) can be R1.read() or R1.write(v) and q(C’) can be R2.read() or R2.write
 
 1. if R1 != R2
 	- Whatever operations p and q issue, we have that q(p(C’)) = p(q(C’)) But q(p(C’)) is 0-val (because p(C’) is) whereas p(q(C’)) is 1-val
+		- impossible case
+2. R1 = R2 and both operations are a read
+	- like point 1... We will again obtain a configuration that is both 0-valent and 1-valent
+
+3. R1 = R2, with p that reads and q that writes (or viceversa)
+	- *Remark:* only p can distinguisc C' from p(C') (reads put the value read in a local variable, visible only by the process that performed the read)
+	- Let S' be the scheduling from C' where p stops and q decides:
+		- S' starts with the write of q
+		- S' leads q to decide 1, since q(C') is 1-valent
+	- Consider p(C') and apply S'
+		- because of the initial remark, q decides 1 also here
+	- Reactivate p
+		- if p decides 0, then we would violate agreement
+		- if