$$ \def\read{\mathsf{read}} \def\write{\mathsf{write}} \def\SER{\mathsf{SER}} \def\SI{\mathsf{SI}} \def\po{\mathsf{\textcolor{red}{po}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\VIS{\mathsf{\textcolor{orange}{VIS}}} \def\CO{\mathsf{\textcolor{orange}{CO}}} \def\WR{\mathsf{\textcolor{green}{WR}}} \def\WW{\mathsf{\textcolor{red}{WW}}} \def\RW{\mathsf{\textcolor{blue}{RW}}} \def\H{\mathcal{H}} \def\T{\mathcal{T}} \def\X{\mathcal{X}} \def\G{\mathcal{G}} \def\P{\mathcal{P}} \def\Int{\mathtt{Int}} \def\Ext{\mathtt{Ext}} \def\Session{\mathtt{Session}} \def\Prefix{\mathtt{Prefix}} \def\NoConflict{\mathtt{NoConflict}} \def\TotalVis{\mathtt{TotalVis}} \def\PreExecSI{\mathsf{PreExecSI}} \def\ExecSI{\mathsf{ExecSI}} \def\ExecSER{\mathsf{ExecSER}} \def\HistSI{\mathsf{HistSI}} \def\HistSER{\mathsf{HistSER}} \def\GraphSER{\mathsf{GraphSER}} \def\GraphSI{\mathsf{GraphSI}} \def\graph{\mathsf{graph}} \def\splice{\mathsf{splice}} \def\DCG{\mathsf{DCG}} $$
摘要
快照隔离(SI)是一种广泛使用的事务处理一致性模型,由大多数主流数据库和一些事务内存系统实现。不幸的是,它的经典定义是以低级操作方式给出的,通过理想化的并发控制算法,这使得对在 SI 下运行的应用程序的行为的推理变得复杂。我们给出了 SI 的替代规范,该规范根据 Adya 等人的事务依赖图对其进行了描述,概括了序列化图。与以前的工作不同,我们的描述不需要在依赖图中添加有关事务开始点和提交点的额外信息。然后,我们利用我们的规范来获得两种静态分析。第一个检查在 SI 下运行的一组事务何时可以分成更小的部分而不引入新的行为,以提高性能。另一个分析检查在 SI 减弱的情况下运行的一组事务是否与在 SI 下运行时的行为相同。
作者:
- Andrea Cerone, IMDEA Software Institute
- Alexey Gotsman, IMDEA Software Institute
