UCLA

Transactional Memory (TM) provides programmers with a high-level and composable concurrency control abstraction. The correct execution of client programs using TM is directly dependent on the correctness of the TM algorithms. In return for the simpler programming model, designing a correct TM algorithm is an art. This dissertation presents techniques to prove the correctness or incorrectness of TM algorithms. In particular, it contributes to the specification, safety criterion, testing and verification of TM algorithms.

We introduce a language for architecture-independent specification of synchronization algorithms. An algorithm specification captures two abstract properties of the algorithm namely the type of the used synchronization objects and the pairs of method calls that should preserve their program order in the relaxed execution.

We introduce the markability correctness condition as the conjunction of intuitive invariants: write-observation and read-preservation. We prove the equivalence of markability and opacity correctness conditions. Decomposition of the correctness condition supports modular and scalable verification.

We identify two pitfalls that lead to violation of opacity: the write-skew and write-exposure anomalies. We present a tool called Samand that automatically finds traces of such bug patterns. Using Samand, we show that the DSTM and McRT algorithms suffer from the write-skew and write-exposure anomalies respectively.

We present a sound program logic called synchronization object logic (SOL) that supports reasoning about the execution order and linearization orders of method calls. It provides inference rules that axiomatize the properties and the interdependence of these orders and also the properties of common synchronization object types. We present the derivation of markability in SOL as a sound syntactic proof technique for opacity. We use SOL to prove the markability and hence opacity of the TL2 algorithm in PVS.