Ada：任务数组

Question

将索引任务 link 到 SPARK 中相应索引保护类型的好方法是什么？

有关细节，请考虑以下设置：

subtype Thread_Range is Natural range 1..n;
protected type P is ... end P;
p: array(Thread_Range) of P;

对于每个 p(i) 我想要一个任务 t(i) 来监视 p(i) 并在准备就绪时对其进行处理。我可以在 Ada 中轻松完成这项工作，但 SPARK w/Ravenscar 要求更高。我已经尝试了两种方法，当我运行它们时它们似乎工作正常：

给 T 一个 Integer 判别式，然后为每个 i 实例化一个 T(i);，但是如果 i 不是很大，这会变得很麻烦.

task type T(which: Integer);
t1: T(1);
t2: T(2);
...

向 P 添加一个 is_not_monitored 函数和一个 set_monitor 过程。创建一个没有判别式的任务数组。当 t(i) 开始时，它将自己分配给第一个 p(j) 它发现尚未分配监视器的监视器。

task type T;
task body T is
  which: Integer;
  available: Boolean;
begin
  for i in Thread_Range loop
    available := p(i).is_not_monitored;
    if available then
      p(i).set_monitor;
      which := i;
    end if;
  end loop;
  -- what the task does with p(i) follows
end T;
t: array(Thread_Range) of T;

我更喜欢第二个，但不是很多。无论如何，SPARK "Prove" 抱怨潜在的数据竞争，我明白为什么（虽然我不确定它实际上是由于这个）。

因此问题。

Answer 1

这不会导致 gnatprove 窒息。

我认为与您的选项 2 的主要区别在于 Claim 检查声明是否可行，如果可行，则在一次受保护的调用中执行声明。

但我不太明白如何证明 T 中的循环 Claim 退出并声明了 Ps (J)。我尝试在循环之后放置一个断言，但无法证明它。

protected type P is
   procedure Claim (Succeeded : out Boolean);
private
   Claimed : Boolean := False;
end P;

subtype Thread_Range is Integer range 1 .. 2;

Ps : array (Thread_Range) of P;

Ts : array (Thread_Range) of T;

task body T is
   Which : Integer;
begin
Claim:
   for J in Thread_Range loop
      declare
         Claimed : Boolean;
      begin
         Ps (J).Claim (Succeeded => Claimed);
         if Claimed then
            Which := J;
            exit Claim;
         end if;
      end;
   end loop Claim;

   loop  -- having a loop keeps gnatprove quiet
      delay until Ada.Real_Time.Time_Last;
   end loop;
end T;

protected body P is
   procedure Claim (Succeeded : out Boolean) is
   begin
      if not Claimed then
         Claimed := True;
         Succeeded := True;
      else
         Succeeded := False;
      end if;
   end Claim;
end P;

经过与 John 的带外讨论，我们发现这个后置条件可以证明：

  procedure Claim (Succeeded : out Boolean)
  with
    Post =>
      (Is_Claimed'Old or (Succeeded and Is_Claimed))
      or
      (not Succeeded and Is_Claimed);

注意不是P’Old.Is_Claimed，主要是因为’Old需要复制，而P是受限的（因为是保护类型）

我们还发现了几种在 GPL 2017 中证明但在 CE 2018 中未证明的替代公式：例如，

      (Is_Claimed
       and
       (Is_Claimed'Old xor Succeeded)

Answer 2

我不是这方面的专家，但似乎您无法向 SPARK 证明任务实例和受保护的 object 实例之间存在 one-to-one 关系，除非您引用受保护的 object 实例显式来自任务实例。这特别是为了让 SPARK 证明只有一个任务会 queue 进入受保护的 object；下面代码中的 Wait 条目）。因此（虽然这可能不是你正在寻找的），我只能通过使用通用包解决连接任务和受保护 objects 的问题，同时具有监视器功能可以多次实例化。这在 GNAT CE 2018 中得到证明：

generic
package Generic_Worker with SPARK_Mode is   

   task T;

   protected P is
      entry Wait;
      procedure Trigger;
   private
      Triggered : Boolean := False;
   end P;

end Generic_Worker;

与 body:

package body Generic_Worker with SPARK_Mode is

   task body T is      
   begin
      loop   --  Ravenscar: Tasks must not terminate.         
         P.Wait;
      end loop;
   end T;

   protected body P is

      entry Wait when Triggered is
      begin
         Triggered := False; 
         --  Do some work.
      end Wait;

      procedure Trigger is
      begin
         Triggered := True;
      end Trigger;

   end P;

end Generic_Worker;

和实例化：

with Generic_Worker;

pragma Elaborate_All (Generic_Worker);

package Workers with SPARK_Mode is

   package Worker_0 is new Generic_Worker;
   package Worker_1 is new Generic_Worker;
   package Worker_2 is new Generic_Worker;
   package Worker_3 is new Generic_Worker;
   package Worker_4 is new Generic_Worker;

end Workers;

Ada：任务数组

Ada: Array of tasks

arrays

concurrency

ada

task