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

This commit is contained in:
Marco Realacci 2025-04-01 09:14:49 +02:00
parent aada254e38
commit 253b3221b4

View file

@ -64,3 +64,20 @@ p(C) can be R1.read() or R1.write(v) and q(C) can be R2.read() or R2.write
4. R1 = R2 and both operations are a write 4. R1 = R2 and both operations are a 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 - *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). - Then, work like in case (3).
### CN(Test&set) = 2
```
TS a test&set object init at 0
PROP array of proposals, init at whatever
propose(i, v) :=
PROP[i] <- v
if TS.test&set() = 0 then
return PROP[i]
else
return PROP[1-i]
```
Wait-freedom, Validity and Integrity hold by construction.
Agreement: the first that performs test&set receives 0 and decides his proposal; the other one receives 1 and decides the other proposal.