Блог

Какой хороший способ связать индексированную задачу с соответствующим индексированным защищенным типом в 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 с Ravenscar более требователен. Я попробовал два подхода, которые, похоже, работают нормально, когда я их запускаю:

1. Укажите T Integer дискриминант, затем создайте экземпляр T(i); для каждого i , но это становится обременительным при не очень больших i размерах.

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

2. Добавьте is_not_monitored функцию и set_monitor процедуру в P . Создайте массив задач без дискриминанта. При 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» ворчит по поводу потенциальной гонки данных, и я понимаю почему (хотя я не уверен, что это действительно связано с этим).

Отсюда и вопрос.

Это не приводит к блокировке gnatprove.

И я думаю, что основное отличие от вашего варианта 2 заключается в том, что Claim проверяет, возможно ли утверждение, и, если да, выполняет утверждение в одном защищенном вызове.

Но я не совсем понимаю, как доказать, что цикл 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;
  

После внеполосных обсуждений с Джоном мы обнаружили, что это постусловие может быть доказано:

   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)
  

Я не эксперт в этом, но, похоже, вы не можете показать SPARK, что существует однозначная связь между экземпляром задачи и экземпляром защищенного объекта, если вы явно не ссылаетесь на этот экземпляр защищенного объекта из экземпляра задачи. Это, в частности, для того, чтобы заставить SPARK доказать, что только одна задача будет стоять в очереди при входе в защищенный объект; Wait запись в коде ниже). Следовательно (и хотя это может быть не совсем то, что вы ищете), я мог решить проблему подключения задач и защищенных объектов и в то же время иметь функциональность монитора, используя универсальный пакет, который может создаваться несколько раз. Это подтверждается в 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;
  

с телом:

 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;