Кратко

  • Happened-before — наименьший частичный порядок, порождённый локальной последовательностью процесса, отправкой до получения того же сообщения и транзитивным замыканием этих связей.
  • Clock Condition работает в одну сторону: a → b требует C(a) < C(b). Меньшее скалярное значение не доказывает, что a вызвало, проинформировало или физически предшествовало b.
  • Конкурентные события не имеют пути happened-before ни в одном направлении. Это означает отсутствие порядка в наблюдаемой модели, а не один момент физических часов.

Два сервиса оставляют будто бы решающие записи. Событие A получает логическое время 41, B — 42. Панель сортирует строки, рисует стрелку и подталкивает команду сказать, что A вызвало B. Числа делают рассказ простым, но не делают его доказанным.

Работа Leslie Lamport 1978 года Time, Clocks, and the Ordering of Events in a Distributed System не искала скрытые всемирные часы. Она точно определила, какой порядок распределённая система вправе обосновать без них.

Наименьший порядок из наблюдаемых рёбер

Lamport описывает процессы с последовательностями событий, связанные сообщениями. Happened-before — наименьшее отношение с тремя правилами: раннее событие процесса предшествует позднему; отправка предшествует получению того же сообщения; отношение транзитивно.

«Наименьшее» сохраняет пробелы. Если нет ни a → b, ни b → a, события конкурентны. Модель не заполняет неизвестное догадкой ради аккуратной шкалы времени.

Lamport толкует a → b как возможность причинного влияния a на b. Существует путь, по которому могла пройти информация. Это не доказательство того, что содержание a фактически изменило результат b, что человек намеревался получить эффект или что ответственность установлена. Причинная достижимость и смысловая причина требуют разных доказательств.

Порядок зависит даже от определения события. В примечании получение сообщения может означать установку бита прерывания или выполнение обработчика; выбор меняет порядок. Поэтому до вопроса «что было раньше» нужна версия того, что считается событием.

Импликация без обратного вывода

Логические часы присваивают событию число. Clock Condition говорит: если a → b, то C(a) < C(b). Процесс увеличивает счётчик между событиями, прикладывает значение к сообщению и при получении переводит свои часы за текущее и полученное значения.

Эти правила сохраняют известные стрелки. Они не разрешают обратный вывод: из C(a) < C(b) не следует a → b.

Это структурная граница, а не мелкий недостаток. Если бы каждое числовое сравнение доказывало happened-before, конкурентные события должны были бы иметь одинаковое значение. Но одно событие может быть конкурентно двум событиям другого процесса, которые упорядочены между собой; равенство всех трёх нарушило бы локальный порядок.

Скалярные часы подтверждают, что известное ребро не перевёрнуто числами. Они не подтверждают причинное ребро для каждой возрастающей пары.

Полный порядок — политика, а не восстановленный мир

Некоторым приложениям нужен один выбор там, где частичный порядок допускает несколько. Lamport сортирует по логическому времени и разрывает равенство фиксированным порядком процессов. Получается полный порядок, согласованный с happened-before.

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

Очередь или репликация вправе выбрать детерминированную последовательность. Важно записать tie-break как правило управления. Если выдать его за открытие прошлого, операционное решение станет ложным историческим фактом.

Телефонный звонок вне системы

В примере «аномального поведения» человек отправляет запрос A на одном компьютере, звонит другу в другом городе и просит отправить B. Телефон не относится к компьютерной системе, поэтому B может получить меньшую метку и оказаться перед A.

Алгоритм, наблюдающий только внутренние события, не восстановит ребро, которого никогда не видел. Lamport предлагает явно внести недостающую информацию о порядке либо использовать достаточно синхронизированные физические часы при более сильных предположениях.

Сегодня пропущенным ребром может быть звонок поддержки, человеческое согласование, webhook или внешняя очередь. «Путь не найден» означает «пути нет в этой выборке», а не «в мире не было влияния».

Логическое, векторное и физическое время

Скалярные часы Lamport сохраняют требуемую импликацию и позволяют построить согласованный полный порядок. Примерно десять лет спустя Colin Fidge и Friedemann Mattern разработали векторные структуры, сохраняющие больше частичного порядка. Mattern отметил, что отображение в линейные целые числа теряет информацию: возможно конкурентные события получают разные значения, словно их порядок определён.

Векторы могут оставаться несравнимыми, когда ни одно событие не входит в причинное прошлое другого. Это важно для отладки, снимков и конфликтов. Но результат всё равно зависит от записанных процессов, событий и сообщений; он не обнаруживает отсутствующий звонок и не доказывает мотив человека.

Физические часы отвечают на другой вопрос. Та же статья Lamport рассматривает Strong Clock Condition, ошибку хода, дрейф, минимальную задержку сообщений и пределы синхронизации. Эти предположения приближают метки к физическому времени с указанной неопределённостью; они не делают логический счётчик настенными часами.

Границы авторства также важны. Lamport формализовал happened-before и скалярные логические часы, указав на более раннюю идею временных меток в сообщениях Paul Johnson и Bob Thomas. Векторные часы относятся к последующим работам Fidge и Mattern.

Что должно сопровождать заявление о порядке

Защищаемое расследование называет определение и версию события, процесс, локальную последовательность, ID сообщения, пару отправка–получение, алгоритм часов и границу телеметрии. Для физического порядка добавляются источник и ошибка часов; для причины — механизм, изменивший результат.

Тогда вывод может быть точным: happened-before в захваченной модели; конкурентно в ней; поставлено раньше правилом tie-break; физически раньше в пределах ошибки; либо смысловая причина пока не доказана.

Вклад Lamport — не разрешение отсортировать всё и назвать правдой. Это способ отделить порядок, который система знает, от порядка, который она выбирает, и от порядка, который пока не может доказать.

Источники