Abstract
This thesis sheds light on key aspects of Persistent Software Transactional Memory.
Persistent memory is a novel memory paradigm that retains its contents even in the event of power loss. It is widely expected to become ubiquitous, and hardware architectures are already providing support for persistent memory programming. However, writing persistent programs is extremely challenging, as it requires the programmer to keep track of which memory writes have become persistent and which have not. This is further complicated in a multi-threaded setting by the intricate interplay between the rules of memory persistency (which determine the order in which writes become persistent) and those of memory consistency (which determine what data can be observed by which threads).
Software Transactional Memory (STM) has emerged as a highly promising solution for concurrency control in multi-threaded environments, allowing programmers to concentrate on algorithm design rather than intricate locking mechanisms.
Recent research efforts focus on integrating durability into transactions. Persistent STMs aim to accomplish more than just thread synchronization; they also endeavor to maintain persistent memory in a consistent state. Implementing such mechanisms can greatly benefit developers, as they would no longer be burdened with the responsibility of persisting coherently memory locations. However, due to their innate complexity, persistent STMs are susceptible to errors, necessitating careful design and thorough testing. In this thesis, we are approaching the problem of persistent STMs correctness from a formal methods perspective.
At the core of this research, two main topics are addressed. The first topic concerns the nature of software transactional memory correctness in the face of persistency. To this end, we present a novel definition of software transactional memory correctness, durable opacity, which adapts opacity to the persistent memory setting.
The second topic concerns the verification of persistent transactional memory algorithms. We aim to investigate how existing verification techniques designed for volatile memory algorithms can be adapted and applied in the context of persistent memory. In our initial work, we attempt to verify a durably opaque version of an STM algorithm, TML [1]. In this first endeavor, we assume a simplified model, Persistent Sequential Consistency (persistent SC), which lays the groundwork for understanding verification challenges unique to persistency. The proposed proof technique constitutes an adaptation to persistency of the verification method demonstrated in [2]. In our second work, we are focusing on developing an Owicki-Gries program logic for reasoning about x86 code that uses low-level operations, such as fences and flushes, for controlling persistency. Our logic is able to accommodate the persistency features and weak behaviors induced by the Px86 model. We exemplify the utility of our logic by verifying a number of persistent x86 litmus tests. In our final work, we adapt our initial STM implementation to the realistic Px86 model and show that it is durably opaque. Our correctness proof is operational and builds on our logic as well as the simulation-based proof technique demonstrated in our first work.
Our entire development has been mechanized in the Isabelle/HOL proof assistant.