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 contributes to the specification, safety criterion, testing and verification of TM algorithms. In particular, it presents techniques to prove the correctness or incorrectness 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.
Decomposition of the correctness condition supports modular and scalable verification. We introduce the markability correctness condition as the conjunction of three intuitive invariants: write-observation, read-preservation and real-time-preservation. We prove the equivalence of markability and opacity correctness conditions.
We identify two pitfalls that lead to violation of opacity: the write-skew and write-exposure anomalies. We present a constraint-based testing technique and an automatic tool called Samand that 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.
We present a sound program logic called synchronization object logic (SOL) that supports reasoning about the execution order and linearization order. It provides inference rules that axiomatize the properties and the interdependence of these orders and also the properties of common synchronization object types. We show that derivation of markability in SOL is a sound syntactic proof technique for opacity. We use SOL to prove the markability and hence opacity of the TL2 algorithm in PVS.