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

vault backup: 2025-04-05 00:07:51

Browse source
This commit is contained in:
Marco Realacci 2025-04-05 00:07:51 +02:00
parent 47b74f3eec
commit 1c82ee3d9d
11 changed files with 30 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

22
.obsidian/workspace.json vendored
View file

@ -4,21 +4,20 @@
"type": "split", "type": "split",
"children": [ "children": [
{ {
"id": "32947c2821d23646", "id": "65ffc94caaa1d4a8",
"type": "tabs", "type": "tabs",
"children": [ "children": [
{ {
"id": "7c5b0ca6f7687800", "id": "eb9b42e21c969fd9",
"type": "leaf", "type": "leaf",
"state": { "state": {
"type": "markdown", "type": "diff-view",
"state": { "state": {
"file": "Concurrent Systems/notes/2b - Round Robin algorithm.md", "file": "Concurrent Systems/notes/6 - Atomicity.md",
"mode": "source", "staged": false
"source": false
}, },
"icon": "lucide-file", "icon": "git-pull-request",
"title": "2b - Round Robin algorithm" "title": "Diff View (6 - Atomicity)"
} }
} }
] ]
@ -189,14 +188,16 @@
"companion:Toggle completion": false "companion:Toggle completion": false
} }
}, },
"active": "7c5b0ca6f7687800", "active": "eb9b42e21c969fd9",
"lastOpenFiles": [ "lastOpenFiles": [
"Concurrent Systems/notes/1b - Peterson algorithm.md", "Concurrent Systems/notes/1b - Peterson algorithm.md",
"Concurrent Systems/notes/2b - Round Robin algorithm.md",
"Concurrent Systems/notes/10 - Implementing Consensus.md",
"\u0001.md",
"Concurrent Systems/notes/images/Pasted image 20250405000438.png", "Concurrent Systems/notes/images/Pasted image 20250405000438.png",
"Pasted image 20250405000428.png", "Pasted image 20250405000428.png",
"Concurrent Systems/notes/3b - Aravind's algorithm and improvements.md", "Concurrent Systems/notes/3b - Aravind's algorithm and improvements.md",
"Concurrent Systems/notes/4 - Semaphores.md", "Concurrent Systems/notes/4 - Semaphores.md",
"Concurrent Systems/notes/2b - Round Robin algorithm.md",
"Concurrent Systems/notes/4b - Monitors.md", "Concurrent Systems/notes/4b - Monitors.md",
"Concurrent Systems/notes/4c - Dining Philosophers.md", "Concurrent Systems/notes/4c - Dining Philosophers.md",
"Concurrent Systems/a.md", "Concurrent Systems/a.md",
@ -204,7 +205,6 @@
"Concurrent Systems/notes/images/Pasted image 20250304093223.png", "Concurrent Systems/notes/images/Pasted image 20250304093223.png",
"Concurrent Systems/notes/Untitled.md", "Concurrent Systems/notes/Untitled.md",
"Concurrent Systems/notes/9 - Consensus.md", "Concurrent Systems/notes/9 - Consensus.md",
"Concurrent Systems/notes/10 - Implementing Consensus.md",
"Concurrent Systems/notes/8 - Enhancing Liveness Properties.md", "Concurrent Systems/notes/8 - Enhancing Liveness Properties.md",
"Concurrent Systems/notes/7- MUTEX-free concurrency.md", "Concurrent Systems/notes/7- MUTEX-free concurrency.md",
"Concurrent Systems/notes/6 - Atomicity.md", "Concurrent Systems/notes/6 - Atomicity.md",

4
Concurrent Systems/notes/1 - CS Basics.md
View file

@ -62,7 +62,7 @@ function withdraw() {
While `read()` and `write()` may be considered as atomic, their sequential composition **is not**. While `read()` and `write()` may be considered as atomic, their sequential composition **is not**.
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250303090135.png) ![](images/Pasted%20image%2020250303090135.png)
#### Mutual Exclusion (MUTEX) #### Mutual Exclusion (MUTEX)
Ensure that some parts of the code are executed as *atomic*. Ensure that some parts of the code are executed as *atomic*.
@ -100,7 +100,7 @@ Every solution to a problem should satisfy at least:
**Both inclusions are strict:** **Both inclusions are strict:**
$$\text{Deadlock freedom} \not \implies \text{Starvation freedom}$$ $$\text{Deadlock freedom} \not \implies \text{Starvation freedom}$$
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250303093116.png) ![](images/Pasted%20image%2020250303093116.png)
*p1 is starving!* *p1 is starving!*
$$\text{Starvation freedom} \not \implies \text{Bounded bypass}$$ $$\text{Starvation freedom} \not \implies \text{Bounded bypass}$$
Assume a $f$ and consider the scheduling above, where p2 wins $f(3)$ times and so does p3, then p1 looses (at least) $2f(3)$ times before winning. Assume a $f$ and consider the scheduling above, where p2 wins $f(3)$ times and so does p3, then p1 looses (at least) $2f(3)$ times before winning.

4
Concurrent Systems/notes/10 - Implementing Consensus.md
View file

@ -30,7 +30,7 @@ A configuration C obtained during the execution of all A is called:
If A wait-free implements binary consensus for n processes, then there exists a bivalent initial configuration. If A wait-free implements binary consensus for n processes, then there exists a bivalent initial configuration.
*Proof:* *Proof:*
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250401083747.png) ![](images/Pasted%20image%2020250401083747.png)
### CN(Atomic R/W registers) = 1 ### CN(Atomic R/W registers) = 1
**Thm:** There exists no wait-free implementation of binary consensus for 2 processes that uses atomic R/W registers. **Thm:** There exists no wait-free implementation of binary consensus for 2 processes that uses atomic R/W registers.
@ -135,7 +135,7 @@ propose(i, v) :=
Let us consider a verison of the compare&swap where, instead of returning a boolean, it always returns the previous value of the object, i.e.: Let us consider a verison of the compare&swap where, instead of returning a boolean, it always returns the previous value of the object, i.e.:
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250401092557.png) ![](images/Pasted%20image%2020250401092557.png)
``` ```
CS a compare&swap object init at ⊥ CS a compare&swap object init at ⊥

2
Concurrent Systems/notes/1b - Peterson algorithm.md
View file

@ -56,7 +56,7 @@ a) `FLAG[1] = down`, this is possible only with the following interleaving:
![](images/Pasted%20image%2020250303100721.png) ![](images/Pasted%20image%2020250303100721.png)
b) `AFTER_YOU = 1`, this is possible only with the following interleaving: b) `AFTER_YOU = 1`, this is possible only with the following interleaving:
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250303100953.png) ![](images/Pasted%20image%2020250303100953.png)
##### Bounded Bypass proof (with bound = 1) ##### Bounded Bypass proof (with bound = 1)
- If the wait condition is true, then it wins (and waits 0). - If the wait condition is true, then it wins (and waits 0).

6
Concurrent Systems/notes/2 - Fast mutex by Lamport.md
View file

@ -49,9 +49,9 @@ unlock(i) :=
##### MUTEX proof ##### MUTEX proof
How can pi enter its CS? How can pi enter its CS?
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250304084537.png) ![](images/Pasted%20image%2020250304084537.png)
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250304084901.png) ![](images/Pasted%20image%2020250304084901.png)
(*must finished before nel senso che $p_i$ deve aspettare $p_j$*) (*must finished before nel senso che $p_i$ deve aspettare $p_j$*)
##### Deadlock freedom ##### Deadlock freedom
Let $p_i$ invoke lock Let $p_i$ invoke lock
@ -72,6 +72,6 @@ Let $p_i$ invoke lock
- In the second wait Y = ⊥: but then there exists a $p_h$ that eventually enters its CS -> good - 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 - In the ∀j.wait FLAG[j]=down: this wait cannot block a process forever
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250304090219.png) ![](images/Pasted%20image%2020250304090219.png)
esercizio: prova che NON soddisfa starvation freedom esercizio: prova che NON soddisfa starvation freedom

2
Concurrent Systems/notes/2b - Round Robin algorithm.md
View file

@ -50,5 +50,5 @@ By Deadlock freedom of RR, at least one process eventually unlocks
The worst case is when TURN = *i+1* mod n when FLAG[i] is set. The worst case is when TURN = *i+1* mod n when FLAG[i] is set.
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250304093223.png) ![](images/Pasted%20image%2020250304093223.png)

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

@ -31,7 +31,7 @@ unlock(i) :=
*Proof:* by contradiction. *Proof:* by contradiction.
Let's consider the execution of $p_i$ leading to its CS: Let's consider the execution of $p_i$ leading to its CS:
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250310172134.png) ![](images/Pasted%20image%2020250310172134.png)
**Corollary** (of the MUTEX proof)**:** DATE is never written concurrently. **Corollary** (of the MUTEX proof)**:** DATE is never written concurrently.
@ -57,7 +57,7 @@ Let's consider the execution of $p_i$ leading to its CS:
**Theorem:** the algorithm satisfies bounded bypass with bound $2n-2$. **Theorem:** the algorithm satisfies bounded bypass with bound $2n-2$.
*Proof:* *Proof:*
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250310103703.png) ![](images/Pasted%20image%2020250310103703.png)
so by this, the very worst possible case is that my lock experiences that. so by this, the very worst possible case is that my lock experiences that.
It looks like I can experience at most $2n-1$ other critical sections, but it is even better, let's see: It looks like I can experience at most $2n-1$ other critical sections, but it is even better, let's see:

2
Concurrent Systems/notes/5 - Software Transactional Memory.md
View file

@ -105,7 +105,7 @@ The **casual past** of a transaction T is the set of all T' and T'' such that
VWC allows more transactions to commit -> it is a more liberal property than opacity. VWC allows more transactions to commit -> it is a more liberal property than opacity.
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250317105355.png) ![](images/Pasted%20image%2020250317105355.png)
#### A Vector clock based STM system #### A Vector clock based STM system
We have m shared MRMW registers; register X is represented by a pair XX, with: We have m shared MRMW registers; register X is represented by a pair XX, with:

4
Concurrent Systems/notes/6 - Atomicity.md
View file

@ -21,9 +21,9 @@ A complete history $\hat{H}$ is **linearizable** if there exists a sequential hi
Given an history $\hat{K}$, we can define a binary relation on events $⟶_{K}$ s.t. (op, op’) ∈ ⟶K if and only if res[op] <K inv[op’]. We write op ⟶K op’ for denoting (op, op’) ∈ ⟶K. Hence, condition 3 of the previous Def. requires that ⟶H ⊆ ⟶S. Given an history $\hat{K}$, we can define a binary relation on events $⟶_{K}$ s.t. (op, op’) ∈ ⟶K if and only if res[op] <K inv[op’]. We write op ⟶K op’ for denoting (op, op’) ∈ ⟶K. Hence, condition 3 of the previous Def. requires that ⟶H ⊆ ⟶S.
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250318090733.png) ![](images/Pasted%20image%2020250318090733.png)
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250318090909.png)But there is another linearization possible! I can also push a before if I pull it before c! ![](images/Pasted%20image%2020250318090909.png)But there is another linearization possible! I can also push a before if I pull it before c!
Of course I have to respect the semantics of a Queue (if I push "a" first, I have to pop "a" first because it's a fucking FIFO) Of course I have to respect the semantics of a Queue (if I push "a" first, I have to pop "a" first because it's a fucking FIFO)
#### Compositionality theorem #### Compositionality theorem

4
Concurrent Systems/notes/6a - Alternatives to Atomicity.md
View file

@ -2,9 +2,9 @@ Let us define $op ->_{proc} op'$ to hold whenever there exists a process p that
### Sequential consistency ### Sequential consistency
**Def:** a complete history is sequentially consistent if there exists a sequential history $𝑆$ s.t. **Def:** a complete history is sequentially consistent if there exists a sequential history $𝑆$ s.t.
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250324082534.png) ![](images/Pasted%20image%2020250324082534.png)
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250324082545.png) ![](images/Pasted%20image%2020250324082545.png)
>[!warning] >[!warning]
>The problem with sequential consistency is that it is NOT compositional. >The problem with sequential consistency is that it is NOT compositional.

6
Concurrent Systems/notes/7- MUTEX-free concurrency.md
View file

@ -64,7 +64,7 @@ this implementation satisfies the three requirements for the splitter
- let us consider the last process that writes into LAST (this is an atomic register, so this is meaningful) - let us consider the last process that writes into LAST (this is an atomic register, so this is meaningful)
- if the door is closed, it receives R and √ - if the door is closed, it receives R and √
3. let $p_i$ be the first process that receives $S \to LAST=i$ in its second if 3. let $p_i$ be the first process that receives $S \to LAST=i$ in its second if
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250324091452.png) ![](images/Pasted%20image%2020250324091452.png)
### An Obstruction-free Timestamp Generator ### An Obstruction-free Timestamp Generator
A **timestamp generator** is a concurrent object that provides a single operation get_ts such that: A **timestamp generator** is a concurrent object that provides a single operation get_ts such that:
@ -98,7 +98,7 @@ this implementation satisfies the three properties of the timestamp generator
- every process that starts after its termination will find NEXT to a greater value (NEXT never decreases!) - every process that starts after its termination will find NEXT to a greater value (NEXT never decreases!)
3. Obstruction freedom is trivial 3. Obstruction freedom is trivial
**REMARK:** this implementation doesn’t satisfy the non-blocking property:![](Concurrent%20Systems/notes/images/Pasted%20image%2020250324092633.png) **REMARK:** this implementation doesn’t satisfy the non-blocking property:![](images/Pasted%20image%2020250324092633.png)
### A Wait-free Stack ### A Wait-free Stack
REG is an unbounded array of atomic registers (the stack) REG is an unbounded array of atomic registers (the stack)
@ -149,7 +149,7 @@ This is needed for the so called ABA problem with compare&set:
- with the compare&set you mainly test that the sequence_number has not changed - with the compare&set you mainly test that the sequence_number has not changed
TOP : a register that can be read or compare&setted TOP : a register that can be read or compare&setted
![](Concurrent%20Systems/notes/images/Pasted%20image%2020250324100652.png) ![](images/Pasted%20image%2020250324100652.png)
``` ```
push(w) := push(w) :=