Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore <brad.moore@shaw.ca>]

On 10/05/2014 2:27 PM, Dmitry A. Kazakov wrote:
>> If Foo calls Bar, and both Foo and Bar have the Task_Safe aspect, but
>> some time later the maintainer of Bar decides to change its
>> implementation to refer to some global variable or call some other
>> subprogram that doesn't have the Task_Safe aspect, the compiler would
>> force the programmer to remove the Task_Safe aspect from Bar.
>
> But this rule is just wrong. Calling unsafe operation from a safe one will
> be pretty much safe in most cases. The reverse is likely wrong.

This doesn't make sense to me. There should be no such thing as a Safe 
operation that calls unsafe ones. Wouldn't that mean that the operation 
is unsafe (to use concurrently)?

>
> Compare it with protected actions. It is safe to call an operation which
> itself is not protected from a protected operation on the context of a
> protected action.

But thats only true if the operation is only ever called from within 
that same instance of the protected object (Something that could be 
difficult to know without the aspect), and that there is only one 
instance of that protected type of the protected object. Otherwise its 
not safe to call from a protected operation as there could be other 
concurrent calls calling the unsafe operation.

The following program illustrates this. If you run the program with a 
small value of N (specified on the command line), say 100, then chances 
are the program executes correctly to completion. However if you use a 
larger value of N (say 1_000_000, the default), then the program fails,
due to the use of global variables. In Test1, the Unsafe function is 
called directly from multiple tasks.

In Test2, the same Unsafe function is only called from protected 
functions, but it still fails.
.
In both tests, the failures are due to function Unsafe failing its 
Postcondition.

If the Task_Safe attribute existed, the compiler could have issued a 
warning at compile time that the tasks were calling subprograms that 
weren't Task_Safe, and the problems could have been avoided.


with Ada.Text_IO; use Ada.Text_IO;
with Ada.Exceptions; use Ada;
with Ada.Command_Line;

procedure Test_Task_Safety is

    --  Defaults to 1_000_000, but can be specified on command line
    N : constant Natural := (if Command_Line.Argument_Count >= 1 then
                             Natural'Value (Command_Line.Argument (1))
                             else 1_000_000);

    Global_Data : Integer := 0;

    function Unsafe (X : Natural) return Natural
        with Post => Unsafe'Result = X + 1 --,
         --  Task_Safe => False
        ;

    function Unsafe (X : Natural) return Natural is
    begin
       Global_Data := X;
       Global_Data := Global_Data + 1;
       return Global_Data;
    end Unsafe;

begin

    New_Line;
    Put_Line ("******************************** ");
    Put_Line ("****  Test1 : Unsafe calls ***** ");
    Put_Line ("******************************** ");
    New_Line;

    Test1 : declare

       task type T1 is
       end T1;

       task body T1 is
          Result : Natural := 0;
       begin
          for I in 1 .. N loop
             Result := Unsafe (Result);
          end loop;
          Put_Line ("Result =" & Natural'Image (Result));
       exception
          when E : others =>
             Put_Line ("Task_Died" & 
Ada.Exceptions.Exception_Information (E));
       end T1;

       Workers : array (1 .. 10) of T1;
    begin
       null;
    end Test1;

    New_Line;
    Put_Line ("********************************************************");
    Put_Line ("****  Test2 : Unsafe calls from protected objects ***** ");
    Put_Line ("********************************************************");
    New_Line;

    Test2 : declare

       protected PO1 is
          function Foo (X : Natural) return Natural;
       end PO1;

       protected PO2 is
          function Bar (X : Natural) return Natural;
       end PO2;

       protected body PO1 is
          function Foo (X : Natural) return Natural is
          begin
             return Unsafe (X);
          end Foo;
       end PO1;

       protected body PO2 is
          function Bar (X : Natural) return Natural is
          begin
             return Unsafe (X);
          end Bar;
       end PO2;

       task type T1 is
       end T1;

       task body T1 is
          Result : Natural := 0;
       begin
          for I in 1 .. N loop
             Result := PO1.Foo (Result);
          end loop;
          Put_Line ("Result =" & Natural'Image (Result));
       exception
          when E : others =>
             Put_Line ("Task_Died" & 
Ada.Exceptions.Exception_Information (E));
       end T1;

       task type T2 is
       end T2;

       task body T2 is
          Result : Natural := 0;
       begin
          for I in 1 .. N loop
             Result := PO2.Bar (Result);
          end loop;
          Put_Line ("Result =" & Natural'Image (Result));
       exception
          when E : others =>
             Put_Line ("Task_Died" & 
Ada.Exceptions.Exception_Information (E));
       end T2;

       Foo_Workers : array (1 .. 10) of T1;
       Bar_Workers : array (1 .. 10) of T2;

    begin
       null;
    end Test2;

    null;
end Test_Task_Safety;

Output:

********************************
****  Test1 : Unsafe calls *****
********************************

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Result = 1000000

********************************************************
****  Test2 : Unsafe calls from protected objects *****
********************************************************

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Result = 1000000

Brad
>
> There is no reasonable rules to verify. Safety of an operation is *not*
> related to the safety of called operations, not transitive nor
> antitransitive.
>