marcorealacci/master-degree-notes
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

vault backup: 2025-03-04 12:40:54

Browse source
This commit is contained in:
Marco Realacci 2025-03-04 12:40:54 +01:00
parent e4f6fdad25
commit 47a34c7a78
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
Concurrent Systems/notes/Lezione2.md
View file

@ -36,11 +36,15 @@ lock(i) :=
wait Y = ⊥ wait Y = ⊥
goto * goto *
else Y <- i else Y <- i
if X = i then return if X = i then return
else FLAG[i] <- down else FLAG[i] <- down
∀j.wait FLAG[j] = down ∀j.wait FLAG[j] = down
if Y = i then return if Y = i then return
else wait Y = ⊥ else wait Y = ⊥
goto * goto *
unlock(i) := unlock(i) :=
@ -49,15 +53,13 @@ unlock(i) :=
return return
``` ```
MUTEX proof ##### MUTEX proof
How can pi enter its CS? How can pi enter its CS?
![[Pasted image 20250304084537.png]] ![[Pasted image 20250304084537.png]]
![[Pasted image 20250304084901.png]] ![[Pasted image 20250304084901.png]]
Deadlock freedom ##### Deadlock freedom
Let $p_i$ invoke lock Let $p_i$ invoke lock
- If it eventually wins -> √ - If it eventually wins -> √
- If it is blocked forever, where can it be blocked? - If it is blocked forever, where can it be blocked?
@ -73,7 +75,8 @@ Let $p_i$ invoke lock
- 3. In the first wait Y = ⊥ - 3. In the first wait Y = ⊥
- since pj read a value different from ⊥, there is at least one pk that wrote Y before (but has not yet unlocked) - since pj read a value different from ⊥, there is at least one pk that wrote Y before (but has not yet unlocked)
- if $p_k$ eventually enters its CS -> ok, otherwise it must be blocked forever as well. Where? - if $p_k$ eventually enters its CS -> ok, otherwise it must be blocked forever as well. Where?
- ![[Pasted image 20250304090207.png]] - In the second wait Y = ⊥: but then there exists a $p_h$ that eventually enters its CS -> good
- In the ∀j.wait FLAG[j]=down: this wait cannot block a process forever
![[Pasted image 20250304090219.png]] ![[Pasted image 20250304090219.png]]