vault backup: 2025-03-10 22:28:12

Concurrent Systems/notes/3b - Aravind's algorithm and improvements.md

@@ -91,3 +91,8 @@ lock(i) :=
 	until foreach j != i, STAGE[j] = 0
 ```
 
+-  $p_n$ invokes lock alone, completes its CS and its new DATE is n
+
+**Lemma 1:** DATE's bounds are $[0, n]$
+*Proof:*
+For the upper bound, it's trivial: DATE is either decreased or set to $n$.