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

## PRZYKŁAD UPIERDALAJĄCY LINEARYZACJE


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.