Линеаризуемость: что значит «объект работает правильно»

Если ты знаешь, что такое история вызовов, точка линеаризации и чем линеаризуемость отличается от последовательной согласованности, листай до «Теперь сам».

Как думаешь, правильно ли

Клиент A положил в очередь 1 и получил ответ «готово». После этого клиент B положил 2 и тоже получил ответ. Ещё позже A забрал из очереди элемент - и получил 2. Очередь работает правильно?

Ответь себе до чтения. «Нет, очередь FIFO, первой должна выйти единица» - верно, если считать, что операции произошли в том порядке, в каком закончились. Но если требовать только, чтобы у каждого клиента порядок сохранялся, история допустима: можно считать, что B положил свою двойку раньше. Какое из двух требований правильное - и есть вопрос урока.

На что это похоже

Банковская выписка. Операции по счёту у разных людей идут одновременно, банк обрабатывает их как получится, но в выписке они выстроены в одну строку - и сумма в каждой строке согласуется с предыдущей. Хорошая выписка ещё и уважает время: если твой перевод выполнился и ты получил смс до того, как жена начала снимать наличные, в выписке перевод стоит раньше снятия.

Линеаризуемость - требование к выписке «уважай реальное время». Последовательная согласованность разрешает выписку, где снятие стоит раньше перевода, если они от разных людей.

Механизм: история, интервалы и точки

Пример объекта в уроке - очередь: enq(x) кладёт x в конец, deq() забирает элемент из начала (или отвечает «пусто»). История - записанные вызовы и ответы: операция deq клиента A началась в момент 4, закончилась в 5 и вернула 2. Каждая операция - интервал на оси времени. Интервалы разных клиентов могут перекрываться - это и есть одновременность.

Линеаризуемость: существует порядок всех операций, такой что (1) если операция закончилась раньше, чем началась другая, она стоит раньше и (2) порядок - допустимая последовательная работа объекта. Мысленно - каждая операция «срабатывает» в точке внутри своего интервала.

Последовательная согласованность требует того же, но в пункте (1) - только для операций одного клиента (клиент вызывает операции по одной, следующую - после ответа на предыдущую).

Два важных свойства. Линеаризуемость композиционна: система из линеаризуемых объектов линеаризуема целиком - каждый объект можно проверять отдельно (операция сразу над двумя объектами, вроде перевода между счетами, - уже свой объект, и её надо проверять как целое). Последовательная согласованность этим свойством не обладает. И проверка истории в общем случае NP-полна (Гиббонс и Кораш, 1997): перебор растёт экспоненциально, поэтому истории проверяют короткими.

Правило

История линеаризуема, если операции можно выстроить в один порядок, где закончившаяся раньше начала другой стоит раньше, и этот порядок - допустимая работа последовательного объекта. Последовательная согласованность требует сохранять только порядок каждого клиента. Линеаризуемость сильнее и композиционна; её проверяют перебором порядков, совместимых с реальным временем.

Разбор: проверка трёх историй очереди

Программа перебирает все порядки операций, разрешённые правилом, и считает те, при которых обычная очередь FIFO даёт ровно записанные ответы. Флаг linear выбирает правило: реальное время или только порядок клиента.

# операция: [клиент, начало, конец, "enq" или "deq", значение]
# у deq значение - что вернула очередь, "пусто" - если ничего
def mozhno_pervoj(h, k, ostalis, linear):
    # linear: раньше обязаны идти операции, ЗАКОНЧИВШИЕСЯ до её начала;
    # иначе (послед. согласованность) - раньшие у того же клиента
    for d in ostalis:
        if d == k:
            continue
        if linear and h[d][2] < h[k][1]:
            return False
        if not linear and h[d][0] == h[k][0] and h[d][1] < h[k][1]:
            return False
    return True

def poryadkov(h, ostalis, ochered, linear):
    # сколько порядков операций согласны и с правилом, и с очередью
    if len(ostalis) == 0:
        return 1
    vsego = 0
    for k in ostalis:
        if not mozhno_pervoj(h, k, ostalis, linear):
            continue
        # своя копия очереди у каждой ветки перебора
        q = ochered[:]
        if h[k][3] == "enq":
            q.append(h[k][4])
        elif len(q) == 0:
            if h[k][4] != "пусто":
                continue
        elif q[0] != h[k][4]:
            continue
        else:
            q.pop(0)
        drugie = []
        for d in ostalis:
            if d != k:
                drugie.append(d)
        vsego = vsego + poryadkov(h, drugie, q, linear)
    return vsego

istorii = [
    ["enq накрест", [["A", 0, 2, "enq", 1], ["B", 1, 3, "enq", 2],
                     ["A", 4, 5, "deq", 2], ["B", 4, 6, "deq", 1]]],
    ["enq по очереди", [["A", 0, 1, "enq", 1], ["B", 2, 3, "enq", 2],
                        ["A", 4, 5, "deq", 2]]],
    ["пусто при enq", [["A", 0, 4, "enq", 1],
                       ["B", 1, 2, "deq", "пусто"],
                       ["B", 5, 6, "deq", 1]]],
]
for imya, h in istorii:
    vse = list(range(len(h)))
    print(imya, "линеаризаций:", poryadkov(h, vse, [], True),
          "посл. согласованных:", poryadkov(h, vse, [], False))

enq накрест линеаризаций: 2 посл. согласованных: 2
enq по очереди линеаризаций: 0 посл. согласованных: 1
пусто при enq линеаризаций: 1 посл. согласованных: 1

«enq накрест»: две вставки перекрываются, два извлечения тоже. Линеаризаций две: «enq(2), enq(1), deq A → 2, deq B → 1» и «enq(1), enq(2), deq B → 1, deq A → 2» - извлечения перекрываются, и первым может сработать любое. «enq по очереди» - история из вопроса: линеаризаций ноль, последовательно согласованный порядок один. Очередь, которая так отвечает, неправильна: пользователь A видел, что его единица уже лежит в очереди, а получил двойку. «пусто при enq»: B получил «пусто», пока вставка A ещё не закончилась, - это допустимо, точка вставки просто позже точки извлечения.

Разбор: проверка реализации по записанным историям

Так проверяют настоящие системы: запускают много клиентов, записывают историю по часам одной машины, которая управляет тестом, и проверяют её. Возьмём счётчик «взять номер и прибавить»: последовательно он выдаёт 0, 1, 2, … Для него перебор не нужен: в любой линеаризации операции выдают 0, 1, 2, … по порядку, так что порядок задан самими номерами. Остаётся проверить, что номера различны и идут подряд и что операция, закончившаяся раньше, получила меньший. Сравним реализацию на CAS и реализацию «прочитал, потом записал».

import random

def zapisat(vid, n, operacij, seed):
    # n потоков вызывают «взять номер и прибавить»; планировщик даёт шаг
    # случайному потоку. История: [начало, конец, вернувшийся номер]
    random.seed(seed)
    c = 0
    faza = [0] * n
    prochital = [0] * n
    nachalo = [0] * n
    istoriya = []
    vremya = 0
    while len(istoriya) < operacij:
        t = random.randint(0, n - 1)
        vremya = vremya + 1
        if faza[t] == 0:
            nachalo[t] = vremya
            prochital[t] = c
            faza[t] = 1
        elif vid == "CAS":
            # сравнение и запись - один шаг модели, как инструкция CAS
            if c == prochital[t]:
                c = c + 1
                istoriya.append([nachalo[t], vremya, prochital[t]])
                faza[t] = 0
            else:
                prochital[t] = c
        else:
            c = prochital[t] + 1
            istoriya.append([nachalo[t], vremya, prochital[t]])
            faza[t] = 0
    return istoriya

def linearizuema(istoriya):
    # последовательно счётчик выдаёт 0, 1, 2, ...: номера различны,
    # и закончившаяся раньше операция получила меньший номер
    nomera = []
    for op in istoriya:
        nomera.append(op[2])
    if sorted(nomera) != list(range(len(istoriya))):
        return False
    for a in istoriya:
        for b in istoriya:
            if a[1] < b[0] and a[2] > b[2]:
                return False
    return True

for vid in ["CAS", "чтение и запись"]:
    plohih = 0
    for seed in range(40):
        if not linearizuema(zapisat(vid, 3, 12, seed)):
            plohih = plohih + 1
    print(vid, "- нелинеаризуемых историй из 40:", plohih)

CAS - нелинеаризуемых историй из 40: 0
чтение и запись - нелинеаризуемых историй из 40: 40

Сорок историй счётчика на CAS - все линеаризуемы: точка линеаризации каждой операции - её успешный CAS, и в этот момент она получает ровно следующий номер. Сорок историй счётчика без CAS - все неверны: два потока читают одно значение, и номер выдаётся дважды. Важно, что метод не смотрел внутрь реализации - только на вызовы, ответы и время. Поэтому им проверяют распределённые базы данных, куда внутрь не заглянуть. Сорок чистых историй при этом не доказательство: тест ловит ошибки, а правильность доказывает точка линеаризации.

Что ломается без этого

«Иногда отдаёт старое значение». Кеш, реплика или очередь, которые после подтверждённой записи отдают старое значение, - нарушение линеаризуемости. Клиенту это выглядит как потерянная запись.

Проверка по частям без композиционности. Два объекта по отдельности последовательно согласованы, а вместе дают историю, которую нельзя объяснить ни одним порядком. С линеаризуемыми объектами такого не бывает.

Длинные истории в проверщике. Перебор экспоненциален: история из тысячи перекрывающихся операций проверяется часами. Поэтому проверяют короткие истории, а длинные делят по независимым ключам: история каждого ключа проверяется отдельно - это разрешает композиционность.

Зачем это в работе

Jepsen - набор тестов, которым Кайл Кингсбери проверяет базы данных (etcd, MongoDB, PostgreSQL, Redis), записывает истории клиентов и проверяет их на линеаризуемость проверщиками Knossos, а позже Elle. Найденные нарушения - потерянные подтверждённые записи - становились исправлениями в этих системах. Документация etcd и ZooKeeper прямо говорит, какие операции линеаризуемы, а какие нет, - и это первое, что стоит прочитать, прежде чем строить на них распределённую блокировку.

Теперь сам

1. A: enq(1) в [0, 5], B: deq() → 1 в [2, 3]. Линеаризуема ли история?
2. A: write(x, 1) в [0, 1], B: read(x) → 0 в [2, 3]. Линеаризуема? Последовательно согласована?
3. Почему точка линеаризации счётчика на CAS - успешный CAS, а не чтение в начале операции?