事务内存中的非干扰性与局部正确性

事务内存承诺通过允许用户将动作序列组装成具有全有或全无语义的原子事务，使并发编程变得可行且高效。人们认为，凭借其固有特性，事务内存必须确保所有已提交的事务构成一个尊重实时顺序的串行执行。相比之下，已中止或未完成的事务不应“生效”。但“不生效”究竟意味着什么？很自然地会预期，已中止或未完成的事务不会出现在全局串行执行中，因此任何已提交的事务都不会受到它们的影响。我们研究了“不生效”的另一个不太明显的特征，称为非干扰性：已中止或未完成的事务不应迫使任何其他事务中止。在本文探讨的最强形式的非干扰性中，通过从历史记录中移除一部分已中止或未完成的事务，我们不应能够在不违反正确性准则的情况下将已中止的事务转变为已提交的事务。我们表明，在严格意义上，相对于流行的不透明性（opacity）准则，非干扰性是不可实现的，该准则要求所有事务（无论是已提交、已中止还是未完成）都见证相同的全局串行执行。相比之下，当我们仅要求局部正确性时，非干扰性是可实现的。非正式地说，如果一个正确性准则仅要求每个事务可以与（其最后事件之前提交的）一部分事务一起被串行化（忽略已中止或未完成的事务），那么该准则就是局部的。我们给出了几个局部正确性属性的示例，包括最近提出的虚拟世界一致性准则，并展示了一个简单但高效的实现，该实现满足非干扰性和局部不透明性。