Лесли Лэмпорт

Шалыто А.А.

Лесли Лэмпорт (Leslie Lamport) родился в 1941 году. Имеет три степени по математике: бакалавр – в MIT (закончил в 1960 году), магистр – в Brandeis University (1963), Ph.D – в Brandeis University (1972). С работал в MIT, DEC и Compaq, с 2001 года – Principal Researcher в Microsoft Research. 

Лэмпорт рассказывает о себе: «Я никогда не изучал информатику формально – не прослушал ни одного курса. Наибольшее влияние в этом вопросе на меня своими статьями оказал Дейкстра. Я начал серьёзно программировать после окончания школы и подрабатывал этим во время дальнейшей учёбы. Я никогда не связывал математику и программирование, хотя когда-то – ещё в начале 1960-х – мне приходила в голову идея компьютерно-проверяемых математических доказательств. Тогда мне казалось, что написать такое доказательство будет раза в четыре труднее обычного. Я рассказал об этом своим преподавателям, но они сказали, что это ужасная идея – «убьёт всю прелесть математики». Я тогда оставил это, но через много лет вернулся к этой идее».

У Лэмпорта есть домашняя страница, которая состоит из двух частей My Writings, на которой он обсуждает свои публикации, и My TLA+ Home Page.

Библиографические показатели Лэмпорта: h-index – 87, citations – 94 027 (на 10.01.2026 года).

1.   Мотивация Лэмпорта на исследования по компьютерным наукам. Как отмечено выше, Лэмпорт получил PhD по математике в 1972 году. Именно тогда он взглянул на зарождающуюся область компьютерных наук и увидел не новую дисциплину, а хаос вместо неё. Мир вычислений был цифровым диким Западом, населённым хакерами, которые строили огромные сложные системы методом проб и ошибок. Их код держался в основном на надежде. Лэмпорт покинул мир чистой математики, чтобы привнести её силу в эту новую область.

Ему очень не нравился слоган, характерный для деятельности программистов: «Двигайся быстро и ломай вещи». Они очень гордились интуицией и тем, как они нащупывали решения проблем, а ошибки исправляли по мере их появления. Скорость написания программ тогда ценилась превыше всего.

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

По мнению Лэмпорта, главная причина, по которой современное ПО содержит много ошибок, состоит в том, что программисты после получения задания сразу же переходят к написанию кода. Архитекторы в строительстве зданий рисуют подробные планы до того, как будет положен первый кирпич или забит первый гвоздь. Однако только немногие программисты выполняют даже грубый набросок того, что будут делать их программы, прежде чем начнут кодировать. Программистов привлекает кодирование, потому что код – это то, что работает. Трата времени на что-то ещё кажется им недопустимым.

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

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

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

2. Классы вычислений. Лэмпорт делит вычисления на два класса: нераспределённые вычисления – когда процессы взаимодействуют, используя общую память, и распределённые вычисления – когда они взаимодействуют друг с другом, посылая сообщения.

Он вводит также понятие «конкурентная система»: в ней несколько процессов работают независимо, но обмениваются сообщениями. Распределённая система – это подкласс «конкурентных систем», в которой время обмена сообщениями велико по сравнению с временем локальных действий.

3. Нераспределённые вычисления. В работе Lamport L. A New Solution of Dijkstra`s Concurrent Programming // Communication of ACM. 1974. Vol. 17. № 8, pp. 453-455  описан алгоритм «пекарни» (Bakery Algorithm) для решения проблемы взаимного исключения (Mutual Exclusion) в системах с N асинхронными процессорами, общающимися через разделяемую память. Алгоритм устойчив к сбоям отдельных компонентов. В нём не используется понятие «State Machine» (машина состояний).

Этот алгоритм имеет такое название, так как Лэмпорт предложил в качестве модели решаемой задачи рассмотреть пекарню с устройством, выдающим номерки у входа. Каждому входящему покупателю выдаётся номерок на единицу больше предыдущего. Общий счётчик показывает номер обслуживаемого в данный момент клиента. Все остальные покупатели ждут, пока не закончат обслуживать текущего клиента, и табло покажет следующий номер. После того, как клиент сделает покупку и сдаст свой номерок, служащий увеличивает у входа на единицу допустимые для выдачи устройством номера. Если совершивший покупку клиент захочет снова что-нибудь купить, он должен будет снова взять у входа номерок и встать в общую очередь. Этот алгоритм также называется алгоритмом Лэмпорта, алгоритмом булочной или Lamport's bakery algorithm. Вот видео на эту тему: Lamport on discovering the Bakery Algorithm.

В этом видео Лэмпорт говорит: «Любимый из моих алгоритмов – алгоритм пекарни. Он потрясающе красив, и я горжусь тем, что наткнулся на эту идею​».

4. Распределённые вычисления. Вот что рассказывает Лэмпорт о том, как он стал заниматься этой тематикой: «Распределённая система – это такая система, в которой Ваш компьютер может стать бесполезным из‑за отказа другого компьютера, о существовании которого Вы даже не подозревали.

Мой интерес к распределённым системам появился случайно. В 1975 году я получил препринт  статьи Роберта Томаса (Robert Thomas) и Пола Джонсона (Paul Johnson), в которой был описан алгоритм для реализации распределённых баз данных – таких баз, в которых может быть несколько копий данных на разных компьютерах для того, чтобы программы на каждом компьютере имели быстрый доступ к данным.​ Эти копии должны были быть синхронизированы, чтобы процессы на всех компьютерах получали согласованное представление о том, какими являются данные.

Так получилось, что я довольно хорошо разобрался в специальной теории относительности. Она, в частности, учит, что у двух разных наблюдателей разные представления о том, что значит «одновременность».​ Однако, есть понятие, которое в этом вопросе инвариантно – это понятие «одно событие произошло раньше другого». Я понял, что это понятие причинности нарушается алгоритмом Томаса и Джонсона. Тогда я написал статью, в которой объяснил это понятие.

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

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

В работе Lamport L. Time, Clocks and the Ordering of Events in a Distributed System // Communications of the ACM. 1978. Vol. 21, № 7, pp. 558-565 рассматривается концепция того, что одно событие в распределённой системе происходит раньше другого, и показано, что это определяет частичный порядок событий. Предлагается распределённый алгоритм для синхронизации системы логических часов, который может быть использован для полного упорядочивания событий. Применение такого упорядочивания иллюстрируется на примере метода решения задач синхронизации. Затем алгоритм специализируется на синхронизации физических часов, и выводится оценка того, насколько сильно могут выйти из синхронизации часы. После этой статьи появилось понятие «Часы Лэмпорта».

Это самая цитируемая статья Лэмпорта. Вот его мнение о ней: «Кажется, статья чему-то научила людей, хотя я сам не до конца уверен, чему именно. Важная её часть – идея реализации распределённой системы как распределённой реализации машины состояний. Но эту часть долго почти никто не замечал. Два раза мне даже говорили, что там ничего нет про машины состояний, и я сам перечитывал статью, чтобы убедиться, что не выдумываю. Думаю, в ней людям понравился новый способ взглянуть на распределённые системы. Для меня он казался очевидным – но так, видимо, не для всех. А вскоре после публикации мне сказали, что люди делятся на две группы: одни считают статью очевидной, другие – гениальной. Я не спорил ни с теми, ни с другими. Всё очевидно – после того как кто-то объяснит Вам это».

Кстати, критерий «неочевидность» (non‑obviousness) есть в американском патентном праве. Это самостоятельный критерий, который отличается от критерия «новизна». Понятие спорное: до прочтения заявки предложение автора обычно не кажется эксперту очевидным, а после её прочтения оно часто представляется ему очевидным, вследствие чего по этому критерию заявка отклоняется.

В работе Lamport L. The implementation of reliable distributed multiprocess systems // Computer Networks. 1978. № 2, pp. 95-114 описан метод реализации любой системы с помощью сети процессов таким образом, чтобы она продолжала функционировать должным образом, несмотря на сбои или неисправности отдельных процессов и коммуникационных дуг. При этом «неисправность» означает неправильное выполнение чего-либо, а «сбой» означает бездействие. Система определяется в терминах последовательной «пользовательской машины», и дано точное условие корректности для реализации этой машины. Приведён алгоритм её реализации в отсутствии неисправностей, а также строгое доказательство её корректности для сети из трёх процессов с идеальными часами. Описано обобщение на произвольную сеть процессов с неидеальными часами. Кратко показано, как можно справиться с неисправностями, добавив избыточную проверку к реализации и включив механизмы обнаружения и исправления ошибок в пользовательскую машину. В статье вместо термина «State Machine» (конечный автомат) использован термин «User Machine» (пользовательская машина).

Лэмпорта спросили: «Как Вы представляли себе будущее в 1978 году, когда писали эту статью, и каким оно оказалось?» Он ответил: «У меня не было дара предвидения. Я занимался распределёнными системами не потому, что думал, будто они станут важными, а просто потому, что само понятие «распределённость» казалось мне фундаментальным и интересным. Всё важное, что я делал, рождалось именно из интереса к базовым идеям.

Как однажды сказал Эдсгер Дейкстра (Лэмпорт в 2000 году стал первым лауреатом премии его имени, учрежденной при жизни классика, а потом становился им ещё дважды), у меня, кажется, есть дар абстракции – способность видеть суть, не отвлекаясь на детали. Для меня часто очевидно то, что, кажется, очевидным не для всех. Я думаю, что это происходит из-за моей математической подготовки: я всегда стремился понимать вещи, начиная с первичных принципов – выводить их из аксиом. И ещё. Большинство исследователей рассматривали проблемы параллелизма как математические, а я – как физические. Например, задача взаимного исключения для меня выглядела как физическая: нужно просто не дать двум агентам делать что-то одновременно. Такой взгляд помог мне предложить первое по-настоящему независимое решение задачи взаимного исключения».

В название статей по этой тематике понятие State Machine (Конечный автомат) попало лишь в 1990 году, в составе более сложного понятия State Machine Approach (Автоматный подход): Schneider F. Implementing Fault-Tolerant Services Using the: A Tutorial // ACM Computing Surveys. 1990. Vol. 22. No. 4, pp. 299-319. Подход с использованием конечных автоматов – это общий метод реализации отказоустойчивых сервисов в распределенных системах. В данной статье рассматривается этот подход и описываются протоколы для двух различных моделей отказов – византийской и остановки при сбое. Также обсуждаются методы реконфигурации системы для удаления неисправных компонентов и интеграции отремонтированных компонентов.

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

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

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

Протокол, предназначенный для решения задачи достижения консенсуса в сети ненадёжных или подверженных сбоям процессоров, был назван Лэмпортом греческим словом Paxos. Этот протокол гарантирует корректную обработку во всех случаях функционирования распределённых сетей. Протокол Paxos был впервые представлен в 1989 году и получил своё название в честь вымышленной системы законодательного консенсуса, действовавшей на греческом острове Paxos (Паксос), где, как писал Лампорт, парламент должен был функционировать «даже несмотря на то, что законодатели постоянно входили и выходили из зала заседаний». Вот видео на эту тему: Lamport on the origins of Paxos.

Статью по этой важнейшей для индустрии теме, написанную в 1989 году, из-за её стиля, непривычного для учёных в области computer science, удалось опубликовать только в 1998 году: Lamport L. The Part-Time Parliament // ACM Transactions on Computer Systems. Vol. 16. 1998. Issue 2, pp. 133-169. В ней говорится, что недавние археологические открытия на острове Paxos показали, что там парламент функционировал, несмотря на склонность его заседателей к вечным перемещениям. Законодатели поддерживали согласованные копии парламентских записей, несмотря на их частые отлучки из зала заседаний и забывчивость посыльных. Протокол парламента Paxos предлагает новый способ реализации распределённых систем на основе конечных автоматов.

Интересно, что на второй «School on the Practice and Theory of Distributed Computing (SPDC)», проходившей в июле 2019 года в Санкт-Петербурге, с двухчастной лекцией на эту тему выступал Лэмпорт: The Paxos algorithm or how to win a Turing Award. Part 1 и The Paxos algorithm or how to win a Turing Award. Part 2.

При этом отмечу, что первую такую школу, которая, правда, называлась несколько иначе «School on Practice and Theory of Concurrent Computing (SPTCC)» в июле 2017 года провела кафедра «Компьютерные технологии» Университета ИТМО совместно с компаниями Telecom Paris Tech и Devexperts (с. 47).

За статьи по теории распределённых систем Лэмпорт получил премию Дейкстры (2000, 2005, 2014), премию IEEE имени Эмануэля Пиора (2004) – за вклад в развитие теории и практики параллельного программирования и отказоустойчивых вычислений, медаль IEEE имени Джона фон Неймана (2008) – за фундаментальный вклад в теорию распределённых и параллельных вычислений, а также премию Тьюринга (2013) – за фундаментальный вклад в теорию распределённых систем.

Интервью с Лэмпортом после получения премии Тьюринга приведено здесь: A Conversation with Turing Award Winner Leslie Lamport.

Отличное пособие по этой тематике написал выпускник кафедры «Компьютерные технологии» ИТМО: Косяков М.С. Введение в распределённые вычисления. СПб: НИУ ИТМО, 2014, 155 с. В нём излагаются основные понятия и концепции из области распределённых вычислений, для модели асинхронных распределённых систем приводятся методы и алгоритмы решения наиболее важных задач. Особое внимание уделяется механизму логических часов, позволяющему значительно упростить разработку алгоритмов для распределённых систем. Рассматриваются основные распределённые алгоритмы взаимного исключения. Изучение этих алгоритмов позволяет раскрыть такие важные вопросы, как обеспечение свойств безопасности и живучести распределённых алгоритмов. Материал пособия сопровождается многочисленными примерами, демонстрирующими применение изучаемых методов и алгоритмов для решения реальных задач.

5. В 1980-х годах письменный обмен сложными идеями был технологическим кошмаром. Учёные тратили бесчисленные часы, пытаясь правильно напечатать математические формулы на пишущей машинке, используя корректирующую жидкость и крошечные, нарисованные от руки символы. Текстовые процессоры при использовании для этой цели превращали элегантные уравнения в мешанину смещённых символов. Документ мог выглядеть идеально на одном компьютере, и мог превратиться в искажённую мешанину на другом.

Первым, кто взялся за решение этой проблемы, был Дональд Кнут. В 1978 году он создал мощный наборный движок под названием TeX. Этот движок мог создавать красивые профессиональные документы с идеально отображаемыми формулами, но у него была серьёзная проблема – он был невероятно сложен в использовании, так как применяемый в нём язык TeX был низкоуровневым. Мощь в движке была, но она была практически недоступна пользователям – математикам, физикам и инженерам. Язык науки оставался запертым за стеной сложности.

Именно здесь Лэмпорт увидел возможность не просто решить техническую проблему, но и реализовать свою идею, состоящую в том, что «ясность изложения – это моральный долг пишущего и говорящего, а быть неясным означает быть нечестным с собой и с миром». Он решил обеспечить доступ пользователей к мощному движку Кнута. Результат – выпущенный в 1984 году набор макросов, который он назвал LaTeX (Why LaTeX?). Это удобный для пользователя слой, который располагался поверх TeX, скрывая его сложность, одновременно раскрывая его мощь.

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

Ключевой принцип созданного: «содержание отдельно, оформление отдельно», что может описано так: «То, что Вы видите, то и имеете в виду». Этому принципу соответствует аббревиатура WYSIWYM (What You See Is What You Mean). Этот принцип отличается от более распространенного: «То, что Вы видите, то и получите» с аббревиатурой WYSIWYG (What You See Is What You Get). Она произносится как «визивиг».

Разработка Лэмпорта позволяет пользователям сосредоточиться на смысле содержимого и его структуре, оставляя системе детали представления. Документ от LaTeX – это обычный текстовый файл, написанный в любом редакторе, с расширением .tex, в котором текст перемежается командами разметки. Файл компилируется специальной программой в формат PDF. После этого автор получает продукт, пригодный для типографии.

Вот его книга по этой теме:  Lamport L. LaTeX: A Document Preparation System Addison-Wesley Addison-Wesley Publishing Company, 1986, 242 p., а вот популярная статья с таким названием: Лесли Лэмпорт – человек, который придумал LaTeX.

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

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

6. Ещё одно направление исследований Лэмпорта связано с верификацией. Вот как Лэмпорт пришёл к исследованиям в этой области: «Я компьютерный учёный. Этого рода деятельности не существовало, когда я начинал заниматься компьютерными науками, и мне понадобилось некоторое время, чтобы понять, что я им являюсь. Мои отношения с компьютерами начались как у программиста, и мне как‑то не приходило в голову, что я занимаюсь чем‑то научным, до тех пор, пока я не опубликовал достаточно статей и до меня, наконец, не дошло это понимание.​ Моё образование было математическим, поэтому для меня было естественно думать о компьютерах как думает математик.

Когда Вы пишете алгоритм, Вам нужно иметь доказательство того, что он корректен. Алгоритм без доказательства – это гипотеза, а не теорема. А если Вы что‑то доказываете, значит, Вы занимаетесь математикой. Компьютерные учёные обычно мыслят в терминах языков программирования. Одним из озарений в моей карьере стало осознание того, что я, как компьютерный учёный, пишу не программы, а разрабатываю алгоритмы.​ И я понял, что если я не пишу программу, то мне не следует использовать язык программирования.

Люди путают программирование с кодированием. Кодирование по отношению к программированию – это то же самое, что набор текста по отношению к письму.​ Письмо – это деятельность, требующая умственных усилий, так как Вы думаете о том, что хотите написать. Слова имеют определённое значение, но они вторичны по отношению к идеям.​ Точно так же программы строятся на идеях: им нужно что‑то делать, и то, что они должны делать, – это как то, что письмо должно передавать. Если людей пытаются учить программированию, обучая их кодировать, это всё равно что учить письму, обучая только тому, как печатать текст, – в этом мало смысла».

О разнице между программированием и кодированием Лэмпорт рассказывает здесь: What's the difference between programming and coding.

Лучший способ, который Лэмпорт предлагает для обучения программированию (в отличие от кодирования) – это думать в математических терминах о том, что программа должна делать, но это весьма трудно осуществимо, так как математическое образование обычно довольно ужасно, и поэтому большинство людей в итоге боятся математики, включая опытных программистов. Он разработал язык под названием TLA+ для записи идей, лежащих в основе программы, который должен использоваться до того, как Вы начнете писать код. Инженерам довольно тяжело к этому привыкнуть, но, когда они это делают, у них развивается способность мыслить математически.

Лэмпорт считает, что хотя программирование родилось в связи с математикой, но с тех пор значительно отдалилось от неё. Большинство программистов не владеют той математикой, которая нужна для работы с TLA+. Очень немногие программисты (и в том числе очень немногие преподаватели программирования) понимают основные концепции TLA+ и то, как они применяются на практике. Эти программисты, похоже, думают, как фон Нейман :-): «Всё что им нужно – только код». Идея о том, что есть некий более высокий уровень абстракции, чем код, на котором можно уметь точно мыслить, и что математика на самом деле позволяет точно мыслить об этом, им совершенно чужда. Потому что они никогда этому не учились.

В 1970-е годы, когда люди рассуждали о программах, они доказывали свойства самой программы, заявленные в терминах языков программирования. Затем они поняли, что главное требование к программе – обеспечить её правильное поведение.

В начале восьмидесятых годов Лэмпорт понял, что одним из практических методов написания спецификаций для параллельных систем является их представление в виде абстрактных алгоритмов. При этом он создал «язык спецификаций». Спецификация похожа на чертеж для программы – она описывает, как ПО должно вести себя на высоком уровне. Такой язык использует точный язык математики, чтобы предотвратить ошибки и избежать недостатков дизайна.

Этот язык предназначен для записи требований к компьютерным программам. Требования к программам на этом языке называют «спецификациями». Они могут быть проверены компьютером. При этом прежде, чем пишется или генерируется код, на языке спецификаций описывается логика программы вместе с ограничениями, которым она должна соответствовать (например, если реализуется поведение банкомата, ограничением может быть то, что никогда нельзя дважды снять одни и те же деньги со своего счёта). Затем инструментальное средство для поддержки TLA+ проверяет, что логика анализируемой программы действительно удовлетворяет этим ограничениям, а если это не происходит, то средство указывает, как эти ограничения нарушены.

На TLA+ Лэмпорт смог выразить алгоритмы математически строго. Для этого не надо писать их на языке программирования, а можно написать их в терминах математики. Вот видео на эту тему: The Man Who Revolutionized Computer Science with Math.

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

До того, как появился метод, названный «Проверка модели» (Model checking), единственным способом убедиться, что алгоритм работает правильно, – была необходимость написать доказательство. Язык Coq был разработан для того, чтобы формализовать рассуждения, которыми пользуются математики. Именно его использовал Жорж Гонтье, чтобы доказать решение проблемы четырёх красок.

Последовательные программы можно описать как функции входных данных, а параллельные системы обычно описываются в терминах их поведения – того, что они делают в процессе выполнения.  В 1977 году Амир Пнуэли предложил использовать временную логику (Temporal Logic) для описания такого поведения (Pnueli A. The temporal logic of programs / In IEEE Proceedings of the 18th Annual Symposium on the Foundations of Computer Science. 1977, pp. 46-57). В 1996 году Пнуэли за это получил премию Тьюринга.

Эта работа стала основой книги: Manna Z., Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. NY.: Springer-Verlag. 1992, 441 pр.

Лэмпорт в своих работах рассматривает другую разновидность временной логики: Temporal Logic of Actions (TLA) (Временная логика действий). Первоначально TLA задумывалась как логический каркас, а не как «язык спецификаций».

Lamport L. The Temporal Logic of Actions // ACM Transactions on Programming Languages and Systems, Vol. 16. 1994. № 3, pp. 1-52. TLA – это логика для описания и анализа параллельных систем. Предложено трактовать предикаты как действия (отношения между парами состояний) и объединить их со стандартной темпоральной логикой, чтобы в одной и той же формальной системе описывать системы и их свойства, поэтому утверждение о том, что система соответствует своей спецификации, и утверждение о том, что одна система реализует другую, выражаются посредством логической импликации.

После этого Лэмпорт спроектировал на основе TLA полноценный язык спецификаций TLA+, который описывал математическое ядро системы (множества, функции, логику, темпоральные операторы). Появившийся в этом обозначении плюс означает, что к Временной логике действий добавились данные.

TLA+ создавался не для математиков, а для программистов и инженеров, которые хотят доказывать свойства систем. После примерно 15 лет работы над доказательствами для параллельных алгоритмов, Лэмпорт понял, что именно нужно делать, чтобы доказать их корректность. TLA стала логикой, которая позволила сделать эти доказательства полностью формальными, а TLA+ – это полноценный язык, основанный на ней.

В 1999 году язык спецификаций TLA+ был описан в статье Lamport L. Specifying Concurrent Systems with TLA+» / Appeared in Calculational System Design. IOS Press, Amsterdam. 1999, pp. 183-247.

В этом же году было создано соответствующее инструментальное средство – Temporal Logic Checker (TLC) для TLA+, которое сразу применили к реальным задачам (Yu Y., Manolios P., Lamport L. Model checking TLA+ specifications / Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science. V. 1703. 1999, pp. 54-66.

После появления этого средства стало возможным утверждать, что проверка модели в TLA+ – это применение Мodel checking к спецификациям на языке TLA+. При этом спецификация фиксирует поведение и требования системы на высоком уровне, без деталей реализации. Модель, в свою очередь, строится на основе спецификации как абстрактное или исполняемое отображение этих требований, позволяющее верифицировать соответствие.

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

В 2002 году появилась книга по этой тематике: Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. 2002. 382 с. Её цель – научить писать спецификации компьютерных систем, используя язык TLA+. Книга довольно большая, и поэтому большинство прочитает только первую её часть, состоящую из 83 страниц. Она содержит всё, что инженерам, создающим ответственные системы, необходимо знать о написании спецификаций.

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

Ещё несколько слов об этой книге. «В ней показано, как писать недвусмысленные спецификации сложных компьютерных систем. Её первая часть представляет собой введение, объясняющее, как с математической точностью описывать поведенческие свойства системы. Акцент делается на свойствах безопасности. Вторая часть охватывает более сложные темы, такие как жизнеспособность, свойства реального времени и т. д. Последние две части книги представляют полное справочное руководство по языку и инструментам TLA+. Этот язык разработан автором для написания простых и элегантных спецификаций поведения систем и протоколов, а также для проверки правильности проекта. Язык доказал свою ценность в понимании и построении параллельных и распределённых систем. Инструменты для синтаксического анализа TLA+ и проверки моделей доступны бесплатно в Интернете».

В 2012 году при участии Лэмпорта был разработан TLA⁺ Proofs  (TLAP) (https://lamport.azurewebsites.net/pubs/tlaps.pdf). Для тех же целей часто используется аббревиатура TLAPS, где последняя буква соответствует слову System.

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

Концептуально TLC не отличается от других верификаторов типа SPIN и NuSMV, и, по сути, делает то же самое – перебирает состояния и проверяет выполнение свойств.

Прекрасное введение в верификацию программ на основе метода Model Checking  с использованием временных логик, указанных ниже, приведено по адресу https://is.ifmo.ru/present/2012/20120218_model_che%D1%81king_karpov_lecture01.pdf, а  применение верификатора SPIN, реализующего этот метод, проиллюстрировано здесь: https://is.ifmo.ru/present/2012/20120218_model_checking_karpov_lecture02.pdf.

Экосистема TLA+/TLC продолжает развиваться. Ее состояние на май 2025 года описано здесь: https://ahelwer.ca/post/2025-05-15-tla-dev-status/.

7. В 2019 году была опубликована книга Concurrency: the Works of Leslie Lamport.  Association for Computing Machinery. NY. 2019, 366 pp. Она описывает деятельность Лесли Лэмпорта в области параллельных вычислений, охватывающую четыре с половиной десятилетия развития индустрии – от появления первых персональных компьютеров до эпохи, когда параллельные и распределённые многопроцессорные системы стали повсеместными.

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

Первая часть книги включает технические главы и биографию. Эти главы представляют ретроспективный взгляд на оригинальные идеи Лэмпорта, изложенный ведущими специалистами в этой области, и демонстрируют долговременное влияние этих идей. Они охватывают ключевые понятия, введённые Лэмпортом: алгоритм «пекарни», атомарные общие регистры и последовательную согласованность, причинность и логическое время, византийское соглашение; репликацию машины состояний и протокол Paxos, временную логику действий.

Профессиональная биография повествует о карьере Лэмпорта, раскрывает контекст, в котором возникали и развивались его идеи, и обсуждает LaTeX – возможно, самый влиятельный вклад Лэмпорта за пределами области параллелизма. Эта глава даёт слово как самому Лэмпорту, так и его коллегам, благодаря которым его идеи получили всемирное признание.

Вторая часть книги включает самые значимые статьи Лэмпорта.

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

8. В большом интервью «How to Write Software With Mathematical Perfection» Лэмпорт обсуждает вопросы применения математики в программировании (текст этого интервью на русском приведен здесь: https://habr.com/ru/companies/first/articles/670538).

Он сожалеет, что несмотря на все его усилия (например, создание TLA+ Video Course) языки спецификации типа TLA+ недостаточно широко используются в индустрии. Это, во-первых, связано с тем, что программисты, а также многие (если не большинство) компьютерных учёных, боятся математики, а во-вторых, все проекты делаются в спешке. По этой причине, так как TLA+ требует значительных усилий на начальном этапе, то фактически добавляется новый этап в процесс разработки, что весьма сложно обеспечить. Все это так, но никого не смущает справедливость старой поговорки: «Никогда нет времени сделать всё правильно, зато всегда находится время переделать».

Программисты обычно склонны тратить больше времени на написание кода, чем на размышления о нём. Идея о необходимости думать и писать спецификацию до того, как начинаешь кодировать, должна «внедряться» в умы студентов в курсах информатики на уровне бакалавриата, но этого не происходит. Это во многом связано с тем, что между теми, кто преподаёт программирование, и теми, кто преподаёт верификацию программ (если такие имеются), обычно нет связи. Преподаватели программирования не знают той верификации, которая им нужна, а преподаватели верификации не понимают, как применять её на практике. Пока этот разрыв не будет преодолён, у TLA+ не появится большое число пользователей.

В работе (https://habr.com/ru/companies/yandex/articles/457810/) различают два подхода: традиционный, названный автором «ремесленным», и инженерный, в рамках которого, как и традиционной инженерии, при создании программ используются различные инструменты, которые предназначены для повышения надёжности программ. Во второй статье этого цикла обсуждается применение TLA+.

Вот что Лэмпорт советует молодым людям, специализирующимся в области компьютерных технологий: «Информатика огромна. Если Вы хотите стать программистом или инженером сложных систем, учите как можно больше математики – не экзотической, а формирующей математическое мышление. Чем сложнее становятся системы, тем важнее абстрактное, точное мышление. И помните: университет – это не курсы по подготовке к работе, а образование. Работать Вы научитесь на работе, а тут нужно научиться думать».

9. Лэмпорт считает, что по мере развития карьеры он стал всё больше ценить индустрию как источник новых задач. Именно оттуда приходило большинство интересных для него задач. При этом он в некотором смысле был согласен с Огюстом Ренуаром, который, когда его спросили, почему он пишет картины ​на пленэре, а не в мастерской, ответил: «Если бы я писал в студии и хотел нарисовать лист, я смог бы придумать лишь с полдюжины разных видов листьев, которые мог изобразить. А когда я пишу на открытом воздухе, вокруг есть миллионы различных листьев, которые я могу взять в качестве натуры». «В индустрии несчётное число задач, они ждут, когда их решат», – говорит Лэмпорт.​

В 2003 году была опубликована статья Batson В., Lamport L. High-Level Specifications: Lessons from Industry, в которой рассказано о том, как Batson использовал предложенный Лэмпортом подход в корпорации Intel. Он считает, что TLA+ представляет собой единственную эффективную методологию, которую он видел для визуализации и количественной оценки алгоритмической сложности способом, который имеет смысл для инженеров.

А вот «свежая» статья моих знакомых на эту тему: Нейзов M.В., Кузьмин Е.В. Применение TLA+/TLC для моделирования и верификации криптографических протоколов // Моделирование и анализ информационных систем. 2024. Т. 31, № 4, c. 446–473. Распространённым формальным методом верификации криптографических протоколов является метод проверки модели. В работе для этой цели используется инструментальное средство TLA+/TLC. На языке спецификации TLA+ задаётся модель протокола, а также требуемые свойства безопасности в форме инвариантов. Модель протокола описывает его поведение в виде системы переходов, содержащей все возможные состояния модели протокола и переходы между ними. Для проведения автоматической проверки соответствия модели требуемым свойствам используется верификатор TLC.

10. Большая часть кода, который пишут программисты по всему миру, не требует предельно точного описания поведения, но есть области, где это критически важно. Для приложений, где важна корректность, требуется высокая строгость. И здесь без методов проектирования программ и инструментов типа TLA+ не обойтись. Об этом моя статья «Автоматное программирование, или Капля камень точит», в которой обсуждается и комментируется текст, название которого по-русски звучит так: «Небольшая группа программистов хочет изменить то, как мы кодируем, прежде чем произойдет катастрофа». Там, в частности, есть такая фраза: «Программисты часто не конца понимают проблему, которую пытаются решить, так как они слишком заняты тем, чтобы заставить свой код работать».

11. Теперь я кратко расскажу мой взгляд на применение в программировании конечных автоматах, названных выше «State Machine». Считается, что «предложенную Лэмпортом идею использования автоматного подхода в распределённых вычислениях можно назвать критически важной разработкой для функционирования современных компьютерных сетей. На основе концепций Лэмпорта в начале 90-х было разработано семейство протоколов для выполнения распределенных транзакций.

В статье «Алгоритм Паксос» сказано, что  протоколы решения задачи консенсуса, разработанные Лэмпортом, основаны на автоматном подходе, для объяснения которого в этой статье приводится ссылка на другую статью в «Википедии»: «Автоматное программирование» 

В ней, в частности, сказано, что «Автоматное программирование – это парадигма программирования, при использовании которой программа или ее фрагмент осмысливается как модель какого-либо формального автомата. Известно также, что «парадигма автоматного программирования базируется на представлении сущностей со сложным поведением в виде автоматизированных объектов управления, каждый из которых это объект управления и автомат». При этом о программе, как в автоматическом управлении, предлагается думать, как о системе автоматизированных объектов управления».

Второе определение парадигмы автоматного программирования принадлежит мне, и я его неоднократно публиковал (например, здесь: Шалыто А.А. Парадигма автоматного программирования // Научно-технический вестник СПбГУ ИТМО. 2008. № 8 (53). Автоматное программирование, с. 3-24.). Оно же приведено и в указанной ниже книге с Надеждой Поликарповой «Автоматное программирование».

Указанный термин на русском (Автоматное программирование) и на английском (Automata-based programming) языках, как и указанная выше парадигма программирования (Парадигма автоматного программирования), в научный лексикон введены мной.

Расскажу более подробно как появился этот термин на русском языке: «Термин «Автоматное программирование», чтобы не говорили недоброжелатели о том, что он существовал «всегда», родился в результате моей беседы с Д.А. Поспеловым на конференции по мультиагентным системам, проходившей в 1997 году в поселке Ольгино под Санкт-Петербургом. Эта история описана в книге, посвященной 20-летию кафедры «Компьютерные технологии» Университета ИТМО.

Приведу некоторые детали этой встречи. После моего рассказа о том, как я предлагаю программировать, по крайней мере, системы логического управления, Дмитрий Александрович сказал: «Очень здоровый подход – крепко стоит на земле. Назови его автоматным программированием. Смотришь – привьется...» Вот я и назвал! 

Вряд ли кто-то в то время в стране лучше Поспелова понимал, что такое автоматы и как их применять, но изложенная технология программирования его удивила, и он помог мне опубликовать статью: Шалыто А.А. Автоматное проектирование программ. Алгоритмизация и программирование задач логического управления // Известия РАН. Теория и системы управления. 2000. № 6, с. 63-81. В этом журнале Дмитрий Александрович в то время был заместителем главного редактора. Вот что написано в аннотации к этой статье: «Описываемая технология может быть названа автоматной технологией, а соответствующая область программирования – автоматным программированием».

На самом деле я этот термин ввел на два года раньше – в книге Шалыто А.А. Switch-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998. 628 с., в которой на странице 14 написано: «Введены понятия «автоматное программирование» и «автоматное проектирование программ». Эта книга была опубликована при поддержке Российского фонда фундаментальных исследований, в экспертный совет которого входил Дмитрий Александрович.

Несколько слов по поводу выбора названия для чего-либо. С одной стороны известно, что «как корабль назовёшь, так он и поплывёт», а с другой – «дать чему-либо имя – это акт творения. Это даёт ему силу, даёт идентичность» (из видео о Б. Мандельброте, в котором, частности, рассказано, как он придумал термин «Фрактал»).

Как отмечено выше, Лэмпорт считает, что предлагаемые им методы тяжело внедряются из-за того, что программисты плохо знают математику, однако он сам не делает даже шага навстречу программистам и инженерам.

Я же такой шаг сделал. В качестве языка спецификации поведения программы я, в отличие от Лэмпорта, предложил использовать системы взаимосвязанных (в том, числе вложенных) графов переходов, которые при применении, например, инструментального средства State Flow (Янкин Ю.Ю., Шалыто А.А. Автоматное программирование ПЛИС в задачах управления электроприводом // Информационно-управляющие системы. 2011. № 1, с. 50-56, могут быть также и языком программирования сверхвысокого уровня. Кроме того, графы переходов очень наглядны, что немаловажно для практики, так как Алиса из страны чудес говорила: «Девочки любят картинки». Я думаю, что их любят не только девочки, но и те ученые и инженеры, которые не дотягивают до того математического уровня, который нужен Лэмпорту.

Ещё один шаг в этом направлении мы сделали непосредственно на «территории» Лэмпорта: Сатюков Р.В., Синев И.А., Шалыто А.А. Реализация алгоритма Лэмпорта на основе автоматного подхода.  СПб.: ИТМО 2006. 42 с. В работе продемонстрирована возможность применения автоматного программирования и инструмента Unimod при реализации алгоритма Лампорта, обеспечивающего контроль доступа параллельных процессов к критической секции. Unimod позволяет интерпретировать и компилировать автоматные программы, поведение которых наглядно задается графами переходов. При этом структура программы в целом определяется схемой связей автоматов с поставщиками событий и объектами управления. При этом отмечу, что в пионерской статье Лэмпорта по этой теме, указанной выше, автоматный подход не применялся. Несколько слов об одном из авторов этой работы – Романе Сатюкове. Он в 2007 г. входил в команду ИТМО, которая заняла третье место на командном студенческом чемпионате мира ACM ICPC (с. 112. 

В тексте нашей работы приведен псевдокод, реализующий этот алгоритм традиционным путем, который взят из книги Garg V. Concurrent and Distributed Computing in Java. Wiley-IEEE Press. 2004, 336 p. Однако, даже по мнению моих соавторов-программистов, он труден для понимания. Поэтому в нашей работе для реализации этого алгоритма применяются автоматы, но не в виде математических абстракций, а в наглядной форме – в виде графов переходов.

При этом рассматриваются два метода построения графов переходов: эвристический и формальный переход от схемы алгоритма, построенной по указанному псевдокоду. Этот переход был выполнен с помощью метода, описанного в статье Шалыто А.А., Туккель Н.И. Преобразование итеративных алгоритмов в автоматные // Программирование. 2002. № 5, с. 12-26. Выполнена также декомпозиция и оптимизация графа переходов, полученного вторым методом.

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

Для обеспечения правильности работы автоматов мы, как и Лэмпорт, используем верификацию: Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПб: Наука, 2011. 244 с. При этом, правда, используем не TLA+, а Liner Temporal Logic (LTL) и Computational Tree Logic (CTL).

Основное отличие нашего подхода к верификации от классического Мodel checking состоит в том, что они по программе строят модель, а мы по модели строим программу, поэтому нашу книгу я бы сегодня назвал «Верификация автоматных моделей» или «Верификация автоматных спецификаций». Предлагаемый нами подход является более естественным, чем классический, так как у нас вся верификация проводится с использованием автоматов: конечные автоматы, автоматы Крипке и автоматы Бюхи, в то время как них в начале верификации конечных автоматов нет.

На юбилее Бертрана Мейера в Цюрихе в 2010 году, я хотел рассказать об этом одному из лауреатов премии Тьюринга 2007 года за Мodel checking – Джозефу Сифакису, но по техническим причинам это сделать не удалось, и он поэтому, видимо, до сих пор не знает, как проводить верификацию правильно :-).  

Для повышения качества спецификаций я также предлагаю проводить и их валидацию: Шалыто А.А. Валидация автоматных спецификаций // Научно-технический вестник информационных технологий, механики и оптики. 2023. № 2, с. 436-438.

В качестве одного из методов валидации автором совместно с В.Ф. Назаровым разработан метод перемножения автоматов, в том числе вложенных, который позволяет по заданной системе взаимосвязанных графов переходов строить граф переходов одного автомата, поведение которого эквивалентно поведению заданной системы. Перемножение проводится последовательно и попарно. При каждом перемножении автоматов могут обнаруживаться некорректности (например, дедлоки) в валидируемой системе. Такой метод особенно актуален при использовании промптов при программировании с помощью больших языковых моделей. Этот метод может быть использован и для других классов программ после их преобразования в автоматные с помощью методов, предложенных в следующих работах:

1. Туккель Н.И., Шалыто А.А. Реализация вычислительных алгоритмов на основе автоматного подхода //Телекоммуникации и информатизация образования. 2001 № 6, с. 35-53. http://is.ifmo.ru/progeny/_2011_01_03_shalyto-tukkel.pdf.

2. Шалыто   А.А.,   Туккель   Н.И. Преобразование итеративных алгоритмов в автоматные // Программирование. 2002 № 5, c. 12-26. http://is.ifmo.ru/works/iter/.

3. Туккель   Н.И.,   Шалыто   А.А.,   Шамгунов   Н.Н. Реализация рекурсивных алгоритмов на основе автоматного подхода // Телекоммуникации и информатизация образования. 2002 № 5, с. 72-99. http://is.ifmo.ru/works/recurse/.

Хочу также отметить, что у Лэмпорта и у меня одинаковые взгляды на качество написания научно-технических текстов.

И в заключение. Вот, как оценивает свои достижения Лэмпорт: «Я считал себя неудачником, потому что не создал теорию параллелизма, а потом понял, что просто проложил путь, по которому пошли другие».

Об авторе: Анатолий Шалыто - докт. техн. наук, профессор, Университет ИТМО
Помещена в музей с разрешения автора. В статье сохранено авторское оформление текста. 6 апреля 2026