From 22eb1d6fb59a13fc67d282058222f3db84a5f130 Mon Sep 17 00:00:00 2001
From: Marco Realacci <marco@marcorealacci.me>
Date: Mon, 24 Mar 2025 10:23:11 +0100
Subject: [PATCH] vault backup: 2025-03-24 10:23:11

---
 .obsidian/workspace.json                              | 4 ++--
 Concurrent Systems/notes/7- MUTEX-free concurrency.md | 5 +++++
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index 7aa2533..e09ce9f 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -51,9 +51,9 @@
               "type": "pdf",
               "state": {
                 "file": "Concurrent Systems/slides/class 7.pdf",
-                "page": 10,
+                "page": 11,
                 "left": -23,
-                "top": 90,
+                "top": 208,
                 "zoom": 0.680522565320665
               },
               "icon": "lucide-file-text",
diff --git a/Concurrent Systems/notes/7- MUTEX-free concurrency.md b/Concurrent Systems/notes/7- MUTEX-free concurrency.md
index 21ac560..4f7bcea 100644
--- a/Concurrent Systems/notes/7- MUTEX-free concurrency.md	
+++ b/Concurrent Systems/notes/7- MUTEX-free concurrency.md	
@@ -176,3 +176,8 @@ pop() :=
 		return v
 ```
 
+#### Liveness theorem
+the implementation of the stack is non-blocking
+
+*Proof:*
+mi fido
\ No newline at end of file