# Współbieżne - lista 4

## Zadanie 1

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;
    }
}


## Dowód: Każdy wątek wykonujący metodę lock() znajduje się na jednym z n-1 poziomów, z których ostatni oznacza zajęcie zamka. Na poziomie n - i znajduje się jednocześnie co najwyżej i wątków.

## Indukcyjnie po i:

### Podstawa indukcji:

Na poziomie i = 0 znajduje się co najwyżej n - 0 wątków

### Krok indukcyjny:
Zał. ind. Co najwyżej n - i + 1 wątków weszło do poziomu i - 1

Zał. nie wprost, że n - i + 1 wątków weszło do poziomu i.

Niech A będzie ostatnim wątkiem, który zapisał do `victim[i]`, a B dowolnym innym wątkiem, który wszedł do poziomu i. Wtedy:

`write_B(level[B]=i) -> write_B(victim[i]=B) -> write_A(victim[i]=A) -> read_A(level[B]=i)`

Wątek A w pętli odczytuje `level[B]=i` oraz `victim[i]=A`, więc nie wejdzie do poziomu i.

Z tego wynika, że na poziomie n - 1 jest co najwyżej 1 wątek, więc warunek wzajemnego wykluczania jest zachowany

## Zadanie 2

## Indukcyjnie po i: Każdy wątek, który wejdzie do poziomu n - i, kiedyś wejdzie do sekcji krytycznej.

### Podstawa indukcji (i = 1):
Poziom n - 1 to sekcja krytyczna

### Krok indukcyjny
Zał. ind. Każdy wątek, który wszedł do poziomu n - i, kiedyś wejdzie do sekcji krytycznej.

Pokazać, że zachodzi dla n - i - 1

Zał. nie wprost, że wątek A wszedł do poziomu n - i - 1 i utknął na pętli, czyli zachodzi `level[A] = n - i` oraz `victim[n-i] = A`
- Żaden wątek nie wejdzie do poziomu n - i - 1, bo wtedy nadpisałby `victim[n-i]` i A mógłby przejść dalej
- Inne wątki chcące wejść do poziomu n-i wejdą, bo `victim[n-i] = A`

Z zał. ind. wszystkie wątki, które weszły do poziomu n-i wejdą do sekcji krytycznej, więc w pewnym momencie A będzie miał najwyższy poziom, czyli wyjdzie z pętli.

## Zadanie 3

**r-Bounded Waiting** to górne ograniczenie na ilość wątków, które mogą uzyskać dostęp do CS przed wątkiem A mimo że same zgłosiły chęć uzyskania dostępu później.

Załóżmy, że istnieje takie $r$, że operacja przejścia na kolejny poziom w metodzie lock() klasy Filter ma własność $r$-ograniczonego czekania.

Rozważmy takie wykonanie programu:
$$
n = 3\\
LV\text{ -przejście na wyższy poziom}\\
D_0^0\rightarrow D_1^0 \rightarrow D_2^0 \rightarrow LV_1^{0} \rightarrow D_1^1 \rightarrow LV_2^{0} \rightarrow D_2^1 \rightarrow\dots\rightarrow D_1^{r}\rightarrow D_2^{r}\rightarrow LV_1^{r} \rightarrow LV_0^{0}
$$
A zatem zachodzi:
$$
D_0^0\rightarrow D_1^0\\
LV_1^{r} \rightarrow LV_0^{0}
$$

Przyjmijmy, że mamy 3 wątki biorące udział w tym algorytmie.
1. Wątek 1 zaczyna wykonywać funkcję lock i dochodzi do momentu ustawienia $level[me] = 1$ oraz $victim[1] = me$. Tym samym wykonał DS. Wątek 1 zostaje wywłaszczony.
2. Wątek 2 zaczyna wykonywać funkcję lock i dochodzi do momentu ustawienia $level[me] = 1$ oraz $victim[1] = me$. Tym samym wykonał DS. Jest ustawiony jako victim i wątek 1 również posiada level[me]=1, więc wątek 2 czeka aż do wywłaszczenia
3. Wątek 3 zaczyna wykonywać funkcję lock i dochodzi do momentu ustawienia $level[me] = 1$ oraz $victim[1] = me$. Tym samym wykonał DS. Jest ustawiony jako victim i wątek 1 (oraz wątek 2) również posiada level[me]=1, więc wątek 3 czeka aż do wywłaszczenia
4. Procesor zostaje przekazany wątkowi 2. Nie jest on już jako victim, więc może wejść na wyższy poziom. Przechodzi przez wszyskie wyższe poziomy, bo warunek czekania nie będzie spełniony ($- ( ∃ k != me) (level[k]>=i)$) i wchodzi do CS. Po wykonaniu CS zaczyna znów wykonywać funkcję lock. Jest ustawiony jako victim i wątek 1 również posiada level[me]=1, więc wątek 2 czeka aż do wywłaszczenia.
5. Procesor zostaje przekazany wątkowi 3. Nie jest on już jako victim, więc może wejść na wyższy poziom. Przechodzi przez wszyskie wyższe poziomy, bo warunek czekania nie będzie spełniony ($- ( ∃ k != me) (level[k]>=i)$) i wchodzi do CS. Po wykonaniu CS zaczyna znów wykonywać funkcję lock. Jest ustawiony jako victim i wątek 1 również posiada level[me]=1, więc wątek 3 czeka aż do wywłaszczenia.

Kroki 4 i 5 mogą powtarzać się dowolną liczbę razy. Z każdym ich wykonaniem liczba wykonań sekcji krytycznej dla wątków 2 i 3 rośnie. Oznacza to, że różnica w liczbie wykonań sekcji krytycznej dla wątku 1 i któregokolwiek z wątków 2 i 3 może być dowolnie duża.

DONE

::: danger
# SKIP
## Zadanie 4
:::

## Zadanie 5


Po wykonaniu jako pierwsze `p.enq(x)` nie może zostać zwrócone y z `p.deq()`


## Zadanie 6

Podobnie jak wyżej, mamy już ustaloną kolejność wykonywania operacji na kolejce. Popatrzmy na kolejkę *p*:
$p.enq(x) \rightarrow p.enq(y) \rightarrow p.deq(y)$, czyli dokładnie jak w diagramie 3.

### Formalnie
* his. sekwencyjna - ciąg operacji wywołanie F, powrót F, wywołanie G, powrót G itd...
* his. ekwiwalentne - his. G jest ekwiwalentna do H jeśli w obrębie każdego wątku jest taka sama kolejność
* his. legalna - projekcja każdego z obiektów, na których działa ten wątek jest zgodna z **sekwencyjną specyfikacją** (warunki *preconditions*, *postconditions* itp...)

W żadnej z rozważanych przez nas sytuacji nie ma niedokończonych wywołań funkcji, więc nie musimy rozszerzać H do G poprzez dodawanie powrotów do takich funkcji, albo pozbywać się ich.

#### Diagram 1
Historia H i legalna, sekwencyjna historia ekwiwalentna, w której zachowujemy $\rightarrow_H$:

B r.write(1)    B r.write(1)
A r.read()      B r: void
C r.write(2)    A r.read()
A r: 1          A r: 1
C r: void       C r.write(2)
B r: void       C r: void
B r.read()      B r.read()
B r: 2          B r: 2


#### Diagram 2
Historia H i legalna, sekwencyjna historia ekwiwalentna, w której zachowujemy $\rightarrow_H$:

B r.write(1)    C r.write(2)
A r.read()      C r: void
C r.write(2)    B r.write(1)
A r: 1          B r: void
C r: void       A r.read()
B r: void       A r: 1
B r.read()      B r.read() 
B r: 1          B r: 1

#### Diagram 3
Historia H (jest sekwencyjna):

A p.enq(x)
A p:void
B p.enq(y)
B p:void
A p.deq()
A p:y


Musimy jednak zachować relację $\rightarrow_H$ - tutaj oznacza to, że nie możemy nic "poprzestawiać".

#### Diagram 4
Historia H (jest sekwencyjna):

A p.enq(x)
A p: void
B q.enq(y)
B p: void
A q.enq(x)
A q: void
B p.enq(y)
B p: void
A p.deq()
A p: y
B q.deq()
B q: x