

Durham e-Theses
You are in:

Reasoning about Locks and Transactions in Concurrent Programs

BARNETT, GRANVILLE (2014) Reasoning about Locks and Transactions in Concurrent Programs. Doctoral thesis, Durham University.

PDF - Accepted Version


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.

Item Type:Thesis (Doctoral)
Award:Doctor of Philosophy
Keywords:Concurrency; Software Transactional Memory; Locks; Programming Languages
Thesis Date:2014
Copyright:Copyright of this thesis is held by the author
Deposited On:06 May 2014 11:38

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitter