# Ćwiczenia 4, grupa cz. 16-18, 9 listopada 2023

###### tags: `PRW23` `ćwiczenia` `pwit`

## Deklaracje

Gotowość rozwiązania zadania należy wyrazić poprzez postawienie X w odpowiedniej kolumnie! Jeśli pożądasz zreferować dane zadanie (co najwyżej jedno!) w trakcie dyskusji oznacz je znakiem ==X== na żółtym tle.

**UWAGA: Tabelkę wolno edytować tylko wtedy, gdy jest na zielonym tle!**

:::danger
| | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 |
| ----------------------:| ----- | --- | --- | --- | --- | --- | --- | --- |
Dominik Baziuk | X | X | X | | X | X | | X |
Paweł Borek | | | | | | | | |
Arti Brzozowski | X | X | X | | X |==X==| | |
Mateusz Golisz | X | | | | X | X | | X |
Kacper Jóźwiak | | | | | | | | |
Julia Konefał | | | | | | | | |
Adam Korta | ==X== | X | X | | X | X | | X |
Jakub Mikołajczyk | X | X | X | | X | X | | X |
Bartosz Morasz | X | X | X | | X | | | |
Andrzej Morawski | x | x |==x==| x | x | x | | x |
Aleksandra Nicpoń | x | x | x | | x | x | | |
Mateusz Reis | X | X | X | | X | | | |
Tomasz Stachurski | | | | | | | | |
Marcel Szelwiga | X | X | X | X | X | | | X |
Volha Tsekalo | x | x | | | x | x | | x |
Martyna Wybraniec | x | x | x | | x | x | | x |
Denys Zinoviev | | | | | | | | |
Dominik Olejarz | | | | | | | | |
:::

Tutaj można zadeklarować zadanie 8 z listy 3:
:::danger
| | 3.8 |
| ----------------------:| ----- |
| Marcel Szelwiga | X |
| Dominik Baziuk | X |
| | |
| | |
:::

:::info
**Uwaga:** Po rozwiązaniu zadania należy zmienić kolor nagłówka na zielony.
:::

## Zadanie 1
:::success
Autor: Adam Korta
:::

:::spoiler kod

class Filter implements Lock {
    int[] level;
    int[] victim;
    public Filter(int n) {
        level = new int[n];
        victim = new int[n]; // use 1..n-1
        for (int i = 0; i < n; i++) {
            level[i] = 0;
        }
    }
    public void lock() {
        int me = ThreadID.get(); // returns 0..n-1
        for (int i = 1; i < n; i++) { // attempt to enter level i
            level[me] = i;
            victim[i] = me;
            // spin while conflicts exist
            while (( ∃ k != me) (level[k] >= i && victim[i] == me)) {};
        }
    }
    public void unlock() {
        int me = ThreadID.get();
        level[me] = 0;
    }
}

:::

**Lemat:**
Na poziomie $i, 0 \leq i < n$ jest co najwyżej $n-i$ wątków.

**D-d:**
Przez indukcje po poziomach.

**Podstawa**
Dla $i = 0$ z konstruktora $Filter$ trywialne.

**Krok**
Załóżmy, że na poziomie $i$ znajduje się co najwyżej $n-i$ wątków. Pokażemy, że na poziomie $i+1$ znajduje się co najwyżej $n - (i + 1)$ wątków.

Załóżmy niewprost, że na poziomie $i+1$ znajduje się $n-i$ wątków.
Niech $A$ będzie ostatnim wątkiem, który ustawił $victim[i+1].$ Wtedy,
$\forall_B$ na poziomie $i+1$ zachodzi:
$write_B(victim[i+1]) \rightarrow write_A(victim[i+1])$
Z kodu:
$write_B(level[B] = i +1 \rightarrow write_B(victim[i+1]) \rightarrow write_A(victim[i+1] \rightarrow Read_A(level[B]$,
stąd wątek A zostaje ofiara i nie może wejść na poziom $i+1$, bo $\forall_B level[B] \geq j$, zatem **sprzeczność**

## Zadanie 2
:::success
Autor: Aleksandra Nicpoń
:::


Dowód przez odwróconą indukcję.

Podstawa indukcji: Poziom n-1 zawiera co najwyżej 1 wątek. Zagłodzenie na tym poziomie nie występuje.

Krok: Załóżmy że każdy wątek który dociera do poziomu j+1 lub wyżej w końcu dotrze do sekcji krytycznej.
Załóżmy nie wprost że pewien wątek A utknął na poziomie j. Wiemy z założenia indukcyjnego że na wyższych poziomach nie ma żadnego wątku. Jak tylko A ustawi level[A] = j to każdy wątek z poziomu j-1 nie może wejść na poziom j. To oznacza że żaen wątek nie wejdzie na poziom j z niższych poziomów.
Jeżeli A jest jedynym wątkiem który utknął na poziomie j to oznacza że w końcu wejdzie na poziom j+1. W przeciwnym przypadku wiemy że victim[j] może przyjąć tylko jedną wartość a zatem któryś z zablokowanych wątków przejdzie o poziomu j+1.

Lemat: Dla każdego poziomu i (i < n) i wątku w:
1. wątek przejdzie "kiedyś" na poziom (i+1).
2. wątek przejdzie "kiedyś" przez wsztystkie poziomy: (i+1)...(n-1)

Dowód ("odwrócona" indukcja):

1. podstawa indukcji: poziom (n-1). Niech identyfikator wątku = w. Z poprzedniego zadania wiemy, że na poziomie n-1 jest tylko jeden wątek, czyli w.

2. krok indukcyjny: poziom k (k < n-1). Niech identyfikator wątku = w. Dwa przypadki: a) victim[k] != w --- OK. b) victim[k] == w. Z pkt 2. założenia indukcyjnego wynika, że "kiedyś" poziomy (k+1)...(n-1) zostaną opróżnione z wątków, które się tam znajdują lub zostanie ustawiona wartość victim[k] != w. Wynika stąd, że wątek w opuści "kiedyś" pętle while i przejdze na następny poziom. Stąd warunek 1. jest spełniony. Spełnienie warunku 2. wynika z założenia indukcyjnego.

## Zadanie 3
:::success
Autor: Andrzej Morawski
:::

Rozpatrzmy wykonanie metody $lock()$ dla wątków $A$,$B$ i $C$.

**Wątek A:**
**1** $Write_A(level[A]=i) \Rightarrow Write_A(victim[i]=A) \Rightarrow ...$
**Wątek B:**
**2** $Write_B(level[B]=i) \Rightarrow Write_B(victim[i]=B) \Rightarrow ...$
**Wątek C:**
**3** $Write_C(level[C]=i) \Rightarrow Write_C(victim[i]=C) \Rightarrow ...$

W tej sytuacji wątek $C$ jest ofiarą i będzie musiał przepuścić pozostałe wątki na kolejne piętra.
Może dojść do takiej sytuacji, że po wyjściu z sekcji krytycznej wątki $A$ i $B$ ponownie będą chciały ponownie do niej wejść.
Bez straty ogólności możemy założyć, że wykonają one pierwszy poziom metody $lock()$ następująco:

$1 \Rightarrow 2$ Teraz wątek $B$ jest ofiarą i musi przepuścić pozostałe wątki. Jeżeli wątek $C$, który wcześniej był ofiarą zostanie uśpiony to może dojść do sytacji w której w tym czasie watek $A$ ponownie zacznie wykonywać metodę $lock()$ po wyjściu z sekcji krytycznej i wykonując $1$ przepuści wątek $B$, który był ofiarą i wątek $C$ nie zdąży się wybudzić.

Mimo tego, że algorytm nie jest $r$-ograniczony to spełnia on własność niezagłodzenia, ponieważ gdy wątek $C$ zostanie wybudzony nie będzie już ofiarą i będzie mógł wejść na wyższy poziom.

## Zadanie 4
:::success
Autor: Marcel Szelwiga
:::

public void lock() {
    flag[i] = true;
    victim = i;
    while (flag[j] && victim == i) {};
}

public void unlock() {
    flag[i] = false;
}

#### 1)
Zakładamy nie wprost, że $D_a \rightarrow D_b \wedge CS_b \rightarrow CS_a$

W takim wypadku musiały kolejno zachodzić, ze względu na relację ($\rightarrow$):

* $W_a($`flag[a] = true`$)$

* $W_a($`victim = a`$)$

* $W_b($`flag[b] = true`$)$

* $W_b($`victim = b`$)$

Skoro $b$ dostał się jako pierwszy do sekcji krytycznej to musiał odczytać `victim = a` -- zachodzi więc oczywista sprzeczność.

#### 2)

Mogło się zdarzyć tak, że:

* $W_a($`flag[a] = true`$)$

* $W_b($`flag[b] = true`$)$

* $W_b($`victim = b`$)$

* $W_a($`victim = a`$)$

Mamy więc $D_a \rightarrow D_b$ oraz $CS_b \rightarrow CS_a$ nie zachodzi więc własność FCFS.

#### 3)

* 1 - Sam odczyt nie wystarczy, ponieważ nie rozróżnimy sytuacji $D_a \rightarrow D_b$ od $D_b \rightarrow D_a$.

* 2 - Sam zapis do pliku nie wystarcza, ponieważ załóżmy $D_a \rightarrow D_b$ w takim razie
$CS_a \rightarrow CS_b$, dostajemy jakiś zapis zmiennych $S$.
Zauważmy, że w przypadku gdy $D_b \rightarrow D_a$ to stan zmiennych $S$ jest taki sam - brak odczytów.
A więc taki sam stan programu $S$ powinien raz wykonać $CS_a \rightarrow CS_b$, a raz $CS_b \rightarrow CS_a$.

* 3 - Zapis do tej samej komórki nie wystarcza, ponieważ sytuacja $D_a \rightarrow D_b$ jest nierozróżnialna od sytuacji z samym $D_b$.
## Zadanie 5
:::success
Autor: Mateusz Golisz
:::
Sekwencyjnie spójne:

Nie sekwencyjnie spójne:

## Zadanie 6
:::success
Autor: Arti Brzozowski
:::


Własność kompozycji mówi o tym, że jeżeli weźmiemy kilka sekwencyjnie spójnych obiektów to wynik ich kompozycji będzie sekwencyjnie spójny.


Skoro p jest kolejką oraz A ściąga z tej kolejki y, zatem y musiał być włożony do kolejki przed x
$(p.enq(y) B) \rightarrow (p.enq(x) A)$
podobnie
$(q.enq(x) A) \rightarrow (q.enq(y) B)$

Jednak z programu wynika
$(p.enq(x) A) \rightarrow (q.enq(x) A)$
$(q.enq(y) B) \rightarrow (p.enq(y) B)$
co tworzy cykl.

W powyższym przykładzie obiekty p i q są sekwencyjnie spójne, ale cała historia już nie jest.

## Zadanie 7
:::danger
Autor: do-deklarować
:::

## Zadanie 8
:::success
Autor: Martyna Wybraniec
:::

**Zadanie 8. Przypomnij dowód własności wzajemnego wykluczania dla algorytmu Petersona. Pokaż dlaczego ten dowód może się załamać dla procesora o modelu pamięci słabszym niż sekwencyjna spójność.**

public void lock() {
flag[i] = true;
victim = i;
while (flag[j] && victim == i) {};
}
public void unlock() {
flag[i] = false;
}


Dowód ten może się załamać dla procesora o słabszym modelu pamięci, ponieważ procesor może wykonać instrukcje w innej kolejności, np:
read_A(flag[B] == false) -> read_B(flag[A] == false) -> write_A(flag[A] = true) -> write_B(flag[B] = true)