编译器检测任务之间的竞争条件

Question

我的日常工作是使用对安全至关重要的嵌入式系统。我还与客户就编写安全嵌入式代码的主题进行了一些教学/咨询。编程语言的问题总是会出现，我们比较 C、D、Ada、Erlang、Rust 等。

我经常使用一个练习来进行演示。这是一个简单的双线程程序，每个线程获取一个全局变量（初始化为 0），将其加 1 并替换它十次。然后我们推测变量在末尾可以具有的最大值 (20) 和它的最小值（我们通常在使用正式证明证明它可以是 2 之前决定 10）。

我演示的一件事是程序的 C 版本可以编译（危险），但 Rust 版本不能（好！）。今天我写了 Ada 版本，并且有两个惊喜，我想请教 cmets。首先，我的程序：

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 任务是否未映射到 pthread？ Ada 版本中是否有隐式循环调度？

循环加法循环 10 次大概不会花费很长时间，所以我尝试将循环计数增加到 100 以查看任务是否可以更频繁地中断。然后我只得到 200 和 100。

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 对象不能出现在这个上下文中 (SPARK RM 7.1.3(12)) main.adb:12:13: volatile 对象不能出现在 此上下文（SPARK RM 7.1.3(11)） gnatprove：生成期间出错 全球合同

在我看来，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。

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);

这确实会产生您所期望的差异。

欢迎解释！