diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json index e922543..d078025 100644 --- a/.obsidian/workspace.json +++ b/.obsidian/workspace.json @@ -34,9 +34,9 @@ "type": "pdf", "state": { "file": "Concurrent Systems/slides/class 3.pdf", - "page": 13, + "page": 14, "left": -26, - "top": 182, + "top": 41, "zoom": 0.57541567695962 }, "icon": "lucide-file-text", diff --git a/Concurrent Systems/notes/3.md b/Concurrent Systems/notes/3.md index 1af61e1..ca9ecab 100644 --- a/Concurrent Systems/notes/3.md +++ b/Concurrent Systems/notes/3.md @@ -226,6 +226,24 @@ unlock(i) := #### MUTEX proof **Theorem:** if $p_i$ is in the CS, then $p_j$ cannot simultaneously be in the CS. -*Proof:* by contradiction. a +*Proof:* by contradiction. -#### proof \ No newline at end of file +... + +#### Bounded bypass proof +**Lemma 1:** exactly after n CSs there is a reset of DATE. +*Proof:* +- the first CS leads $max_j{DATE[j]}$ to n+1 +- the seconds CS leads ... to n+2 +- ... +- the n-th read leads ... to n+n = 2n -> RESET + +**Lemma 2:** there can be at most one reset of DATE during an invocation of a lock +*Proof:* +- let $p_i$ invoke lock, if no reset occurs, ok +- otherwise, let us consider the moment in which a reset occurs + - if pi is the next process that enters the CS, ok + - Otherwise let $p_j$ be the process that enters, its next date is $n+1 > DATE[i]$ + - $p_{j}$ cannot surpass $p_i$ again (before a RESET) + - The worst case is then all processes perform lock together and $i = n$ (i am process n) + - all $p_{1}\dots p_{n}$ surpass $ \ No newline at end of file