Использование TLA+ и методологии Цая-Ли для построения моделей транзакционной памяти

Использование TLA+ и методологии Цая-Ли для построения моделей транзакционной памяти

Первунецких Е.Д. (НИУ ВШЭ, Москва, Россия)

Аннотация

В работе адаптирована методология Цая-Ли, предложенная для неблокирующих бинарных деревьев поиска, к моделям программной транзакционной памяти, которая упрощает неблокирующую реализацию сложных конкурентных алгоритмов. На примере спецификаций на языке темпоральной логики действий TLA+ и верификации с помощью инструмента проверки моделей TLC доказывается корректность универсального подхода. Полученные результаты показывают, что блокирующие и неблокирующие алгоритмы имеют больше структурных сходств, чем их исходный код. Этот вывод обосновывает создание универсальных конструкций для достижения неблокируемости.

Ключевые слова

параллельные структуры данных; темпоральная логика; формальная верификация; неблокирующие алгоритмы; двоичные деревья поиска; транзакционная память.

Издание

Труды Института системного программирования РАН, том 38, вып. 6, часть 2, 2026, стр. 57-66.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(6)-25

Для цитирования

Первунецких Е.Д. Использование TLA+ и методологии Цая-Ли для построения моделей транзакционной памяти. Труды Института системного программирования РАН, том 38, вып. 6, часть 2, 2026, стр. 57-66. DOI: 10.15514/ISPRAS-2026-38(6)-25.

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома