vault backup: 2025-04-01 11:48:48

.obsidian/workspace.json

@@ -212,9 +212,9 @@
   },
   "active": "483215723737b6f7",
   "lastOpenFiles": [
-    "Concurrent Systems/notes/9 - Consensus.md",
-    "Concurrent Systems/notes/10 - Implementing Consensus.md",
     "Concurrent Systems/slides/class 10.pdf",
+    "Concurrent Systems/notes/10 - Implementing Consensus.md",
+    "Concurrent Systems/notes/9 - Consensus.md",
     "Pasted image 20250401092557.png",
     "Pasted image 20250401083747.png",
     "Concurrent Systems/notes/3a - Hardware primitives & Lamport Bakery algorithm.md",

Concurrent Systems/notes/10 - Implementing Consensus.md

@@ -65,7 +65,7 @@ p(C’) can be R1.read() or R1.write(v) and q(C’) can be R2.read() or R2.write
 	- *Remark:* q(p(C)) = q(C) cannot be distinguished by q since the value written by p is lost after the write of q
 	- Then, work like in case (3).
 
-### CN(Test&set) = 2
+### CN(test&set) = 2
 ```
 TS a test&set object init at 0
 PROP array of proposals, init at whatever
@@ -106,12 +106,32 @@ Let S’ be a schedule of operations only from r that leads p(q(C’)) to a deci
 - 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
 
-### CN(Swap) = CN(Fetch&add) = 2
+### CN(swap) = CN(fetch&add) = 2
 ```
-...
+S a swap object init at ⊥
+PROP array of proposals, init at whatever
+
+propose(i, v) :=
+	PROP[i] <- v
+	if S.swap(i) = ⊥ then
+		return PROP[i]
+	else
+		return PROP[1-i]
 ```
 
-### CN(Compare&swap) = ∞
+```
+FA a fetch&add object init at 0
+PROP array of proposals, init at whatever
+
+propose(i, v) :=
+	PROP[i] <- v
+	if FA.fetch&add(1) = 0 then
+		return PROP[i]
+	else
+		return PROP[1-i]
+```
+
+### CN(compare&swap) = ∞
 
 Let us consider a verison of the compare&swap where, instead of returning a boolean, it always returns the previous value of the object, i.e.: