marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

vault backup: 2025-04-04 23:35:23

Browse source
This commit is contained in:
Marco Realacci 2025-04-04 23:35:23 +02:00
parent 96872ffa06
commit 6a9cf80167
13 changed files with 28 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

4
Concurrent Systems/notes/6 - Atomicity.md
View file

@ -21,9 +21,9 @@ A complete history $\hat{H}$ is **linearizable** if there exists a sequential hi
Given an history $\hat{K}$, we can define a binary relation on events $⟶_{K}$ s.t. (op, op’) ∈ ⟶K if and only if res[op] <K inv[op’]. We write op ⟶K op’ for denoting (op, op’) ∈ ⟶K. Hence, condition 3 of the previous Def. requires that ⟶H ⊆ ⟶S.
![[Pasted image 20250318090733.png]]
![[images/Pasted image 20250318090733.png]]
![[Pasted image 20250318090909.png]]But there is another linearization possible! I can also push a before if I pull it before c!
![[images/Pasted image 20250318090909.png]]But there is another linearization possible! I can also push a before if I pull it before c!
Of course I have to respect the semantics of a Queue (if I push "a" first, I have to pop "a" first because it's a fucking FIFO)
#### Compositionality theorem