Programming Languages
《漏水的分号》
Author
Venue
ACM 2021年编程语言会议论文集
Abstract
程序逻辑与语义为顺序组合描绘了一幅美好的图景：在执行 (S1; S2) 时，我们先执行 S1，再执行 S2。然而，为了提升性能，处理器会以乱序方式执行指令，而编译器对程序的重新排序则更为剧烈。按设计，单线程系统无法察觉这些重新排序；但多线程系统却能察觉，这使得上述图景变得不那么美好。 一种旨在理解由此产生的混乱的正式尝试被称为“宽松内存模型”。先前的模型要么未能直接处理顺序组合，要么过度限制了处理器和编译器，要么允许在实践中无法观察到的荒谬的“凭空”行为。为了在支持顺序组合的同时适应现代硬件，我们通过先决条件和谓词转换器族来丰富标准的基于事件的方法。 在计算 (S1;S2) 的含义时，针对 S2 中事件 e 的先决条件所应用的谓词转换器，是根据 e 所依赖的 S1 中的事件集来选择的。我们将此方法应用于两种现有的内存模型。
