Using TLA+ and the Tsay-Li Framework for Building Transactional Memory Models

Using TLA+ and the Tsay-Li Framework for Building Transactional Memory Models

Pervunetskikh E.D. (NRU HSE, Moscow, Russia)

Abstract

This paper adapts the Tsay-Li framework, designed for non-blocking binary search trees, to software transactional memory (STM) models, which simplify the non-blocking implementation of complex concurrent algorithms. Using TLA+ (language for temporal logic of actions) specifications and verification with the TLC model checker, we demonstrate how formal methods prove the correctness of universal algorithms built from specialized components. This approach addresses the challenge of developing other specialized frameworks by enabling refining rollbacks from the state of the general STM. The results show that lock-based and non-blocking algorithms share more structural similarities than their source code suggests. This insight justifies the creation of universal constructions for achieving lock-free properties.

Keywords

concurrent data structures; temporal logic; formal verification; non-blocking algorithms; binary search trees; transactional memory.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 6, part 2, 2026, pp. 57-66

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

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

For citation

Pervunetskikh E.D. Using TLA+ and the Tsay-Li Framework for Building Transactional Memory Models. Proceedings of the Institute for System Programming, vol. 38, issue 6, part 2, 2026, pp. 57-66 DOI: 10.15514/ISPRAS-2026-38(6)-25.

Full text of the paper in pdf Back to the contents of the volume