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

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

Browse source
This commit is contained in:
Marco Realacci 2025-03-03 10:36:24 +01:00
parent 3a122c3833
commit 78d4c57789
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Concurrent Systems/notes/Lezione1.md
View file

@ -217,4 +217,4 @@ Induction (true for ℓ, to be proved for ℓ+1):
- p at level ℓ can increase its level by writing its FLAG at ℓ+1 and its index in $A_Y[ℓ+1]$ - p at level ℓ can increase its level by writing its FLAG at ℓ+1 and its index in $A_Y[ℓ+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 - 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).