CODEWITHSUNDEEP
adaspark-ada
jsinglet
jsinglet

Reputation: 1151

Specify that a Subprogram in another package is not blocking?

SPARK restricts the calling of potentially blocking subprograms from within protected objects.

However, I've noticed if I call ANY subprogram outside of the package in which the protected object lives I get the warning about a potentially blocking subprogram.

What is missing from the external package I'd like to use to tell it the call will be non-blocking? I've tried just putting a "add one to argument" subprogram in another package and it doesn't work. If I move it into the package containing the protected object it does.

What am I missing?

Upvotes: 2

Views: 137

Answers (2)

jsinglet
jsinglet

Reputation: 1151

Thank you @shark8 for your detailed answer.

I examined the body of the method I was trying to call and as it was a simple return statement, it did not have any of the effects mentioned in the manual.

I did however discover that turning on SPARK_Mode => On in the package I am trying to use fixed the issue.

Here's a MwE that reproduces the issue:

-- 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;

Upvotes: 2

Shark8
Shark8

Reputation: 4198

In Ada 2020 there is an attribute Non_Blocking which explicitly marks the blocking/nonblocking attributes for static-analysis and the compiler ensuring things are correct.

But this doesn't help if you're stuck in Ada 2012 — and there are specific things that are "potentially blocking" like entry-calls and [IIRC] things like Ada.Text_IO.Put — and SPARK takes the reasoning that if it's potentially blocking then you cannot ensure that it's not non-blocking.

According to the RM, here's what you have to look out for:

During a protected action, it is a bounded error to invoke an operation that is potentially blocking. The following are defined to be potentially blocking operations:

  • a select_statement;
  • an accept_statement;
  • an entry_call_statement;
  • a delay_statement;
  • an abort_statement;
  • task creation or activation;
  • an external call on a protected subprogram (or an external requeue) with the same target object as that of the protected action;
  • a call on a subprogram whose body contains a potentially blocking operation.

So, if the subprogram you're trying to call has a select, accept, delay, or task it's potentially blocking.

Upvotes: 2

Related Questions