程序逻辑和语义讲述了一个关于顺序组合的愉快故事：当执行（𝑆1; 𝑆2）时，我们首先执行 𝑆1，然后是 𝑆2。 然而，为了提高性能，处理器会不按顺序执行指令，而编译器则会更大幅度地重新排列程序。 根据设计，单线程系统无法观察到这些重新排序。然而，多线程系统可以，这就使故事变得相当不愉快。 试图弄清由此产生的混乱被正式称为“松弛型内存模型”。

先前的模型未能直接解决顺序组成问题，或过度限制处理器和编译器，或允许在实践中无法观察到的无稽之谈的凭空行为。 为了支持顺序组合，同时针对现代硬件，我们用前提条件和谓词变换器系列丰富了基于事件的标准方法。 在计算（𝑆1; 𝑆2）的意义时，应用于 𝑆2 中的事件 𝑒 的前提条件的谓词变换器是根据 𝑆1 中的事件集来选择的，而 𝑒 则依赖于此。

• 项目代码库