Moverness for Locks and Transactions

Granville  Barnett; Shengchao Qin

doi:10.1109/TASE.2012.29

Moverness for Locks and Transactions

Granville Barnett , Shengchao Qin

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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	https://doi.org/10.1109/TASE.2012.29
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

Access to Document

10.1109/TASE.2012.29

Cite this

@inproceedings{ff3f4bad6ab8440ab5da483df617af15,

title = "Moverness for Locks and Transactions",

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.",

author = "Granville Barnett and Shengchao Qin",

year = "2012",

doi = "10.1109/TASE.2012.29",

language = "English",

isbn = "9781467323536",

booktitle = "2012 Sixth International Symposium on Theoretical Aspects of Software Engineering",

publisher = "IEEE",

note = "6th International Symposium on Theoretical Aspects of Software Engineering, TASE 2012 ; Conference date: 04-07-2012 Through 06-07-2012",

}

TY - GEN

T1 - Moverness for Locks and Transactions

AU - Barnett , Granville

AU - Qin, Shengchao

N1 - Conference code: 6

PY - 2012

Y1 - 2012

N2 - 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.

AB - 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.

UR - http://dx.doi.org/10.1109/TASE.2012.29

U2 - 10.1109/TASE.2012.29

DO - 10.1109/TASE.2012.29

M3 - Conference contribution

SN - 9781467323536

BT - 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering

PB - IEEE

T2 - 6th International Symposium on Theoretical Aspects of Software Engineering

Y2 - 4 July 2012 through 6 July 2012

ER -

Moverness for Locks and Transactions

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this