TY - GEN
T1 - The push/pull model of transactions
AU - Koskinen, Eric
AU - Parkinson, Matthew
N1 - Publisher Copyright:
© 2015 ACM.
PY - 2015/6/3
Y1 - 2015/6/3
N2 - We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics in which concurrent transactions PUSH their effects into the shared view (or UNPUSH to recall effects) and PULL the effects of potentially uncommitted concurrent transactions into their local view (or UNPULL to detangle). Each operation comes with simple criteria given in terms of commutativity (Lipton's left-movers and right-movers). The benefit of this model is that most of the elaborate reasoning (coinduction, simulation, subtle invariants, etc.) necessary for proving the serializability of a transactional algorithm is already proved within the semantic model. Thus, proving serializability (or opacity) amounts simply to mapping the algorithm on to our rules, and showing that it satisfies the rules' criteria.
AB - We present a general theory of serializability, unifying a wide range of transactional algorithms, including some that are yet to come. To this end, we provide a compact semantics in which concurrent transactions PUSH their effects into the shared view (or UNPUSH to recall effects) and PULL the effects of potentially uncommitted concurrent transactions into their local view (or UNPULL to detangle). Each operation comes with simple criteria given in terms of commutativity (Lipton's left-movers and right-movers). The benefit of this model is that most of the elaborate reasoning (coinduction, simulation, subtle invariants, etc.) necessary for proving the serializability of a transactional algorithm is already proved within the semantic model. Thus, proving serializability (or opacity) amounts simply to mapping the algorithm on to our rules, and showing that it satisfies the rules' criteria.
KW - Abstract data-types
KW - Commutativity
KW - Movers
KW - Push/pull transactions
KW - Transactional boosting
KW - Transactional memory
UR - http://www.scopus.com/inward/record.url?scp=84951801339&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84951801339&partnerID=8YFLogxK
U2 - 10.1145/2737924.2737995
DO - 10.1145/2737924.2737995
M3 - Conference contribution
AN - SCOPUS:84951801339
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 186
EP - 195
BT - PLDI 2015 - Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
A2 - Blackburn, Steve
A2 - Grove, David
T2 - 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015
Y2 - 13 June 2015 through 17 June 2015
ER -