Reasoning about Locks and Transactions in Concurrent Programs

Abstract

The aim of this thesis is to present novel techniques for reasoning about the dynamic and static semantics of concurrent programs that use locks and transactions to isolate accesses to shared memory. We use moverness to characterise the observational semantics of reads issued by locks and transactions under the simpler semantics of free, left, right and both movers. The second contribution is guaranteed transactions which are a safer alternative to locks and the privatisation/publication idioms for specific scenarios. Guaranteed transactions facilitate a simpler pessimistic coordination semantics than locks, but offer most of the conveniences that have made transactions appealing. Finally, we present a static analysis for reasoning about the isolation of a program that uses locks and transactions. If our isolation algorithm determines that all the accesses issued by a program are isolated, then the program is declared data-race-free.