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

Лесли Лампорт — американский учёный в области информатики, пионер теории распределённых вычислений и один из создателей языка разметки LaTeX. Наиболее известен разработкой алгоритмов для обеспечения согласованности данных в распределённых системах, в частности алгоритма Лампорта для синхронизации логических часов и алгоритма пекарни для взаимного исключения. Лауреат премии Тьюринга (2013).

Биография

Ранние годы и образование

Лесли Лампорт родился 7 февраля 1941 года в Нью-Йорке, США. В 1960 году окончил Бронксскую школу наук. Получил степень бакалавра математики в Массачусетском технологическом институте (MIT) в 1962 году, степень магистра в области математики и компьютерных наук в Университете Брандейса в 1963 году, а также степень доктора философии (PhD) по математике в Гарвардском университете в 1972 году. Диссертация была посвящена аналитической теории дифференциальных уравнений.

Карьера

После защиты диссертации Лампорт работал в исследовательской лаборатории компании Xerox в Пало-Альто (Xerox PARC), где занимался проблемами распределённых вычислений. В 1970-х и 1980-х годах он внёс основополагающий вклад в теорию параллельных и распределённых систем. В 1985 году перешёл в компанию Digital Equipment Corporation (DEC), где работал в Systems Research Center. В 2001 году стал профессором компьютерных наук в Стэнфордском университете, где преподавал до выхода на пенсию в 2016 году.

Научный вклад

Логические часы и порядок событий

В 1978 году Лампорт опубликовал статью «Time, Clocks, and the Ordering of Events in a Distributed System», которая стала одной из самых цитируемых работ в области распределённых систем. В ней он ввёл понятие логических часов (часов Лампорта) — механизма, позволяющего определить частичный порядок событий в распределённой системе без использования физического времени. Этот подход лёг в основу многих алгоритмов синхронизации и репликации данных.

Алгоритм пекарни

В 1974 году Лампорт предложил алгоритм пекарни (bakery algorithm) — алгоритм взаимного исключения для n процессов, работающих с общей памятью. Название алгоритма связано с аналогией с выдачей номеров в пекарне: каждый процесс получает временный номер, и процесс с наименьшим номером получает доступ к критической секции. Алгоритм гарантирует отсутствие взаимной блокировки и голодания.

Распределённые консенсусы и Paxos

Лампорт является автором семейства протоколов Paxos для достижения консенсуса в распределённых системах. Первая версия протокола была опубликована в 1989 году, но широкую известность получила после публикации статьи «The Part-Time Parliament» (1998). Протокол Paxos используется в системах управления базами данных, облачных платформах и распределённых файловых системах (например, в Google Chubby и Apache ZooKeeper).

Верификация и формальные методы

Лампорт внёс значительный вклад в формальную верификацию параллельных систем. Он разработал язык TLA+ (Temporal Logic of Actions) для спецификации и проверки алгоритмов. TLA+ позволяет описывать поведение распределённых систем и доказывать их корректность. Лампорт также написал книгу «Specifying Systems» (2002), посвящённую TLA+.

LaTeX

В начале 1980-х годов Лампорт начал разрабатывать систему вёрстки LaTeX как набор макросов поверх системы TeX, созданной Дональдом Кнутом. Первая версия LaTeX была выпущена в 1985 году. LaTeX стал стандартом для подготовки научных и технических документов, особенно в математике, физике и информатике. Лампорт написал книгу «LaTeX: A Document Preparation System» (1986), которая долгое время служила основным руководством по системе.

Награды и признание

• Премия Тьюринга (2013) — за фундаментальный вклад в теорию и практику распределённых и параллельных систем, включая логические часы, алгоритмы взаимного исключения и протоколы консенсуса.
• Премия Эдсгера Дейкстры (2000, 2005) — за работы по распределённым алгоритмам.
• Медаль Джона фон Неймана (2004) — от IEEE.
• Член Национальной инженерной академии США (1991) и Американской академии искусств и наук (2011).

Критика

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

Интересные факты

• Лампорт является автором эссе «How to Write a Proof» (1993), в котором излагает методику написания строгих математических доказательств.
• Он известен своей любовью к математическим головоломкам и часто использует их в качестве примеров в своих лекциях.
• Лампорт — один из немногих учёных, получивших премию Тьюринга за работы, которые имеют прямое применение в промышленных системах.

Источники

• Lamport, L. «Time, Clocks, and the Ordering of Events in a Distributed System». Communications of the ACM, 1978.
• Lamport, L. «The Part-Time Parliament». ACM Transactions on Computer Systems, 1998.
• Lamport, L. «LaTeX: A Document Preparation System». Addison-Wesley, 1986.
• Lamport, L. «Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers». Addison-Wesley, 2002.
• Премия Тьюринга 2013 года — ACM A.M. Turing Award.