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

Concurrent Systems/notes/10 - Consensus Implementation.md

@@ -92,4 +92,17 @@ Let’s assume that:
 - at C’ r stops for a long time
 - $op_{p}$ and $op_{q}$ are the next operations that p and q issue from C’ by following A
 
-1. $op_p$ and $op_q$ are both R/W 
+1. $op_p$ and $op_q$ are both R/W operations on atomic registers
+	- like in the previous proof
+2. one is an operation on an atomic register and the other is a test&set but on different objects
+	- like the first case of the previous proof, since p(q(C')) = q(p(C'))
+3. they are both test&set on the same object
+	- p(q(C’)) is 1-val whereas q(p(C’)) is 0-va
+
+Let us now stop both p and q and resume r
+- r cannot see any difference between p(q(C’)) and q(p(C’)) (the only diff.’s are the values locally stored by p and q as result of T&S)
+
+Let S’ be a schedule of operations only from r that leads p(q(C’)) to a decision (that must be 1)
+- Since r cannot see any difference between p(q(C’)) and q(p(C’)), if we run S’ from q(p(C’)) we must decide 1 as well
+	- in contradiction with q(p(C')) be 0-val
+