代码之家 › 专栏 › 技术社区 › John Perry

Ada:任务数组

ada task concurrency arrays

John Perry · 技术社区 · 7 年前

请考虑设置细节:

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

为每一个 p(i) 我想要个任务 t(i) 监视当它准备好的时候,处理它。在Ada中我可以很容易地完成这个任务,但是SPARK w/Ravenscar要求更高。我尝试过两种方法,当我运行它们时,它们似乎运行得很好:

给予 T 安 Integer 判别,然后实例化 T(i); 为每一个 i 但是这会增加不太大的负担 .

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

is_not_monitored 函数和 set_monitor 程序 P . 创建任务数组没有区别对待。什么时候? t(一) 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“证明”抱怨潜在的数据竞争,我可以理解原因(尽管我不确定这是否是因为这个)。

0 回复 | 直到 7 年前

Simon Wright 7 年前

这不会导致gnatpreve窒息。

Claim

但我不太明白如何证明这个循环在里面 T 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

我们还发现了一些替代配方,这些配方在2017年的GPL中得到了证明,但在2018年CE中没有:例如,

      (Is_Claimed
       and
       (Is_Claimed'Old xor Succeeded)

DeeDee 7 年前

我不是这方面的专家,但似乎你无法向SPARK证明任务实例和受保护对象实例之间存在一对一的关系,除非你从任务实例中显式引用该受保护对象实例。这特别是为了使SPARK证明只有一个任务将在受保护对象的条目上排队 Wait 在下面的代码中输入)。因此(虽然这可能不是您所要寻找的),我只能通过使用一个可以多次实例化的通用包来解决连接任务和受保护对象的问题,同时还具有监视器功能。这在2018年GNAT CE会议上证明:

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;

带主体:

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;