ada - 指定另一个包中的子程序没有阻塞？

Question

SPARK 限制从受保护对象中调用可能阻塞的子程序。

但是，我注意到如果我在受保护对象所在的包之外调用任何子程序，我会收到有关潜在阻塞子程序的警告。

我想用来告诉它调用将是非阻塞的外部包中缺少什么？我试过在另一个包中放一个“添加一个参数”子程序，但它不起作用。如果我将它移动到包含受保护对象的包中，它会这样做。

我错过了什么？

Answer 1

在 Ada 2020 中，有一个属性Non_Blocking明确标记了静态分析的阻塞/非阻塞属性，编译器确保一切正确。

但是，如果你被困在 Ada 2012 中，这将无济于事——并且有一些特定的东西“可能阻塞”，比如入口调用和 [IIRC] 之类的东西——SPARKAda.Text_IO.Put的推理是，如果它可能阻塞，那么你不能确保它不是非阻塞的。

根据RM，您需要注意以下几点：

在受保护的操作期间，调用可能阻塞的操作是有界错误。以下被定义为潜在的阻塞操作：

• 一个选择语句；
• 一个accept_statement；
• entry_call_statement；
• 延迟声明；
• abort_statement；
• 任务创建或激活；
• 对受保护子程序（或外部重新排队）的外部调用，其目标对象与受保护动作的目标对象相同；
• 对其主体包含潜在阻塞操作的子程序的调用。

因此，如果您尝试调用的子程序有select, accept, delay，或者task它可能会阻塞。

Answer 2

谢谢@shark8 的详细回答。

我检查了我试图调用的方法的主体，因为它是一个简单的返回语句，它没有手册中提到的任何效果。

然而，我确实SPARK_Mode => On发现在我尝试使用的包中打开解决了这个问题。

这是重现该问题的 MwE：

-- main.adb

pragma Profile (GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);

with P1;

procedure Main is

begin
   --  Insert code here.
   null;
end Main;

-- simple.ads
package Simple is

   procedure Do_Nothing;

end Simple;

-- simple.adb 
package body Simple is

   procedure Do_Nothing is
   begin
      null;
   end Do_Nothing;


end Simple;

-- p1.ads
pragma Profile (GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);

package P1 with 
  SPARK_Mode => On 
is

   protected Protected_Object with 
     SPARK_Mode => On
   is
      procedure Do_Something;
   end Protected_Object;


end P1;

-- p1.adb 
with Simple;

package body P1 with 
  SPARK_Mode => On 
is

   protected body Protected_Object 
   with 
     SPARK_Mode => On 
   is      
      procedure Do_Something is 
      begin
         Simple.Do_Nothing;
      end Do_Something;
   end Protected_Object;


end P1;