# PRW 4
## Z1
### IMPLEMENTACJA ZAMKA DLA $N$ WĄTKÓW

class Filter implements Lock  {
    //informacje o poziomie każdego wątku
    int[] level;
    //informacje o wątku który jako ostatni zgłosił chęć zdobycia poziomu
    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
            // inny wątek jest na wyższym lub równym poziomie
            // i nasz wątek jako ostatni zgłosił chęć zdobycia poziomu
            while (( ∃ k != me) (level[k] >= i && victim[i] == me)) {};
        }
    }
    public void unlock() {
        int me = ThreadID.get();
        level[me] = 0; //zerujemy poziom wątku
    }
}

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


### DOWÓD SPEŁNIENIA WARUNKU WZAJEMNEGO WYKLUCZANIA
**Własności poziomów**
* Przynajmniej jeden wątek próbujący wejść na poziom $l$ odnosi sukces
* Przynajmniej jeden z wątków próbujących wejść w tym samym czasie na poziom $l$ zostaje zablokowany
* Każdy wątek musi przejść przez $n-1$ poziomów by się dostać do sekcji krytycznej

#### Dowód przez indukcję po liczbie poziomów $j$.
Niech $n$ oznacza liczbę wątków.
**Baza**
Wszystkie $n$ wątków znajduje się na poziomie $0$ od samego początku

**Krok**
Załóżmy nie wprost, że nie jest spełniona własność **przynajmniej 1 wątek nie może przejść na poziom $j$**, tj. że na poziomie $j-1$ zamiast $n-(j-1)$ wątków jest ich $n-j$

**Z kodu widzimy własności:**

- Niech $A$ będzie ostatnim wątkiem na poziomie $j$, który wykonał zapis w polu $victim[j]$.
Wtedy dla każdego innego wątku $B$ na poziomie $j$ mamy

write$_B$(victim[j]) -> write$_A$(victim[j])

- Wątek $B$ zapisuje $level[B]$ przed zapisaniem $victim[j]$

write$_B$(level[B] = j) -> write$_B$(victim[j]) -> write$_A$(victim[j])

- Wątek $A$ odczytuje $level[B]$ po zapisaniu $victim[j]$

write$_B$(level[B] = j) -> write$_B$(victim[j]) -> write$_A$(victim[j]) -> read$_A$(level[B])

Wątek $B$ znajduje się na poziomie $j$, za każdym razem, gdy wątek $A$ odczytuje wartość $level[B]$, otrzymuje wartość $>=j$, więc $A$ nie mógł ukończyć swojej pętli oczekiwania w linii $21$, sprzeczność

## Z2

class Filter implements Lock  {
    //informacje o poziomie każdego wątku
    int[] level;
    //informacje o wątku który jako ostatni zgłosił chęć zdobycia poziomu
    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
            // inny wątek jest na wyższym lub równym poziomie
            // i nasz wątek jako ostatni zgłosił chęć zdobycia poziomu
            while (( ∃ k != me) (level[k] >= i && victim[i] == me)) {};
        }
    }
    public void unlock() {
        int me = ThreadID.get();
        level[me] = 0; //zerujemy poziom wątku
    }
}

Dowód przez infukcję odwrotną na poziomach

#### Baza (poziom $n-1$):
Zawiera najwyżej jeden wątek

#### Krok
Załóżmy, że każdy wątek, który dotrze do poziomu $>=j+1$ osiągnie sekcję krytyczną
Załóżmy, że $A$ utknął na poziomie $j$.
Wtedy z pierwszego założenia, na wyższych poziomach nie ma wątków.
Kiedy $A$ ustawi $level[A]$ na $j$, to żaden z kolejnych wątków na poziomie $j-1$ nie będzie mógł wejść na poziom $j$, a wartości $victim$ i $level$ się już nie zmieniają.

Przypadki:
- Wątek $A$ jest jedynym wątkiem na poziomie $>=j$:
Wtedy wejdzie na poziom $j+1$
- Załóżmy, że na poziomie $j$ nie może utknąć mniej niż $k$ wątków, niech będą to między innymi wątki $A$ i $B$:
$A$ jest zablokowany tak długo, jak $victim[j]$ == $A$, $B$ tak długo jak $victim[j]$ == $B$
Jednak wartość $victim$ się nie zmienia i $A!=B$, więc jeden z nich przejdzie na poziom $j+1$, redukując liczbę zablokowanych wątków do $k-1$, sprzeczność

**Powyższy dowód również pokazuje własność niezakleszczenia**

## Z3

class Filter implements Lock  {
    //informacje o poziomie każdego wątku
    int[] level;
    //informacje o wątku który jako ostatni zgłosił chęć zdobycia poziomu
    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
            // inny wątek jest na wyższym lub równym poziomie
            // i nasz wątek jako ostatni zgłosił chęć zdobycia poziomu
            while (( ∃ k != me) (level[k] >= i && victim[i] == me)) {};
        }
    }
    public void unlock() {
        int me = ThreadID.get();
        level[me] = 0; //zerujemy poziom wątku
    }
}

SW - sekcja wejściowa (instrukcje przypisania `level[me]` i `victim[i]`)
Załóżmy, że uruchamiamy algorytm z użyciem 3 wątków

1. Wątek 1 wchodzi do `lock` i wykonuje SW (`level[me] = 1`, `victim[1] = me`) i zostaje wywłaszczony
2. W wątku 2 to samo co w kroku 1., jest ustawiony jako `victim`, zostaje wywłaszczony
3. W wątku 3 to samo co w kroku 2., jest ustawiony jako `victim`, zostaje wywłaszczony
4. Wątek 2 zostaje kontynuowany, wchodzi na wyższy poziom (`victim[1] = 3`). Warunek czekania w pętli `while` (linijka 21) nie jest spełniony, więc może przejść przez wszystkie następne poziomy, co też mu się udaje i wchodzi do CS. Po wykonaniu znów wykonuje `lock()`. Jest ustawiony jako `victim` i zostaje wywłaszczony.
5. W wątku 3 to samo co w kroku 4.

Może wystąpić sytuacja taka, że kroki 4 i 5 będą powtarzały się dowolną liczbę razy, zwiększając liczbę udanych wejść na wyższy poziom dla wątków 2 i 3, i nie zmieniając dla wątku 1, zatem ta różnica dla wątku 1 i któregoś z wątków 2 i 3 może być dowolnie duża, nie istnieje taka stała $r$, że operacja przejścia na kolejny poziom ma własność $r$-ograniczonego czekania

## Z4
chyba jakis skip material

## Z5


**Sekwencyjne** - nie nachodzą na siebie, zawsze następują jeden po drugim

**Historia** - skończona sekwencja zdarzeń wezwania i odpowiedzi metody.

Historia $H$ jest **linearyzowalna**, jeżeli może być rozszerzona do $G$ poprzez
- dołączenie odpowiedzi na zero lub więcej wezwań w toku
- ignorowanie pozostałych wezwań w toku
$G$ jest równoważna
- legalnej sekwencyjnej historii $S$
- gdzie $\rightarrow_G \subset \rightarrow_S$

1

Historia H

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

Legalna, sekwencyjna historia $S$, w której zachowujemy $\rightarrow_H$

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

$\rightarrow_H\subset\rightarrow_S$
$\rightarrow_H=$ {
B write(1) -> B read(),
A read() -> B read(),
C write(2) -> B read()
}
$\rightarrow_S=$ {
B write(1) -> A read() -> C write(2) -> B read()
}

2

Historia H

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

rownowazna poprawnej sekwencyjnie historii S

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

$\rightarrow_H \subset \rightarrow_S$
$\rightarrow_H=$ {
C write(2) -> B read(),
B write(1) -> B read(),
A read() -> B read()
}
$\rightarrow_S=$ {
C write(2) -> B write(1) -> A read() -> B read()
}
3

Historia H

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

nie jest linearyzowalna, ponieważ brakuje `p.deq(x)` przed `p.deq(y)` (nie zgadza się FIFO)

4

Historia H

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

czyli
p: x -> yx -> x
q: y -> xy -> y

ponownie historia nie jest linearyzowalna, ponieważ ani p ani q nie otrzymaliśmy efektów oczekiwanych od kolejek FIFO

między A: p.deq(y) i udanym zapisie x w A: p.enq(x) brakuje p.deq(x)
między B: q.deq(x) i udanym zapisie y w B: q.enq(y) brakuje q.deq(y)

## Z6

1
Jeżeli historia jest linearyzowalna to jest sekwencyjnie spójna.

B r.write(1) -> A r.read(1) -> C r.write(2) -> B r.read(2)

2
Jeżeli historia jest linearyzowalna to jest sekwencyjnie spójna.

C r.write(2) -> B r.write(1) -> A r.read(1) -> B r.read(1)

3
G

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

S

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

G jest ekwiwalentne do S
B p.enq(y) -> A p.enq(x) -> A p.deq(y)

4
G

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

Aby zachować własność FIFO muszą być spełnione warunki:
- p: B p.enq(y) ==1== -> A p.enq(x) ==2==
- q: A q.enq(x) ==3== -> B q.enq(y) ==4==

Aby zachować ekwiwalentność musi być:
A p.enq(x) ==2== -> A q.enq(x) ==3==
B q.enq(y) ==4== -> B p.enq(y) ==1==

sprzeczność, diagram nie przedstawia sekwencyjnie spójnych historii