Конференции USENIX ATC и OSDI – это знаковые мероприятия в области операционных систем, распределённых систем и масштабируемых технологий. В 2025 году оба события прошли параллельно, при этом OSDI впечатлял своей строгостью одного трека и высоким конкурсом из 339 поданных заявок, среди которых было принято всего 16% работ. ATC, в свою очередь, предложил две параллельные дорожки, что позволило охватить более широкий спектр тем и проектов. Технические сессии ATC/OSDI’25 выявили интересные тенденции – от формальных методов верификации протоколов до мультимодальных систем с использованием больших языковых моделей (LLM) и специализированных аппаратных решений для баз данных. Особое внимание приковали доклады, посвящённые применению ИИ в ускорении разработки ПО и автоматизации сложных процессов в распределённых вычислениях.
Одним из самых ярких событий стало выступление Эмери Бёрджера, ученого из Университета Массачусетса и Amazon Scholar. Его доклад был посвящён революции, вызванной интеграцией моделей LLM в инструменты разработчика и развитию экосистемы программных продуктов. Докладчик провел метафору, сравнивая традиционную разработку с динозавром, а LLM – с астероидом, запускающим камбрийский взрыв инноваций в области инструментального обеспечения. Он подробно рассказал о серии своих проектов, реализованных в лаборатории Plasma: Scalene, chatDBG, cwhy, coverup и flowco, представляющих собой новую волну LLM-усиленных инструментов для профилирования, отладки, компиляции, тестирования и анализа данных. Scalene, например, сочетает мощь традиционного профайлера с генеративными моделями, предоставляя не просто статистику, но и объяснения и рекомендации по оптимизации кода, что позволяет обеспечить значительный прирост производительности, вплоть до ускорения в 90 раз.
ChatDBG олицетворяет эволюцию от обычного отладчика к интеллектуальному ассистенту с диалоговым интерфейсом, который понимает причинно-следственные связи, анализирует динамическое состояние программы и помогает пользователю определить корни проблем. Такой подход существенно улучшает показатели успешного поиска ошибок, достигая 75–80% при использовании расширенных запросов. Аналогично, компилятор cwhy предоставляет понятные человеку объяснения ошибок компиляции с приложенными конкретными решениями, позволяя разработчикам быстрее устранять проблемы, даже в сложном синтаксисе C++. Среди представленных докладов наиболее значимым признана работа, отмеченная как лучшая статья OSDI’25 – «Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols». Ее авторы разработали новую методологию формирования инвариантов для автоматической проверки безопасности распределённых протоколов, существенно упрощающую традиционно длительный и сложный процесс формальной верификации.
Основная идея заключается в использовании «инвариантов происхождения», которые связывают переменные состояния с их причинно-следственной цепочкой, позволяя выявлять надежные свойства системы, объясняющие, почему состояние является корректным. Этот подход реализован в расширении для языка Dafny, что позволило проверить широкий спектр протоколов, таких как Paxos и MultiPaxos, с высоким уровнем автоматизации и удобства. Интересным инновационным решением стало представление системы Tigon – распределённой базы данных, разработанной для эксплуатации преимуществ CXL-подов памяти. Вместо традиционной сетевой синхронизации, использующей RPC и сокеты, Tigon применяет атомарные аппаратные операции и кэш-совместимость, что снижает задержки и повышает пропускную способность в пределах одного стойки. Несмотря на ограничения масштабируемости, архитектура демонстрирует впечатляющие показатели производительности на эмуляторах, опережая существующие решения на RDMA и других платформах.
В условиях растущей потребности в глобальных распределённых транзакциях со строгой поддержкой согласованности и низкой задержкой был представлен проект Mako. Он решает проблему медленных межрегиональных согласований, отделяя выполнение транзакций от процесса репликации. Такой спекулятивный механизм с отслеживанием зависимостей с помощью векторных часов позволяет ускорить ответы и обеспечить исправное поведение при откатах, которые, однако, требуют дальнейшего исследования и уточнений в части консенсуса на этапе роллбэков. Методы обеспечения консистентности и капельной свежести данных в кэшах глобального масштаба представлены инновационной системой Skybridge от Meta. Skybridge предлагает добавочный канал репликации, независимый от основного асинхронного, выполненный с помощью эффективных Bloom-фильтров и обеспечивающий стабильно ограниченную задержку обновлений в 2 секунды с точностью в 99.
99998%, значительно улучшая пользовательский опыт без ощутимого увеличения потребления ресурсов. Снижение задержек логирования и повышение производительности критичных для масштабируемых систем журналов транзакций обеспечено в проекте SpecLog и его реализации Belfast. Они вводят концепцию спекулятивной доставки записей с предварительным распределением квот для каждого шарда, что позволяет приложениям начинать обработку данных до окончательного установления глобального порядка, сокращая задержки в 3.5 раза и улучшая концевую латентность на 60%. Такие подходы приближают идею исключения узких мест синхронизации и вывода согласованности из критического пути выполнения.
Весь комплекс новинок и идей, представленных на ATC и OSDI 2025, демонстрирует, что поле распределённых систем находится на стадии интенсивного технологического превращения. Возрастающая роль машинного обучения, официальное признание важности формальных методов, инновации в аппаратной базе и архитектуре приложений образуют новую парадигму, направленную на обеспечение более надёжных, эффективных и масштабируемых систем. Для профессионалов и исследователей эти конференции продолжают оставаться источником перспективных концепций и практических инструментов, которые задают вектор развития индустрии в ближайшие годы. Кроме технического вклада, стоит отметить и организационную сторону мероприятий, которая остается на высоком уровне с открытым доступом к материалам и ожидаемым в скором времени выпуском видеозаписей презентаций. Это открывает широкие возможности для изучения последних достижений и внедрения их идей в собственные проекты.
Подводя итог, ATC и OSDI 2025 года подарили сообществу богатый фонд знаний и свежих взглядов на современные вызовы и решения в области системного программного обеспечения и распределённых вычислений. Интеграция ИИ и формальных методов, новые архитектуры баз данных, инновации в средствах разработки – всё это гарантирует дальнейшее развитие отрасли и формирование новых стандартов качества и производительности.
