# L4 - zarys teoretyczny (bez wyprowadzenia wzorów)

* Algorytm piekarni

class Bakery implements Lock {
    boolean[] flag;
    Label[] label;
    public Bakery (int n) {
        flag = new boolean[n];
        label = new Label[n];
        for (int i = 0; i < n; i++) {
            flag[i] = false; label[i] = 0;
        }
    }
    public void lock() {
        int i = ThreadID.get();
        flag[i] = true;
        label[i] = max(label[0], ...,label[n-1]) + 1;
        while ((∃k != i)(flag[k] && (label[k],k) << (label[i],i))) {};
    }
    public void unlock() {
        flag[ThreadID.get()] = false;
    }
}


wzajemnie wykluczenie dla n wątków, fcfs

jest **deadlock-free**, ponieważ istnieje wątek z unikatowym najmniejszym (label[i], i), który nie czeka na żaden inny wątek
jest **fcfs**, ponieważ jeśli wątek **A** jako pierwszy wykonał **doorway-section**, to wątek **B** ma na pewno większy swój `label[i]`, flaga wątku **A** jest zapalona, więc wątek **B** nie wyprzedzi **A**
jest **starvation-free**, ponieważ jednocześnie **deadlock-free** i **FCFS** implikują **starvation-free**

* **Filter lock**
generalizacja Petersona dla n wątków
przed wejściem do sekcji krytycznej wątek musi przejśc przez **n-1** poziomów
jeśli więcej niż jeden wątek próbuje wejść na jakiś poziom, to przynajmniej jeden wątek się tam zablokuje
ogólnie dla j pomiędzy 0 i n-1 na poziomie j jest co najwyżej n-j wątków
nie istnieje r t.ż. przejście na kolejny poziom ma własność r-ograniczonego czekania (dla 3 wątków jeden z nich może zatrzymać się na jednym poziomie, a dwa pozostałe przeskakiwać do sekcji krytycznej na zmianę)

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

* **nieformalna def. linearyzacji:**
* **formalna def. linearyzacji**

przykład l4z6

* **Sekwencyjna spójność**
(przykład slajd 158 prw3)

* **Własność kompozycji:**

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

* Sekwencyjna spójność nie ma własności kompozycji (l5z2)