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

vault backup: 2025-03-03 10:46:24

Browse source
This commit is contained in:
Marco Realacci 2025-03-03 10:46:24 +01:00
parent 37e6fb6da9
commit 65118f7cfd
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Concurrent Systems/notes/Lezione1.md
View file

@ -218,3 +218,5 @@ Induction (true for ℓ, to be proved for ℓ+1):
- let $p_x$ be the last one that writes `A_Y[ℓ+1]`, so `A_Y[ℓ+1]=x` - let $p_x$ be the last one that writes `A_Y[ℓ+1]`, so `A_Y[ℓ+1]=x`
- for $p_x$ to pass at level ℓ+1, it must be that $∀k≠x. F[k] < ℓ+1$, then $p_x$ is the only proc at level ℓ+1 and the thesis holds, since 1<=n-ℓ-1 - for $p_x$ to pass at level ℓ+1, it must be that $∀k≠x. F[k] < ℓ+1$, then $p_x$ is the only proc at level ℓ+1 and the thesis holds, since 1<=n-ℓ-1
- otherwise, $p_x$ is blocked in the wait and so we have at most n-ℓ-1 processes at level ℓ+1 (i.e., those at level ℓ, that by induction are at most n-ℓ, except for px that is blocked in its (ℓ+1)-th wait). - otherwise, $p_x$ is blocked in the wait and so we have at most n-ℓ-1 processes at level ℓ+1 (i.e., those at level ℓ, that by induction are at most n-ℓ, except for px that is blocked in its (ℓ+1)-th wait).
##### Starvation freedom proof