我的日常工作是处理安全关键型嵌入式系统。我还向客户提供一些有关编写安全嵌入式代码的教学/咨询服务。在比较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;
是的,我熟悉受保护对象和任务会合,但这不是该程序的重点。
我的两个惊喜:
即使使用了完整的编译器标志字母表(-fstack-check,-gnata,-gnato13,-gnatf,-gnatwa,-g,-gnatVa,-gnaty3abcdefhiklmnoOprstux,-gnatwe,-gnat2012,-Wall,-O2),我仍然没有收到编译器警告。Rust 告诉我全局变量没有唯一的所有者,因此它不会为我编译 Rust 版本的程序。我知道 SPARK 不能处理任务,所以 Ada 不会生成有关代码中可能存在危险竞争条件的警告,这在 Ada 这样的语言中让我感到惊讶。我错过了一个聪明的编译器或运行时选项吗?
当我执行相应的 C 程序时,最常见的输出是 20,但是当我运行多次时,我得到的值相差很大,通常在 8 到 20 之间。我已经运行了上面的 Ada 程序 500,000 次,并且只得到了 10 和 20 的值(没有中间值,并且 99.9% 的输出是 20)。这表明 C 的 pthreading 和 Ada 的 Tasking 之间存在一些根本性的差异。那是什么?Ada 任务没有映射到 pthreads 吗?在 Ada 版本中有隐含的轮换调度吗?
假设循环增加了 10 次不需要太长时间,所以我已经将循环次数增加到 100,以查看任务是否会更频繁地被中断。然后我只得到了 200 和 100。