Max Home IndustryИсследователь Microsoft Лесли Лэмпорт был назван лауреатом премии ACM A. M. Turing Award 2013 года (она же Нобелевская премия по информатике) за свою работу в области распределенных вычислений.
Премия ACM A. M Turing Award широко считается «Нобелевской премией в области вычислительной техники» и присуждается в размере 250 000 долларов США при финансовой поддержке Intel и Google.
Ежегодный победитель, индивидуальный или команда из двух или трех человек, выбирается из числа тех, кто номинирован комитетом, который в настоящее время возглавляет Адель Голдберг, и включает в себя двух недавних лауреатов премии Тьюринга, Лесли Валиант (2010) и Барбару Лисков (2008) среди своих восьми членов. Номинации закрываются в ноябре, лауреат объявляется в марте следующего года, а награда вручается на ежегодном банкете ACM Awards в июне.
Цитата для Лесли Лэмпорта гласит::
За фундаментальный вклад в теорию и практику распределенных и параллельных систем, в частности за изобретение таких понятий, как причинность и логические часы, безопасность и живучесть, реплицированные машины состояний и последовательная последовательность.
В этом видео нынешние коллеги и прошлые корифеи Microsoft Research объясняют, почему Лэмпорт заслуживает этой награды, и поздравляют его с ее достижением.
Согласно ACM, он удостоен чести
для наложения четкой, четко определенной согласованности на кажущееся хаотичным поведение распределенных вычислительных систем, в которых несколько автономных компьютеров взаимодействуют друг с другом, передавая сообщения. Он разработал важные алгоритмы и разработал формальные протоколы моделирования и верификации, которые улучшают качество реальных распределенных систем. Эти вклады привели к повышению корректности, производительности и надежности компьютерных систем.
Хотя он специально не указан в ACM, алгоритм Пекарни, разработанный Лампортом в 1979 году, является, пожалуй, самым известным и наиболее широко используемым — по крайней мере, в преподавании компьютерных наук. Это отправная точка для этого видео канала 9 2010 года, в котором он рассказывает с Эриком Мейером о математических рассуждениях и распределенных системах.
Обсуждение переходит к часам Лэмпорта, и здесь Лэмпорт объясняет, как на них повлияла концепция Специальной теории относительности Эйнштейна. Позже он охватывает TLA, Временную логику действий,которая является логикой для определения и рассуждения о параллельных и реактивных системах. TLA+, последнее воплощение этого набора инструментов формальной спецификации, с открытым исходным кодом в прошлом году.
Наряду с алгоритмами и инструментами для распределенных систем Lamport разработал решения для обеспечения отказоустойчивости, которые способствуют предотвращению сбоев в компоненте системы, который ведет себя ошибочно при взаимодействии с другими компонентами.
Он также является оригинальным автором LaTeX, системы подготовки документов и языка разметки, который является стандартом де-факто для публикации научных и академических работ.
На веб-сайте Лесли Лэмпорта есть список из 179 ссылок в качестве его «Собрания сочинений» с PDF-файлами большинства из них. Это портал для увлекательного чтения.