c++ - 如何使用 “non sequential”语义证明MT程序正确无误？

Question

这可能是一个与语言无关的问题，但实际上我对C++案例感兴趣:如何用支持MT编程的C++版本(即具有内存模型的现代C++)编写的多线程程序被证明是正确的？

在旧的C++中，MT程序只是使用pthread语义编写的，并根据pthread规则进行了验证，这在概念上很简单:正确使用基元并避免数据争用。

现在，C++语言语义是根据内存模型定义的，而不是按顺序执行原始步骤来定义的。 (标准也提到了“抽象机器”，但我再也听不懂它的意思了。)

如何用非顺序语义证明C++程序正确无误？有人会如何推理一个程序而不是一个又一个却没有执行原始步骤的程序？

Answer 1

与在C++内存模型之前使用pthreads相比，使用C++内存模型“在概念上更容易”。内存模型与pthread交互之前的C++宽松地指定，并且对该规范的合理解释允许编译器“引入”数据竞争，因此很难(如果可能的话)很难推理或证明MT算法的正确性。具有pthread的旧C++的上下文。

这个问题似乎存在根本的误解，因为C++从未定义为原始步骤的顺序执行。表达式评估之间总是存在部分排序的情况一直存在。除非有限制，否则允许编译器四处移动这样的表达式。内存模型的引入并没有改变。内存模型为执行的单独线程之间的评估引入了部分顺序。

“正确使用原语并避免数据争用”的建议仍然适用，但是C++内存模型更加严格和精确地限制了原语与语言其余部分之间的交互，从而可以进行更精确的推理。

在实践中，要证明这两种情况的正确性都不容易。大多数程序都没有证明没有数据争用。人们试图尽可能多地封装任何同步，以便对较小的组件进行推理，其中一些可以证明是正确的。人们使用诸如地址清除器和线程清除器之类的工具来捕获数据争用。

在数据竞赛中，POSIX says:

Applications shall ensure that access to any memory location by more than one thread of control (threads or processes) is restricted such that no thread of control can read or modify a memory location while another thread of control may be modifying it. Such access is restricted using functions that synchronize thread execution and also synchronize memory with respect to other threads.... Applications may allow more than one thread of control to read a memory location simultaneously.

在数据竞赛中，C++ says:

The execution of a program contains a data race if it contains two potentially concurrent conflicting actions, at least one of which is not atomic, and neither happens before the other, except for the special case for signal handlers described below. Any such data race results in undefined behavior.

C++定义了更多术语，并试图变得更加精确。其要点在于，两个禁止数据竞争，这两个都被定义为冲突的访问，而没有使用同步原语。

POSIX说pthread函数使内存相对于其他线程同步。这是未指定的。可以合理地解释为:(1)编译器无法在此类函数调用之间移动内存访问，并且(2)在一个线程中调用此类函数后，从该线程到内存的先前操作将在该线程之后对另一个线程可见。调用这样的函数。这是一种常见的解释，可以通过将函数视为不透明并可能破坏所有内存来轻松实现。

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

C++ says, with regard to mutex lock:

Synchronization: Prior unlock() operations on the same object shall synchronize with this operation.

因此，C++更加具体。您必须锁定和解锁同一个互斥锁才能进行同步。但是鉴于此，C++ says可以在新储物柜看到解锁之前的操作:

An evaluation A strongly happens before an evaluation D if ... there are evaluations B and C such that A is sequenced before B, B simply happens before C, and C is sequenced before D. [ Note: Informally, if A strongly happens before B, then A appears to be evaluated before B in all contexts. Strongly happens before excludes consume operations. — end note ]

(对于B =解锁，C =锁定，B只会在C之前发生，因为B与C同步。在先序列是在单个执行线程中的概念，因此，例如，一个完整表达式在下一个序列之前进行排序。)

因此，如果将自己限制为存在于pthread中的原语(锁，条件变量等)，以及pthread提供的保证类型(顺序一致性)，则C++应该不会感到惊讶。实际上，它消除了一些意外，增加了精度，并且更适合于正确性证明。

对于对这个主题感兴趣的任何人，对于当时的现状问题以及为在C++ 11内存模型中解决这些问题而做出的选择，这篇文章Foundations of the C++ Concurrency Memory Model都是不错的说明性阅读。

编辑以更清楚地说明问题的前提是有缺陷的，使用内存模型可以使推理更容易，并为Boehm论文添加了引用，Boehm论文也构成了一些论述。