diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index e8dc440..fe3685f 100644 --- a/.obsidian/workspace.json +++ b/.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", diff --git a/Concurrent Systems/notes/10 - Implementing Consensus.md b/Concurrent Systems/notes/10 - Implementing Consensus.md index fd15b8e..654561e 100644 --- a/Concurrent Systems/notes/10 - Implementing Consensus.md +++ b/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.: