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

Вторая часть интервью 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. Деккер проанализировал задачу математически, выявив ключевые требования.

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

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

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

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

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

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

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

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

Интервью: 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

© Habrahabr.ru