事务内存中延迟更新语义的安全性

事务内存允许用户将指令序列声明为推测性的“事务”，这些事务可以“提交”或“中止”。如果事务提交，它看起来像是顺序执行的，因此已提交的事务构成一个正确的顺序执行。如果事务中止，其任何指令都不能影响其他事务。流行的“不透明性”准则要求，中止事务的视图也必须与已提交事务所构成的全局顺序保持一致。这被认为是重要的，因为中止事务所观察到的不一致可能导致致命的不可恢复错误，或使系统陷入无限循环而浪费资源。直观上，一个不透明的实现必须确保事务在提交或中止之前获得的任何中间视图，都不会受到尚未开始提交的事务的影响，即所谓的“延迟更新”语义。本文旨在形式化地把握这一直觉。我们提出一种不透明性的变体，明确要求顺序执行尊重延迟更新语义。我们证明我们的准则是一个安全性属性，即它是前缀封闭和极限封闭的。与不透明性不同，我们的属性还确保一个历史的可序列化性蕴含其前缀的可序列化性。最后，我们证明，在假设没有两个事务在同一变量上提交相同值的前提下，我们的属性等价于不透明性，并给出当“唯一写入”假设不成立时的反例。