在 SPARK 中不允许在干扰上下文中调用 volatile 函数

Question

我目前正在大学实时编程语言课程中学习 Ada，对 SPARK 有疑问。

我正在从事一个项目，其任务是监控离网电源。这项任务对机器安全至关重要，因此应尽可能无差错，例如通过 SPARK 证明。我能够得到一些关于 Whosebug 的运行其他问题，但我仍然运行遇到无法通过用户指南中的快速搜索修复的错误。

参考

中的if monitoring_interface.is_all_config_set then ...行，错误是call to a volatile function in interfering context is not allowed in SPARK

task body monitoring_task is
      next_time : Time;
   begin
      --  Initialisation of next execution time
      next_time := Clock;
      --  Superloop
      loop
         Put_Line ("Run task monitoring");
         --  Load monitor configuration
         monitor_pfc_voltage.config := monitoring_interface.get_monitor_pfc_voltage_config;
         monitor_pfc_current.config := monitoring_interface.get_monitor_pfc_current_config;
         monitor_output_voltage.config := monitoring_interface.get_monitor_output_voltage_config;
         monitor_output_current.config := monitoring_interface.get_monitor_output_current_config;

         --  Check if module has been configured correctly
         --  Don't do anything otherwise
         if monitoring_interface.is_all_config_set then --  <= erroneous line
            do_monitoring;
         end if;

         next_time := next_time + TASK_PERIOD;
         delay until next_time;
      end loop;
   end monitoring_task;

函数 is_all_config_set 是在我用于任务间通信的受保护类型中定义的。

package PSU_Monitoring is

   ... Declaration of some types (Monitor_Config_T) ...

   protected type Monitoring_Interface_T is
      function is_all_config_set return Boolean;

      procedure set_monitor_pfc_voltage_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_pfc_voltage_config return Monitor_Config_T;

      procedure set_monitor_pfc_current_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_pfc_current_config return Monitor_Config_T;

      procedure set_monitor_output_voltage_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_output_voltage_config return Monitor_Config_T;

      procedure set_monitor_output_current_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_output_current_config return Monitor_Config_T; 
   private
      --  Configuration for PFC intermediate voltage
      monitor_pfc_voltage_config : Monitor_Config_T;
      monitor_pfc_voltage_config_set : Boolean := False;
      --  Configuration for PFC inductor current
      monitor_pfc_current_config : Monitor_Config_T;
      monitor_pfc_current_config_set : Boolean := False;
      --  Configuration for output voltage
      monitor_output_voltage_config : Monitor_Config_T;
      monitor_output_voltage_config_set : Boolean := False;
      --  Configuration for output inductor current
      monitor_output_current_config : Monitor_Config_T;
      monitor_output_current_config_set : Boolean := False;
   end Monitoring_Interface_T;

   monitoring_interface : Monitoring_Interface_T;

private

... Declaration of a task and some private constants and subprograms ...

end PSU_Monitoring

相应正文为

package body PSU_Monitoring is

   protected body Monitoring_Interface_T is

      function is_all_config_set return Boolean is
      begin
         return monitor_pfc_voltage_config_set and monitor_pfc_current_config_set and monitor_output_voltage_config_set and monitor_output_current_config_set;
      end is_all_config_set;

      procedure set_monitor_pfc_voltage_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_pfc_voltage_config := new_monitor_config;
         monitor_pfc_voltage_config_set := True;
      end set_monitor_pfc_voltage_config;

      function get_monitor_pfc_voltage_config return Monitor_Config_T is
      begin
         return monitor_pfc_voltage_config;
      end get_monitor_pfc_voltage_config;

      procedure set_monitor_pfc_current_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_pfc_current_config := new_monitor_config;
         monitor_pfc_current_config_set := True;
      end set_monitor_pfc_current_config;

      function get_monitor_pfc_current_config return Monitor_Config_T is
      begin
         return monitor_pfc_current_config;
      end get_monitor_pfc_current_config;

      procedure set_monitor_output_voltage_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_output_voltage_config := new_monitor_config;
         monitor_output_voltage_config_set := True;
      end set_monitor_output_voltage_config;

      function get_monitor_output_voltage_config return Monitor_Config_T is
      begin
         return monitor_output_voltage_config;
      end get_monitor_output_voltage_config;

      procedure set_monitor_output_current_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_output_current_config := new_monitor_config;
         monitor_output_current_config_set := True;
      end set_monitor_output_current_config;

      function get_monitor_output_current_config return Monitor_Config_T is
      begin
         return monitor_output_current_config;
      end get_monitor_output_current_config;

   end Monitoring_Interface_T;

... Definition of the remaining subprograms defined in the specification file ...

end PSU_Monitoring;

这里有什么问题？

Answer 1

正如 Jeffrey 所说，我们需要查看程序中标记错误的部分。一般来说，这与有副作用的功能有关，参见参考手册： http://docs.adacore.com/spark2014-docs/html/lrm/packages.html#external-state-variables

如果您以 "wrong" 方式使用实时包中的时钟函数，则可以观察到相同的错误消息：

with Ada.Real_Time; use Ada.Real_Time;
with Ada.Text_IO; use Ada.Text_IO;

procedure Main with SPARK_Mode is
    Last : Time := Clock;
begin

    -- some stuff happening here ...

    if Clock > Last + Milliseconds(100) then
        Put_Line("Too late");
    end if;
end Main;

Clock 是一个有副作用的函数（每次调用它时 returns 都有不同的值），在此示例中，该函数用于所谓的 "interfering context"（请参阅 link上面的定义）。

解决方案是稍微重写您的代码：

with Ada.Real_Time; use Ada.Real_Time;
with Ada.Text_IO; use Ada.Text_IO;

procedure Main with SPARK_Mode is
    Last : Time := Clock;
begin

    -- some code
    declare
        now : Time := Clock;
    begin      
        if now > Last + Milliseconds(100) then
            Put_Line("Too late");
        end if;
    end;
end Main;

所以，基本上，您所做的是将对具有副作用的函数的调用隔离到一个单独的语句中，将结果保存在一个变量中，然后在您之前进行调用的地方使用该变量。这个技巧也应该有助于您调用受保护的对象。

在 SPARK 中不允许在干扰上下文中调用 volatile 函数

Call to a volatile function in interfering context is not allowed in SPARK

ada

gnat

spark-ada