Verification of Concurrent Data Structures with TLA

Abstract

Concurrent systems have critical applications such as aviation. Due to their inherent complexity, mechanised verification is well suited for reasoning about the safety and liveness properties of such systems. Temporal logics, such as TLA and LTL, have been used to verify distributed systems and protocols. However, it is not clear whether these logics are good fits for modelling and verifying concurrent data structures. This work describes how Temporal Logic of Actions (TLA) can be adapted to handle concurrent data structures and weak memory models. It also shows how the TLA toolchain, especially the model checker, can aid in cleanly applying the logical machinery to concrete programs. I used litmus tests to validate my encoding of memory models against prior work. These models enabled me to formalize various concurrent data structures, including the Chase-Lev queue. Then, I am able to check the behaviours of these data structures against abstract specification of their operations. In particular, my modelling can successfully find bugs in a faulty implementation of the Chase-Lev queue. The results suggest that TLA is appropriate for modelling concurrent data structures. The formal models I designed and the related modelling techniques can be used by the wider research community in their verification work.