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

我的日常工作是使用安全关键的嵌入式系统。我还与客户就编写安全嵌入式代码的主题进行了一些教学/咨询。编程语言的问题总是出现，我们比较了 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。

回答