Abstract
Locks are pervasive in multithreaded code. For software transactional memory (STM) to be widely adopted there must be a consensus on a semantics for programs that entail both locks and transactions, particularly for weakly isolated STMs. For instance, in a weakly isolated STM, use of both locks and transactions to access the same data may introduce data races. In response we present a simple and intuitive semantics that guarantees ordered linearisation points for conflicting locks and transactions. Our approach allows us to classify the moverness of locks and transactions, making reasoning about parallel compositions trivial. Under our semantics we show locks to be left movers and transactions right movers, and the serialisability of conflicting locks and transactions.
Original language | English |
---|---|
Title of host publication | 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering |
Publisher | IEEE |
ISBN (Print) | 9781467323536 |
DOIs | |
Publication status | Published - 2012 |
Event | 6th International Symposium on Theoretical Aspects of Software Engineering - Beijing, China Duration: 4 Jul 2012 → 6 Jul 2012 Conference number: 6 |
Conference
Conference | 6th International Symposium on Theoretical Aspects of Software Engineering |
---|---|
Abbreviated title | TASE 2012 |
Country/Territory | China |
City | Beijing |
Period | 4/07/12 → 6/07/12 |