vault backup: 2025-03-18 09:24:12

Concurrent Systems/notes/6 - Atomicity.md

@@ -25,3 +25,9 @@ Given an history $\hat{K}$, we can define a binary relation on events $⟶_{K}$
 
 ![[Pasted image 20250318090909.png]]But there is another linearization possible! I can also push a before if I pull it before c!
 
+#### Compositionality theorem
+$\hat{H}$ is linearizable if $\hat{H}|_{X}$ is linearizable, for all X in H
+(it is good to linearize complex traces)
+
+For all X, let $\hat{S}_{X}$ be a linearization of $\hat{H}_{X}$
+	- $\hat{S}_{X} def$