Семинар НУЛ ПОИС "Using TLA+ as a Tool for Building Transactional Memory Models from Specialized Frameworks" ("Использование TLA+ в качестве инструмента для построения моделей транзакционной памяти на основе специализированных фреймворков")

Тема доклада: "Using TLA+ as a Tool for Building Transactional Memory Models from Specialized Frameworks" ("Использование TLA+ в качестве инструмента для построения моделей транзакционной памяти на основе специализированных фреймворков")

Дата проведения: 20 мая 2026, 17:00
Аннотация: Most modern concurrent algorithms are either lock-based or complex, hard-to-understand lock-free structures, while Software Transactional Memory (STM) remains underutilized. STM facilitates the non-blocking implementation of complex algorithms through transaction mechanisms. This paper adapts the Tsay-Lee framework to transactional memory models. Originally designed to grant lock-free properties to Binary Search Trees, this framework is used here to demonstrate how formal specifications can prove that universal algorithms maintain correctness when constructed from specialized components. The specifications are developed using the TLA+ language and the TLC model checker. The resulting specialization demonstrates that lock-based and non-blocking algorithms share more structural similarities than their source code suggests. This insight supports the creation of universal constructions for achieving lock-free properties. This work is intended for researchers seeking new universal paths to non-blocking algorithm implementations.

(Аннотация: Большинство современных алгоритмов параллельного выполнения либо основаны на блокировках, либо представляют собой сложные и трудные для понимания безблокировочные структуры, тогда как программная транзакционная память (STM) остаётся недостаточно используемой. STM упрощает безблокировочную реализацию сложных алгоритмов за счёт использования транзакционных механизмов. В данной работе фреймворк Tsay-Lee адаптируется для моделей транзакционной памяти. Изначально разработанный для обеспечения безблокировочности бинарных деревьев поиска, данный подход в настоящей работе используется для демонстрации того, как формальные спецификации позволяют доказать сохранение корректности универсальных алгоритмов при их построении из специализированных компонентов. Спецификации создаются с использованием языка TLA+ и верификатора моделей TLC. Результаты специализации демонстрируют, что блокировочные и безблокировочные алгоритмы имеют больше структурного сходства, чем это может показаться при анализе их исходного кода. Данное наблюдение обосновывает создание универсальных конструкций для обеспечения безблокировочности. Работа адресована исследователям, разрабатывающим новые универсальные подходы к реализации неблокирующих алгоритмов.)

Докладчик: Студент 1-го курса ПИ Еремей Первунецких