Имя Лесли Лэмпорта, возможно, не является узнаваемым, но он стоит за несколькими великими проектами: программой для набора текста LaTeX и работой, которая сделала возможной облачную инфраструктуру в Google и Amazon. Он также уделил много внимания нескольким проблемам, дав им отличительные названия, такие как алгоритм пекарни и задача византийских генералов. Это не случайно. 81-летний учёный необычайно внимательно относится к тому, как люди используют программное обеспечение.
В 2013 году он выиграл Премию Тьюринга, считающуюся Нобелевской премией в сфере вычислительной техники, за его работу над распределенными системами, в которых несколько компонент в разных сетях координируются для достижения общей цели. Интернет-поиск, облачные вычисления и искусственный интеллект – все это требует совместной работы легионов мощных вычислительных машин. Конечно, такого рода координация создает много проблем.
«Распределенная система — это система, где сбой компьютера, о существовании которого вы даже не подозревали, может сделать ваш собственный компьютер непригодным для использования», — сказал однажды Лэмпорт.
Одним из самых больших источников проблем являются «параллельные системы», в которых несколько вычислительных операций выполняются в течение перекрывающихся отрезков времени, что приводит к двусмысленности: часы какого компьютера являются правильными? В основополагающей статье 1978 года Лэмпорт ввел понятие «причинности» для решения этой проблемы, используя идеи специальной теории относительности. Два наблюдателя могут не согласиться с порядком событий, но если одно событие вызывает другое, это устраняет двусмысленность. А отправка или получение сообщения может установить причинно-следственную связь между несколькими процессами. Логические часы – теперь также называемые часами Лэмпорта – давали стандартный способ рассуждать о параллельных системах.
Имея в руках этот инструмент, учёные затем задались вопросом, как они могут делать эти сети ещё больше, не добавляя ошибок. Лэмпорт придумал элегантное решение: Paxos, «алгоритм консенсуса», который позволяет нескольким компьютерам выполнять сложные задачи. Без Paxos и его семейства алгоритмов современные вычисления не могли бы существовать. В начале 1980-х годов, работая в этой сфере, Лэмпорт также создал LaTeX, систему подготовки документов, которая предоставляет сложные способы набора сложных формул и форматирования научных документов. LaTeX стал стандартом для форматирования статей не только по математике и информатике, но и по большинству научных областей.
Работа Лэмпорта с 1990-х годов была сосредоточена на «формальной проверке», использовании математических доказательств для проверки правильности программных и аппаратных систем. Примечательно, что он создал «язык спецификаций» под названием TLA+ (от Temporal Logic of Actions). Спецификация программного обеспечения подобна чертежу или рецепту программы; он описывает, как программное обеспечение должно вести себя на высоком уровне. Это не всегда необходимо, так как кодирование простой программы сродни варке яйца. Но более сложная задача с более высокими ставками — программирование, эквивалентное банкету из девяти блюд — требует большей точности. Вам нужно подготовить каждый компонент каждого блюда, точно соединить их, а затем подать каждому гостю в правильном порядке. Для этого требуются точные рецепты и инструкции, написанные недвусмысленным и лаконичным языком, но описания, написанные английской прозой, могут оставить место для неправильного толкования. TLA+ использует точный язык математики, чтобы предотвратить ошибки и избежать недостатков дизайна.
Используя ваш рецепт или спецификацию в качестве входных данных, программа, называемая проверкой модели, проверит, имеет ли рецепт смысл и работает ли он так, как задумано, готовя блюдо так, как того хочет шеф-повар. Лэмпорт сетует на то, что программисты часто собирают систему, прежде чем написать надлежащую спецификацию, тогда как повара никогда не будут обслуживать банкет, не зная заранее, что их рецепты сработают.
Quanta поговорила с Лэмпортом о его работе над распределенными системами, о том, что не так с образованием в области компьютерных наук и о том, как использование TLA+ может помочь программистам создавать более совершенные системы. Интервью было сокращено и отредактировано для ясности.
Интервью с Лесли Лэмпортом
— Начнем с Paxos, так как это такой важный алгоритм. Что заставило вас начать работать над ним в первую очередь?
Люди создавали систему с помощью какого-то кода, и у меня было предчувствие, что то, что их код пытается сделать, невозможно. Поэтому я решил попытаться доказать это и придумал алгоритм, который люди должны были использовать для своей системы.
— Что было не так с их первоначальным алгоритмом?
Ну, у них не было алгоритма, просто куча кода. Очень немногие программисты думают с точки зрения алгоритмов. При попытке написать параллельную систему, если вы просто кодируете ее без алгоритмов, ваша программа не может не быть полна ошибок.
— Публикация, в которой был представлен Paxos, поначалу не была широко принята. Почему это произошло?
Что сделало невозможным чтение публикации, так это то, что мне нравилось объяснять вещи историями, и я придумал имена персонажей псевдогреческими буквами. Например, в газете был инспектор сыра по имени Γωυδα. Выросший математиком, где повсюду использовались греческие буквы, я просто не знал, что нематематики совершенно сходят с ума от этих букв. Судя по всему, читатели не могли с этим справиться, и из-за этого публикацию не читали как положено.
Так что поначалу это не срабатывало. Хотя в конечном итоге его приняли, потому что люди называют это семейство алгоритмов Paxos, а не «viewstamped replication», что было иным названием того же алгоритма от Барбары Лисков.
— Что привело вас в TLA+ после стольких лет работы над распределенными системами?
В 1970-х годах, когда люди рассуждали о программах, они доказывали свойства самой программы, выраженные в терминах языков программирования. Затем люди поняли, что они действительно должны указывать, что программа должна делать в первую очередь – поведение программы.
В начале 1980-х я понял, что одним из практических методов написания этих высокоуровневых спецификаций для параллельных систем является их запись в виде абстрактных алгоритмов. С помощью TLA+ я смог выразить их математически совершенно строго. Это включает в себя, по сути, не попытки писать алгоритмы на языке программирования: если вы действительно хотите делать что-то правильно, вам нужно написать свой алгоритм в терминах математики.
— Вы сказали: «Если вы думаете, не записывая, вы только думаете, что думаете». Это то, где начинается проверка модели?
Проверка модели – это метод исчерпывающего тестирования всех исполнений небольшой модели системы. Это просто показывает правильность модели, а не алгоритма. В то время как проверка модели проверяет правильность, кодирование просто создает код. Это ничего не тестирует. До проверки модели единственным способом убедиться в том, что ваш алгоритм работает, было написать доказательство.
На практике проверка модели проверяет все выполнения небольшого экземпляра алгоритма. И если вам повезет, вы сможете проверить достаточно большие экземпляры, что придаст вам достаточно уверенности в алгоритме. Но доказательство может доказать правильность системы любого размера и любого использования алгоритма.
— Похоже, что проверка моделей связана с другим методом проверки программ: интерактивным доказательством теорем с использованием таких инструментов, как Coq. Насколько они разные?
Coq был разработан, чтобы заниматься реальной математикой и иметь возможность фиксировать рассуждения, которые делают математики. Это то, что Жорж Гонтье использовал, например, для доказательства теоремы о четырех красках. Машинно проверенное доказательство математического утверждения показывает, что утверждение почти наверняка верно.
TLA+ предназначен не для математиков, а для инженеров, которые хотят доказать свойства своих систем. В 1990-х, потратив около 15 лет на написание доказательств параллельных алгоритмов, я узнал, что нужно сделать, чтобы доказать правильность параллельного алгоритма. TLA была логикой, которая позволяла всему этому быть полностью формальным. И TLA+ – это полный язык, основанный на этом.
— Языки спецификаций, такие как TLA+, не очень широко используются в промышленности, верно? Как вы думаете, почему?
Ну, я делаю, что могу. Но в основном программисты и многие (если не большинство) учёных боятся математики. Так что это не легко.
Во-вторых, каждый проект делается в спешке. Есть старая поговорка: «Никогда не бывает времени, чтобы сделать это правильно. Всегда есть время всё переделать». Поскольку TLA+ требует предварительных усилий, вы добавляете новый шаг в процесс разработки, а это также не легко.
— Всегда ли предварительные усилия стоят этого?
Верно, большая часть кода, написанного программистами по всему миру, не требует очень точных указаний о том, что он должен делать. Но есть вещи, которые важны и должны быть корректными.
Когда люди создают чип, они хотят, чтобы этот чип работал правильно. Когда люди строят облачную инфраструктуру, они не хотят ошибок, которые могут привести к потере данных людей. Для приложений, где важна точность, вы должны быть очень строгими. И вам нужно что-то вроде TLA+, особенно если задействован параллелизм, который обычно присутствует в этих системах.
— Уверены ли программисты в том, что они тратят больше времени на написание кода, чем думают о нем?
Да, важность думать и писать свои мысли, прежде чем писать код, нужно преподавать на курсах информатики для студентов, а это не так. И причина в том, что нет связи между людьми, которые преподают программирование, и людьми, которые преподают верификацию программ.
Судя по тому, что я видел, вина лежит по обе стороны. Люди, преподающие программирование, не знают верификацию, которую им нужно знать. Люди, преподающие верификацию, не понимают, как ее применять и использовать на практике.
Пока этот разрыв не будет преодолен, TLA+ не найдет большого числа пользователей. Я надеюсь, что смогу хотя бы заставить людей, преподающих параллельное программирование, понять, что им это нужно. Тогда, возможно, есть какая-то надежда.
— У меня такое ощущение, что вы не слишком довольны образованием в сфере компьютерных наук. Это потому, что в них не уделяет должного внимания математике?
Математическому мышлению, верно.
— Как бы вы тогда построили программу бакалавриата?
Я не педагог, поэтому не знаю, как их этому научить. Но я знаю, чему люди должны были бы научиться. Им не следует бояться математики. Это простая математика, которую они, вероятно, изучали, но не знают, как ею пользоваться. Они не знают её пользы. Они узнают достаточно, чтобы сдать экзамен, а потом забывают об этом.
— Математики часто говорят, что видят красоту в математике. Вы начинали в этой сфере, так что вы видите красоту в алгоритмах?
Я не думаю об эстетике. У меня, вероятно, есть чувства, которые есть у иных людей, но я просто использую иные слова, чтобы выразить их. Быть красивым – это не то, что я бы сказал об алгоритме. Но простота – это то, что я очень ценю.
— И последнее, о другом вашем значимом проекте: LaTeX. Я хочу, наконец, прояснить кое-что с создателем. Как произносится Ла-тех или Лей-тех?
Как хотите. Не советую тратить много времени на размышления об этом.
Автор перевода @arielf
НЛО прилетело и оставило здесь промокод для читателей нашего блога: –15% на все тарифы VDS (кроме тарифа Прогрев) — HABRFIRSTVDS.
