编译器如何检测任务之间的竞态条件

Question

我的日常工作是处理安全关键型嵌入式系统。我还向客户提供一些有关编写安全嵌入式代码的教学/咨询服务。在比较C、D、Ada、Erlang、Rust等编程语言时，我们经常会讨论这个问题。

我经常使用一个简单的双线程程序来进行演示。每个线程都要从一个全局变量（初始化为0）中获取值，并将其加1并替换10次。然后我们推测该变量可以达到的最大值（20）和最小值（通常我们决定在使用正式证明之前先确定为10，以证明它可能是2）。

我展示的一件事是C版本的程序可以编译（存在风险），但Rust版本不行（很好！）。今天我写了Ada版本，并遇到了两个惊喜，想请教您的意见。首先是我的程序：

with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
   task AddTenA;
   task AddTenB;

   --  Global variable

   x : Natural := 0;

   finished : array (0 .. 1) of Natural := (0, 0);

   --  Make sure that the compiler doesn't remove
   --  all the addition.

   pragma Volatile (x);

   task body AddTenA is
      y : Integer;
   begin
      for I in 1 .. 10 loop
         y := x + 1;
         x := y;
      end loop;
      finished (0) := 1;
   end AddTenA;
   
   task body AddTenB is
      y : Integer;
   begin
      for I in 1 .. 10 loop
         y := x + 1;
         x := y;
      end loop;
      finished (1) := 1;
   end AddTenB;
   
begin

   while finished (0) + finished (1) < 2 loop
      delay 0.001;
   end loop;

   Put_Line (Integer'Image (x));

end Main;

是的，我熟悉受保护对象和任务会合，但这不是该程序的重点。

我的两个惊喜：

1. 即使使用了完整的编译器标志字母表（-fstack-check，-gnata，-gnato13，-gnatf，-gnatwa，-g，-gnatVa，-gnaty3abcdefhiklmnoOprstux，-gnatwe，-gnat2012，-Wall，-O2），我仍然没有收到编译器警告。Rust 告诉我全局变量没有唯一的所有者，因此它不会为我编译 Rust 版本的程序。我知道 SPARK 不能处理任务，所以 Ada 不会生成有关代码中可能存在危险竞争条件的警告，这在 Ada 这样的语言中让我感到惊讶。我错过了一个聪明的编译器或运行时选项吗？

2. 当我执行相应的 C 程序时，最常见的输出是 20，但是当我运行多次时，我得到的值相差很大，通常在 8 到 20 之间。我已经运行了上面的 Ada 程序 500,000 次，并且只得到了 10 和 20 的值（没有中间值，并且 99.9% 的输出是 20）。这表明 C 的 pthreading 和 Ada 的 Tasking 之间存在一些根本性的差异。那是什么？Ada 任务没有映射到 pthreads 吗？在 Ada 版本中有隐含的轮换调度吗？

假设循环增加了 10 次不需要太长时间，所以我已经将循环次数增加到 100，以查看任务是否会更频繁地被中断。然后我只得到了 200 和 100。

- Chris Hobbs

---

只是一条信息注释（类似 FYI 的东西）：Rust（和 SPARK）检测到“数据竞争”，这是对非原子数据的多线程访问，可能导致错误值。 “竞态条件”是允许您的数据处于您不希望的有效状态的逻辑错误。 Rust 和 SPARK 都可能在编译时错过竞态条件（尽管如果编写得好，SPARK 的合同很可能会捕获它）。 - Jere

你的系统有多少个处理器？现代系统通常有多个处理器，如果可用的处理器数量>= 3，则每个任务通常都会在自己的处理器上运行，并且不会进行任务调度。在这种情况下，竞争应该是显而易见的，值<20很常见。在单个处理器上，默认的调度策略是一个任务在另一个任务获得处理器之前运行到完成，因此总是期望20。我现在看到了您关于使用Zoom进一步混淆此问题的评论。 - Jeffrey R. Carter

我还记得一个简单的问题是“有多少个处理器？”现在我们区分处理器和核心，英特尔还加入了超线程技术来让我们保持警惕。回到8080年代（我正在打字时桌子抽屉里有一台），一切都被原谅了。无论如何，我有4个处理器和2个核心。我使用Zoom和其他多线程处理器占用程序来加载系统。我的剩下的惊喜是，使用C和Python等价的程序，我通常会得到10到20之间的一些值，但有时会低至8。而使用Ada版本，我似乎只能得到10或20。 - Chris Hobbs

我的第一反应是编译器可能正在展开您的循环，甚至可能将最终赋值给x保存到最后。如果您还没有尝试过，在调试模式下编译代码。 - Patrick

Answer 1

我使用 GNAT Community 2020 版本时，在使用 SPARK 时出现以下诊断：

package threads with
   SPARK_Mode
is
   X : Natural := 0;
   pragma Volatile (X);

   task type AddTen with
   Global => (in_out => X);
end threads;

pragma Ada_2012;
package body threads with
SPARK_Mode
is

   ------------
   -- AddTen --
   ------------

   task body AddTen is
      Y : Integer;
   begin
      for I in 1 .. 10 loop
         Y := X + 1;
         X := Y;
      end loop;
   end AddTen;

end threads;

with Ada.Text_IO; use Ada.Text_IO;
with threads; use threads;

procedure Main with SPARK_Mode is
begin
   declare
      A : AddTen;
      B : AddTen;
   begin
      null;
   end;
   Put_Line(X'Image);
end Main;

当我检查所有源代码时，SPARK 给出了以下信息：

gnatprove -PD:\Ada\Stack_Overflow\Race\race.gpr -j0 --mode=flow --ide-progress-bar -U Phase 1 of 2: generation of Global contracts ... threads.adb:14:15: volatile object cannot appear in this context (SPARK RM 7.1.3(12)) main.adb:12:13: volatile object cannot appear in this context (SPARK RM 7.1.3(11)) gnatprove: error during generation of Global contracts

在我的看法中，SPARK 确实将使用 volatile 对象视为不正确的。

当我简化程序，将 volatile 改为 atomic 并消除对 SPARK 的使用时，如下所示：

with Ada.Text_IO; use Ada.Text_IO;

procedure Main is
   X : Natural := 0;
   pragma Atomic (X);

   task type AddTen;
   task body AddTen is
      Y : Integer;
   begin
      for I in 1 .. 100 loop
         Y := X + 1;
         X := Y;
      end loop;
   end AddTen;
begin
   declare
      A, B : AddTen;
   begin
      null;
   end;
  
   Put_Line(X'Image);
end Main;

我始终得到200的结果。

请注意，在内部块中运行任务会导致主过程的外部块等待内部块完成，只有当两个任务都完成时，内部块才会完成。

当我将上限循环范围更改为10000以强制执行更长时间时，我得到了各种数字，例如15509、16318、15283、14555。

- Jim Rogers

---

你（当然）是对的：我现在得到了相同的错误信息。我之前看到了《使用SPARK构建高完整性应用程序》一书中John W McComick和Peter Chapin的评论，其中提到：“本文撰写时[2015年]可用的SPARK 2014版本不支持任何Ada任务特性...”。 - Chris Hobbs

是的，在循环中使用更大的数字可以使线程运行足够长的时间以获取调度操作。对于C程序，我不需要超过10。我只运行了它100,000次： 10-> 9次 11-> 1次 12-> 1次 13-> 1次 15-> 4次 16-> 2次 17-> 1次 18-> 1次 19-> 1次 20-> 99979次 - Chris Hobbs

Answer 2

除了轮流调度（默认情况下通常是优先级中的FIFO），为什么任务会互换？那里没有调度点。我应该补充说，我更习惯在单处理器MCU上使用Ravenscar RTS进行调度，所以我可能有错误的想法！ 这将导致每次都是200，显然不是这种情况（顺便说一句，当循环次数为10_000_000时，结果非常相似！但我总是看到一个结果为10000000）。我想主程序中的delay可能会对调度产生一些影响。

我尝试只使用

pragma Task_Dispatching_Policy 
  (Round_Robin_Within_Priorities);

没有效果。

然后

Ada.Dispatching.Round_Robin.Set_Quantum 
  (System.Default_Priority,
   Ada.Real_Time.Microseconds (2));

这会导致错误

Round_Robin is not supported in this configuration

（配置为macOS/GCC 10.1.0）。

然后

pragma Atomic (x);

这确实能够产生您期望的差异。

欢迎解释！

- Simon Wright

---

关于调度点，我应该提到当我做测试时，我会故意将视频或其他东西运行在更高的优先级上。Zoom在这方面表现得特别好/不好：当我在Zoom通话中进行演示时，数值的分布范围比使用其他任何程序都要宽广得多。而且，进行演示所需的时间几乎是不用Zoom时的两倍。我猜测Zoom启动了许多高优先级线程，并且我正在一台相当慢的笔记本电脑上运行。 - Chris Hobbs

该程序实际上存在错误，参见[ARM 9.10（11）]（http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-9-10.html#p13） - 尽管似乎存在与[ARM C.6（17）]（http://www.ada-auth.org/standards/rm12_w_tc1/html/RM-C-6.html#p17）之间的冲突！ - Simon Wright

换句话说（主要是为了检查我的理解），Ada允许错误的程序（例如，如果您避免使用正确的工具，就像这个例子中尖叫的保护对象一样，你会得到你应得的），但SPARK不允许？ - user1818839

听起来没错，除了检测错误代码是SPARK的设计目标之一，这可能在某些情况下无法实现。我想他们可以扫描ARM中所有出现的单词，并为所有单词实现检查...但即使如此，仍然有可能会有一些聪明的人问ARG：“这个{晦涩的案例}不应该是错误的吗？”然后ARG说“哎呀”。顺便说一句，我用System.Atomic_Operations.Modular_Arithmetic（202X功能，在GNAT CE 2020中实现）实现了这个问题，感觉很有趣。 - Simon Wright

是的，我刚刚尝试了带有System.Atomic_Operations.Modular_Arithmetic版本的程序。它通过始终工作来破坏问题！ - Chris Hobbs