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

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

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

我演示的一件事是程序的 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。

回答

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;

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;