如何用“非顺序”语义证明机器翻译程序是正确的?

在C++内存模型之前,C++内存模型比“概念”更容易“概念化”。在与PthPro交互的内存模型之前,C++被严格指定,并且对规范的合理解释允许编译器“引入”数据竞争,因此在旧的C++与PtLoG的上下文中,对MT算法的推理或证明是正确的(如果可能的话)是非常困难的。

在C++中,从来没有定义为原始步骤的顺序执行,这似乎有一个根本性的误解。表达式求值之间总是存在偏序的情况。编译器可以移动这些表达式,除非受到限制。记忆模型的引入并没有改变这一点。内存模型为不同执行线程之间的求值引入了偏序。

在数据竞赛上, POSIX says :

应用程序应确保多个控制线程(线程或进程)对任何内存位置的访问受到限制,这样当另一个控制线程可能正在修改某个内存位置时,任何控制线程都不能读取或修改该内存位置。使用同步线程执行并同步与其他线程相关的内存的函数来限制这种访问。。。。应用程序可以允许多个控制线程同时读取内存位置。

在数据竞赛上, C++ says

程序的执行包含 如果它包含两个 可能同时发生 动作,至少有一个不是原子的,而且 除下文所述的其他特殊案件处理人员外。任何这样的数据竞争都会导致未定义的行为。

POSIX说pthread函数 与其他线程同步内存

作为这个松散规范问题的一个例子,编译器仍然可以引入或删除内存访问(例如通过寄存器提升和溢出),并进行比必要的更大的访问(例如,访问结构中的相邻字段)。因此,编译器可以完全正确地“引入”不是直接在源代码中编写的数据竞争。C++ 11内存模型阻止了它这样做。

C++ says, with regard to mutex lock

同步:同一对象上的先前unlock()操作应与此操作同步。

C++ says 解锁前的操作对新储物柜可见:

A评价A 如果。。。有B和C两种评估方法,A在B之前排序,B在C之前发生,C在D之前排序。[注:非正式地说,如果A强发生在B之前,那么在所有上下文中,A似乎都在B之前被计算。强烈发生在排除消费操作之前。尾注]

(对于B=unlock,C=lock,B只发生在C之前,因为B与C同步。Sequenced before是单个执行线程中的一个概念,因此,例如,一个完整表达式在下一个表达式之前进行排序。)

Foundations of the C++ Concurrency Memory Model