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

This commit is contained in:
Marco Realacci 2025-04-01 09:09:49 +02:00
parent 0fb24852b1
commit aada254e38

View file

@ -51,7 +51,7 @@ p(C) can be R1.read() or R1.write(v) and q(C) can be R2.read() or R2.write
- like point 1... We will again obtain a configuration that is both 0-valent and 1-valent - 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) 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) - *Remark:* only p can distinguish 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: - Let S' be the scheduling from C' where p stops and q decides:
- S' starts with the write of q - S' starts with the write of q
- S' leads q to decide 1, since q(C') is 1-valent - S' leads q to decide 1, since q(C') is 1-valent
@ -59,4 +59,8 @@ p(C) can be R1.read() or R1.write(v) and q(C) can be R2.read() or R2.write
- because of the initial remark, q decides 1 also here - because of the initial remark, q decides 1 also here
- Reactivate p - Reactivate p
- if p decides 0, then we would violate agreement - if p decides 0, then we would violate agreement
- if - if p decides 1, we contradict 0-valence of p(C')
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
- Then, work like in case (3).