Интервью с Эдсгером В. Дейкстрой (2001), часть 2: программирование как искусство доказательств

Вторая часть интервью 2001 года Ф. Франы с Э. Дейкстрой.

Продолжаем вспоминать историю программирования, которая помогает ответить на вопрос, почему оно получилось таким, а не другим. Как зародились формальные методы программирования и актуальны ли они сейчас?

• в скобках квадратных [ ] указаны примечания самого интервьюера Ф. Франы;

• в скобках фигурных { } указаны мои уточнения.

В этом блоке привожу пояснения.

Скрытый блок

В этом блоке тоже пояснения для экономии места

Ссылки на источники в конце, но их сегодня мало, так как монологом высказывается одна мысль, и позиция её автора хорошо раскрывается и в этом интервью, и в отдельной заметке.

---

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

Итак, в 1958 году я сделал базовое программное обеспечение {basic software} и написал о нем свою диссертацию. Я защитил ее устно только годом позже, потому что написал ее на голландском языке.

Это было время, когда я не мог свободно писать по‑английски, и она была переведена с помощью южноафриканского коллеги. В 1959 году я опубликовал эти два алгоритма: кратчайший путь и минимальное остовное дерево.

У меня состоялась устная защита, и я стал доктором Дейкстрой {Dr. Dijkstra}. А в Математическом центре произошёл один примечательный случай. Я бросил вызов своим коллегам следующей задачей программирования.

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

«Синхронизируемся» в терминах и мы.

Герой интервью описал задачу, которая связана с синхронизацией доступа к критической секции в программах, работающих в многозадачной среде. Суть задачи заключалась в том, чтобы два процесса могли работать параллельно, но при этом гарантировалось, что они никогда одновременно не окажутся в своей критической секции — основа концепции взаимного исключения (mutual exclusion).

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

Многозадачная среда — окружение, в котором операционная система может выполнять несколько процессов одновременно.

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

Концепция взаимного исключения — принцип, который гарантирует, что критическая секция кода будет выполняться только одним процессом или потоком за раз.

В чём состояла сложность задачи?

На момент работы над этой проблемой (1960-е годы) ещё не существовало аппаратной поддержки синхронизации, и все механизмы приходилось реализовывать в программном обеспечении.

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

Это реализация проблемы взаимного исключения, которая позже стала краеугольным камнем системы THE Multiprogramming — лежащей в основе концепции монитора и множества вещей.

Операционная система «THE» (Technische Hogeschool Eindhoven) была разработана под руководством Дейкстры в 1960-е годы в Нидерландах. Пакетная система, поддерживающая многозадачность.

Монитор (monitor) — конструкция для управления доступом к общим ресурсам в многозадачной среде. Концепция мониторов была введена Пером Бринчи‑Хансеном (Per Brinch Hansen) и затем формализована Тони Хоаром (Tony Hoare). Но это уже 1970-е годы. Она легла в основу многих современных подходов к синхронизации потоков, например, в языках Java и C#.

Дейкстра говорит о том, что концепции, заложенные в THE, оказали значительное влияние на дальнейшее развитие.

Э. Дейкстра: Я посмотрел на это и понял, что это {решение этой задачи} совсем нетривиально, были всевозможные дополнительные условия. Например, если одна из программ будет оставаться очень долго вне критической секции, другая должна иметь возможность работать беспрепятственно, поэтому поочерёдное переключение в критическое состояние не допускалось.

Ещё одно недопустимое явление — то, что мы называли блокировкой «after‑you‑after‑you» когда программы конкурировали за доступ к критической секции, и дилемма никогда не решалась.

Ситуация «after‑you‑after‑you» — когда оба процесса бесконечно «уступают» друг другу («после‑тебя‑нет‑после‑тебя»), что приводит к блокировке обоих.

Мои друзья из Математического центра представили свои решения, но все они были неверными. Для каждого предлагаемого решения я набрасывал сценарий, который выявлял ошибку. Затем происходило следующее: люди делали свои программы более изощрёнными, более сложными, и через один или два дня они приходили с новой версией. Она тоже была неправильной, только построение и контрпримеры стали ещё более трудоёмкими, и мне пришлось изменить правила игры. Я говорил: «Сэр, извините, но я больше не могу тратить все свои дни на опровержение результатов ваших тщетных усилий. С этого момента я принимаю только решение с обоснованием, почему это правильно.»

Ф. Франа: Имеется в виду корректность программы?

Здесь не очень поняла, почему интервьюер переспрашивает, потому что последнее предложение весьма понятно: «Sir, sorry but I can no longer spend all my days refuting your vain efforts. From now onwards I only accept a solution with an argument why it is correct.» Возможно, ответ был длинным, и он упустил нить повествования, слушать — не читать. Или даёт своему герою интервью понять, что он его слушает, переспрашивая последнюю мысль, опять же, из‑за достаточно длинного ответа со множеством деталей.

Э. Дейкстра: Да, и примерно через три часа Теун Дж. Деккер (Th. J. Dekker) представил идеальное решение и доказательство его правильности.

Речь идёт о том, что позднее назовут алгоритмом Деккера.

Он проанализировал, какое доказательство потребуется. Что мне нужно показать? Как я могу это доказать? Какова будет приемлемая структура доказательства правильности? Установив это, он написал программу, которая соответствовала требованиям доказательства.

Что очень ясно показывает, что вы много теряете, если ограничиваете роль математики проверкой программы, а не построением или выводом программы. Вот чему мы научились из соревнования, которое выиграл Деккер. (Извините меня на минуту.)…

---

Здесь конец диалога второй части интервью, поэтому рассмотрим поподробнее, о чем говорит Дейкстра.

Ранее он сказал про разные подходы к программированию, очевидно, что «американский» он не поддерживает. Он использовал пример с решением задачи, чтобы продемонстрировать, какой подход он считает правильным.

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

Герой интервью убеждён, что математика должна быть основой для построения или вывода программы. Это означает, что вместо того, чтобы писать код интуитивно, а затем доказывать его правильность, следует делать следующее:

1. Формализовать требования к программе.

2. Найти доказательства, что эти требования достижимы.

3. Разработать алгоритм, который вытекает из доказательства.

Какие требования следовало формализовать Деккеру, чтобы написать программу?

1.1. Взаимное исключение (Mutual Exclusion)

В любой момент времени только один процесс может находиться в критической секции.

Формула:

CS₁ и CS₂ — логические переменные (Critial Section, критическая секция), указывающие, находится ли процесс P₁​ или P₂ в критической секции соответственно.

∧ — логическое И, указывает, что оба процесса P₁​ или P₂ одновременно в критической секции.

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

Библиотека с уникальной редкой книгой. Если один читает её в зале, второй читатель должен подождать, пока книга освободится.

1.2. Отсутствие взаимной блокировки (No Deadlock)

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

Формула:

want₁ ​ и want₂ — логические переменные, обозначающие желание процессов P₁ и P₂ войти в критическую секцию. Они могут принимать значение «истина» или «ложь».

∧ — логическое И; want₁​ ∧ want₂​: оба процесса хотят войти в критическую секцию (обе переменные — «истина»).

⟹ — логическая ИМПЛИКАЦИЯ («если, то»), если левое условие истинно, то правое должно быть истинным.

∨ — логическое ИЛИ; CS₁ ​∨ CS₂​: в критической секции находится либо первый процесс P₁, либо второй P₂ (или оба). «Или оба» в данном случае исключается первым пунктом «1. Взаимное исключение», поэтому считаем, что в критической секции находится либо один, либо другой.

Получаем: «Если оба процесса хотят войти в критическую секцию, то хотя бы один из них должен войти.»

Двое хотят пройти через узкую дверь. Если оба уступают друг другу («проходи первым»), это может продолжаться бесконечно.

1.3 Ограничение ожидания (Bounded Waiting)

Каждый процесс, который хочет войти в критическую секцию, рано или поздно сможет это сделать.

Формула:

и

want₁ ​ и want₂ — логические переменные, обозначающие желание процессов P₁ и P₂ войти в критическую секцию. Они могут принимать значение «истина» или «ложь».

⟹ — логическая импликация («если, то»), если левое условие истинно, то правое должно быть истинным.

◊ — модальный оператор, обозначающий, что выражение в конечном итоге станет истинным («рано или поздно»).

want₁​⟹◊CS₁​ означает: если процесс P₁​ хочет войти в критическую секцию, то он рано или поздно получит доступ после P₂​, даже если в это время процесс P₂​ находится в критической секции.

Аналогично со вторым процессом.

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

1.4 Справедливость (Fairness)

Если процессы чередуются, то доступ к критической секции распределяется равномерно, без бесконечного ожидания.

Формула:

и

∀t — квантор всеобщности («для всех моментов времени t»).

CS₁ и CS₂ — логические переменные (Critial Section, критическая секция), указывающие, находится ли процесс P₁​ или P₂ в критической секции соответственно.

¬ — логическое «НЕ», ¬want ₂ — ложь, процесс P₂ не хочет войти в критическую секцию

∨ — логическое «ИЛИ»

turn — переменная, которая указывает, чей ход войти в критическую секцию, принимает два значения: 1, 2. Если turn = 2: очередь процесса P₂.

Первая формула означает: для каждого момента времени, если процесс P₁ в критической секции, то либо процесс P₂ не хочет входить в секцию ¬want₂ (например, не требуется ему сейчас читать и писать в общее хранилище), либо очередь стоит на P₂ (turn=2), т.е. только P₂ может потом войти.

Использование одной кофемашины на работе. Каждый из двух сотрудников может приготовить кофе только после того, как предыдущий сотрудник закончит. Если один сотрудник приготовил кофе, следующий сотрудник получает возможность использовать кофемашину. Справедливость здесь заключается в том, что каждый сотрудник по очереди использует кофемашину, и никто не ждет свою очередь бесконечно долго.

Если упростить описание формальных требований

• «Один за всех» — взаимное исключение.

• «Если оба хотят, кто-то должен пройти первым» — отсутствие взаимной блокировки.

• «Каждый дойдёт до своей цели» — ограниченное ожидание.

• «По очереди, без обид» — справедливость.

Что сделал Деккер?

• Деккер проанализировал задачу математически, выявив ключевые требования, провёл доказательства достижимости.

• Построил алгоритм, который соответствовал этим требованиям, основываясь на строгом доказательстве корректности. Это показывает силу подхода, когда программа создаётся не методом проб и ошибок, а выводится из доказательства.

В чём назидание Дейкстры?

• Он критиковал популярную в то время практику, при которой программы писались сначала, а затем «лепились заплатки», чтобы исправить ошибки.

• Он считал, что подход, где доказательство корректности является основой для построения программы, намного эффективнее и надёжнее.

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

Применимо ли это сейчас?

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

Использование формул непопулярно в повседневной разработке (особенно в приложениях, где скорость важнее строгости).

В чем проблемы:

• Требуются хорошие знания в математических областях для формализации требований.

• Проблемы в многозадачных системах трудно формализовать.

• Для работы с формальными методами нужно уметь пользоваться специальными инструментами.

• Требуется значительные временные и трудовые затраты.

• Абстракции трудны для поддержки.

Для большинства популярных задач (например, разработки веб‑приложений или мобильных приложений) использование формальных методов излишне и неоправданно с точки зрения затрат времени и ресурсов.

Почему это важно сегодня?

Сегодняшние системы (распределенные базы данных, облачные платформы, мультипоточность) гораздо сложнее, чем программы времен Дейкстры. Ошибки в таких системах могут быть критичными.

Например, TLA+ используется компаниями вроде Amazon, Oracle и Microsoft для проверки распределенных систем (работы облаков или согласованности данных).

TLA ⁺ — это формальный язык для спецификации систем, используемых в промышленности и академии для проверки сложных распределенных и параллельных систем.

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

Использование формальных методов технологические гиганты продвигают среди своих команд, создавая культуру, в которой эти инструменты становятся неотъемлемой частью проектирования и разработки. Пример — ежегодная конференция TLA⁺ conference https://conf.tlapl.us/home/.

Конец перевода и разбора второй части интервью.

Ссылка на первую часть

---

_{Использованные источники:}

_{Интервью: Oral history interview with Edsger W. Dijkstra https://works.bepress.com/philip_frana/6}

_{Заметка: Edsger W. Dijkstra Cooperating sequential processes https://www.cs.utexas.edu/~EWD/transcriptions/EWD01xx/EWD123.html}