# L5 GRUPA 1

## Zadanie 1
:::success
Autor: Mateusz Kisiel
:::
### Sekwencyjnie spójne:
a)
b)
c)

### Sekwencyjnie niespójne:
a)
`p.enq(y)` musi być przed `p.enq(x)`, aby zgodziło się `p.deq(y)`, zatem także `q.enq(y)` musi być przed `p.enq(x)` czyli także przed `q.enq(x)`. Jednak wtedy `q.deq(x)` nie zwróci prawidłowej wartości.
b)
Pomiędzy write(0) a read(0) nie może być write(1), bo się zepsuje read(0), ani read(1), ponieważ nie zwróciłoby on prawidłowej wartości.
Analogicznie dla write(1) i read(1) - nic nie może być pomiędzy nimi.

Zatem jedyne możliwości to `write(1) read(1) write(0) read(0)`
oraz `write(0) read(0) write(1) read(1)`
Musi być jednocześnie zachowana kolejność funkcji w wątkach. Wątek pierszy wymaga najpierw operacji z zerami a nastepnie z jedynkami, a drugi odwrotnie. Sprzeczność.

## Zadanie 2
:::success
Autor: Jan Dalecki
:::

Własność kompozycji:

Jeżeli $H|p$ i $H|q$ są sekwencyjnie spójnie to $H$ jest sekwencyjnie spójne.

Przykład dla, którego tak nie zachodzi:


Nie możemy zmieniać kolejności wykonywanych operacji dla poszczególnych wątków. Możemy jednak przestawiać operacje na osi z zachowaniem ich kolejności wywołań. W powyższym przykładzie `p.enq(y)` powinno wykonać się przed `p.enq(x)` to implikuje, że `q.enq(y)` wykona się przed `q.enq(x)`.

## Zadanie 3
:::success
Autor: Marcin Wróbel
:::

public class WaitFreeQueue {
    int head = 0, tail = 0;
    items = (T[]) new Object[capacity];
    public void enq(Item x) {
        if (tail - head == capacity) throw new FullException();
        items[tail % capacity] = x;
        tail++;
    }
    public Item deq() {
        if (tail == head) throw new EmptyException();
        Item item = items[head % capacity];
        head++;
        return item;
    }
}

1. Tylko wątek używający metody **enq(Item x)** zmienia zmienną **tail**
2. Tylko wątek używający metody **deq()** zmienia zmienną **head**
Niech \[6, 2\) mod 8 oznacza liczby 6,7,0,1
4. Wątek **enq** może wstawiać elementy w przedziale od **\[tail, head\)** mod capacity
5. Wątek **deq** może wyciągać elementy w przedziale **\[head, tail\)** mod capacity
6. Powyższe przedziały są rozłączne
Na czerwono jest zaznaczony przedział dostępny przez wątek deq, na zielono zaznaczony jest przedział dostępny przez wątek enq
7. Każdy wątek najpierw wykonuje jakieś działanie na elemencie ze swojego przedziału i dopiero potem "oddaje" ten element do obsługi przez drugi wątek. Wątki mają tak jakby założonego lock'a na elementy w swoim przedziale
8. Powyższa własność (6) jest także, realizowana na maszynie z sekwencyjnie spójną pamięcią, ponieważ zależy nam tylko na tym, aby kolejność dostępów do pamięci była zachowana w obrębie wątku

Powyższa analiza omawia sytuację, gdy kolejka jest niepusta i niepełna

W sytuacji, gdy kolejka jest pusta punktami linearyzacji są

(tail == head)
tail++;

W sytuacji, gdy kolejka jest pełna punktami linearyzacji są

(tail - head == capacity)
head++;

Historie omawiane podczas prezentacji:

## Zadanie 4
:::success
Autor: Mikołaj Depta
:::

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

Przypomnienie dowodu, wazjemnego wykluczenia:

//A wszedł do sekcji krytycznej pierwszy.
write_A(flag[A] = true) -> 
write_A(victim = A) -> 
read_A(flag[B] == false) ->
read_A(victim = B) ->

// skoro B wszedł
read_B(flag[A] == false) -> write_A(flag[A] = true)

write_B(flag[B] = true) -> 
write_B(victim = B) -> 
read_B(flag[A] == false) -> 
read_B(victim = A) ->

Z powyższego można wyprowadzić sprzeczność.

write_B(flag[B] = true) ->
read_B(flag[A] == false) ->
write_A(flag[A] = true) ->
read_A(flag[B] == false)

Dlaczego algorytm może nie zadziałać.

> A load may be reordered with a prior store to a different location but not with a prior store to the same location.

Odczyt z pamięci, do której nie piszemy, może zostać wykonany w dowolnej kolejności względem wcześniejszych zapisów pod inny adres.

Oznacza, to że procesor może wykonać coś podobnego do takiego kodu.

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

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

Wówczas następujący przeplot spowoduje wejście dwóch wątków do sekcji krytycznej.

A: read(flag[B] == false)
A: *sleep*

B: read(flag[A] == false)
A: *wake*

A, B: write(flag[_] = true)
A, B: write(victim = _)
A, B: flag_temp (false) && victim == _ -> false
A, B: wejdź do sekcji krytycznej

## Zadanie 5
:::success
Autor: Wiktor Bukowski
:::


public class WaitFreeQueue {
    int head = 0, tail = 0; 
    items = (T[]) new Object[capacity];
    
    public void enq(Item x) {
        if (tail-head == capacity) 
            throw new FullException();
        temp = tail
        temp2 = temp + 1
        tail = temp2
        items[temp % capacity] = x;
    }
    public Item deq() {
        if (tail == head) 
            throw new EmptyException();
        Item item = items[head % capacity];
        head++;
        return item;
    }
}

Przykład niepoprawnego działania:
Przy wstawianiu elementu do kolejki `tail` najpierw zostaje zwiększony, a dopiero potem w odpowiednie miejsce tablicy wstawiany jest element. W tym samym czasie `deq` odczytuje nową wartość `tail` i próbuje odczytać element z tablicy, podczas gdy nie ma tam jeszcze pożądanego elementu.

## Zadanie 6
:::success
Autor: Bartosz Szczeciński
:::


class IQueue<T> {
    AtomicInteger head = new AtomicInteger(0);
    AtomicInteger tail = new AtomicInteger(0);

    T[] items = (T[]) new Object[Integer.MAX_VALUE];

    public void enq(T x) {
        int slot;

        do {
            slot = tail.get();
        } while (!tail.compareAndSet(slot, slot+1));

        items[slot] = x;
    }
    
    public T deq() throws EmptyException {
        T value;
        int slot;

        do {
            slot = head.get();
            value = items[slot];
            if (value == null)
                throw new EmptyException();
        } while (!head.compareAndSet(slot, slot+1));

        return value;
    }
}


1. A p.enq(x)
2. B p.enq(y)
3. B p:void
4. B p.deq()
5. B p:EmptyException
6. A p:void()

W tym wykonaniu wątek A zatrzymał się pomiędzy instrukcjami `tail.compareAndSet()` i `items[slot] = x`, czyli zarezerwował slot, ale jeszcze nie wstawił elementu do tablicy. Wątek B wykonał `enq()`, a później `deq()`, które zwróciło `EmptyException`, bo głowa wskazuje na `null`.

Taka historia nie jest linearyzowalna - `B.deq(x)` wykonuje się po operacji `B.enq(y)`, czyli mamy gwarancję, że w FIFO znajduje jakiś element, a mimo to dostajemy `EmptyException`. Jest to niezgodne z sekwencyjną specyfikacją FIFO.

## Zadanie 7
:::success
Autor: Andrzej Morawski
:::

public class HWQueue < T > {
    AtomicReference < T > [] items;
    AtomicInteger tail;
    static final int CAPACITY = Integer.MAX_VALUE;
    public HWQueue() {
        items = (AtomicReference < T > []) Array.newInstance(AtomicReference.class,
            CAPACITY);
        for (int i = 0; i < items.length; i++) {
            items[i] = new AtomicReference < T > (null);
        }
        tail = new AtomicInteger(0);
    }
    public void enq(T x) {
        int i = tail.getAndIncrement();
        items[i].set(x);
    }
    public T deq() {
        while (true) {
            int range = tail.get();
            for (int i = 0; i < range; i++) {
                T value = items[i].getAndSet(null);
                if (value != null) {
                    return value;
                }
            }
        }
    }
}

### Pierwsza instrukcja nie jest punktem linearyzacji:

$int$ $i = tail.getAndIncrement();$

Mamy zatem następujący ciąg instrukcji:


Jeżeli chcielibyśmy zlinearyzować tą historię względem pierwszej instrukcji metody enq() otrzymamy nastepującą kolejność:

A: enq(x)
B: enq(y)
B: deq(y)

Ponieważ wątek B jako piewszy przed wątekiem A zapisze swoją zmienną do kolejki to podczas wykontywania metody deq() kolejka zwróci wartość y, ponieważ $items[i]$ cały czas będzie równe null. Zatem jest to sprzeczne.

### Druga instrukcja nie jest punktem linearyzacji:

$items[i].set(x);$

Mamy zatem następujący ciąg instrukcji:


Jeżeli chcielibyśmy zlinearyzować tą historię względem drugiej instrukcji metody enq() otrzymamy nastepującą kolejność:

B: enq(y)
A: enq(x)
B: deq(x)

Pomimo, że wątek B zapisuje zmienną y do pamięci wcześniej niż wątek A, to index elementu x będzie mniejszy zatem podczas wyciągania elementu z kolejki najpierw zostanie wyciągnięty element x.

Dokładniej:
A: int i = tail .getAndIncrement(); // i == 0
B: int i = tail .getAndIncrement(); // i == 1
B: items[ 1 ]. set (y);
A: items[ 0 ]. set (x);
// według punktów linearyzacji kolejność elementów w kolejce to: y x
B: dequeue() // zwróci x
B: dequeue() // zwróci y

## Zadanie 8
:::success
Autor: Marcin Wróbel
:::


public class HWQueue < T > {
    AtomicReference < T > [] items;
    AtomicInteger tail;
    static final int CAPACITY = Integer.MAX_VALUE;
    public HWQueue() {
        items = (AtomicReference < T > []) Array.newInstance(AtomicReference.class,
            CAPACITY);
        for (int i = 0; i < items.length; i++) {
            items[i] = new AtomicReference < T > (null);
        }
        tail = new AtomicInteger(0);
    }
    public void enq(T x) {
        int i = tail.getAndIncrement();
        items[i].set(x);
    }
    public T deq() {
        while (true) {
            int range = tail.get();
            for (int i = 0; i < range; i++) {
                T value = items[i].getAndSet(null);
                if (value != null) {
                    return value;
                }
            }
        }
    }
}

Obserwacje:
1. Do każdej komórki w tablicy zapisze co najwyżej jeden wątek (dzięki temu, że metoda .getAndIncrement() jest wykonywana atomowo, będzie ona zwracać kolejne liczby naturalne).
2. Stąd metoda enq(T x) zawsze doda gdzieś w wolne miejsce x.
3. Każdy element komórki tablicy items zostanie wyciągnięty co najwyżej raz dzięki atomowej metodzie .getAndSet(null)
4. Wszystkie obiekty czekające w kolejce muszą mieć znajdować się w komórkach o indexie od 0 do tail. Stąd jeżeli jakiś element jest już w kolejce, to metoda deq(), go wyciągnie.

Początkowo możemy ustawić punkt linearyzacji deq w momencie wykonania items[i].getAndSet(null).

W przypadku, gdy kolejność deq nie zgadza się z kolejnością items[i].set(x), czasem można ustawić enq w kolejności zgodnej z tail.getAndIncrement()

    ↓                        ↓        ↓
A < i   enq(x)      set > <deq(x)> <deq(y)>
      ↓ 
B <   i  enq(y) set     >
                    

Może się jednak zdarzyć, że to nie zadziała, ponieważ jakiś wątek umożliwi przeskoczenie elementu z mniejszym indeksem, dodanym wcześniej, taka sytuacja jest możliwa tylko, gdy enq są współbieżne i jakieś inne enq zwiększyło wartość zmiennej tail. Wtedy należy ustawić punkt linearyzacji tak, aby były one ustawione zgodnie z kolejnoścjią deq.

                                                        ↓
A                    <  i enq(z)                       set >
                          ↓ 
B < i enq(x)               set > 
                       ↓
C                  < i enq(y)  set >
                                     ↓          ↓
D                         <        deq(y)>   <deq(x)>
                    

<!-- Należy jeszcze pokazać, że jeżeli
$enq(x)→enq(y)$, to
$deq(x)→deq(y)$

Załóżmy nie wprost, że
$enq(x)→enq(y)$ i
$deq(y)→deq(x)$

Skoro
$enq(x)→enq(y)$ to x znajdzie się w komórce o indeksie mniejszym niż indeks komórki w której znajduje się y
Musi zachodzić
$enq(y)→deq(y)$
Stąd
$enq(x)→enq(y)→deq(y)→deq(x)$
$enq(x)→deq(y)$
Wiemy, że x znajduje się w komórce o mniejszym indeksie niż y, stąd
deq(y) w swojej pętli natrafiłoby na x przed y -->