vault backup: 2025-03-25 13:59:04

.obsidian/workspace.json

@@ -242,10 +242,10 @@
   },
   "active": "43416c0d533d9ab4",
   "lastOpenFiles": [
+    "Concurrent Systems/slides/class 7.pdf",
+    "Concurrent Systems/notes/7- MUTEX-free concurrency.md",
     "Concurrent Systems/notes/3a - Hardware primitives & Lamport Bakery algorithm.md",
     "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md",
-    "Concurrent Systems/notes/7- MUTEX-free concurrency.md",
-    "Concurrent Systems/slides/class 7.pdf",
     "Concurrent Systems/slides/class 8.pdf",
     "Pasted image 20250325090735.png",
     "Concurrent Systems/notes/images/Pasted image 20250324091452.png",

Concurrent Systems/notes/7- MUTEX-free concurrency.md

@@ -182,3 +182,6 @@ la conclude serve a garantire che il sequence number sia corretto. Se è stato g
 the implementation of the stack is non-blocking
 
 *Proof:*
+Let us consider an operation invocation performed by p
+- if it terminates, √
+- otherwise, TOP has changed between the first of TOP and the last Compare&set