The Push/Pull model of transactions
The Push/Pull model of transactions
复制标题
交易的推/拉模型
DOI：
10.1145/2737924.2737995
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Matthew J. Parkinson
中科院分区：
文献类型：
--
作者：
Eric Koskinen;Matthew J. Parkinson
我们提出了序列化性的一般理论，统一了广泛的交易算法，包括一些尚未来的算法。为此，我们提供了一种紧凑的语义，在该语义中，并发交易将其效果推向了共享的视图（或不及以召回效果），并将潜在的不合同的交易的效果提升到其本地视图（或删除且截断）。每个操作都有简单的标准，就通勤性（立顿的左移动者和右移动者）提供。该模型的好处是，在语义模型中已经证明了大多数详细的推理（共同诱导，模拟，微妙的不变等），这已经证明了交易算法的序列化。因此，证明序列化（或不透明度）仅仅是将算法映射到我们的规则上，并表明其满足规则的标准。
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.