Re: Safety of unprotected concurrent operations on constant objects

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

On 05/05/2014 10:36 AM, Dmitry A. Kazakov wrote:
> On Mon, 05 May 2014 09:11:05 -0600, Brad Moore wrote:
>
>> Eg. For Ada.Containers.Vectors...
>>
>> type Vector is tagged private
>>      with
>>         Constant_Indexing => Constant_Reference,
>>         Variable_Indexing => Reference,
>>         Default_Iterator  => Iterate,
>>         Iterator_Element  => Element_Type,
>>         Task_Safe         => False;
>>
>> Then programmers could apply the aspect to their own abstractions, which
>> better defines the contract of the subprogram or type.
>
> Task safety is not a type property. Even for a tagged type an unsafe
> operation can be defined later on. For non-tagged types it is even less
> clear which operations must be safe and which not.
>
> Furthermore, task-safety cannot be inherited or composed. At least not
> without massive overhead to prevent deadlocking when two safe types meet as
> mutable parameters of a safe subprogram.

I agree that such a property is not likely inheritable or composable, 
and I don't think we'd want it to be.  I think conceivably it could 
apply to a type, however. It may be that such an aspect could only be 
applicable to tagged types, and only would apply to the primitive 
subprograms of that type. The aspect, if true would become false for any 
derivations of that type, unless those derived types also explicitly set 
the aspect to True.

  If such an aspect were explicitly specified as false for the standard 
containers, for instance, it would pretty much describe
the state of affairs today that have been mentioned in this thread,
but hopefully more obvious to the user. That is, you really cant count 
on any of the subprograms in the containers as being task safe, even 
though some of them may be in a given implementation.

However, it might make sense to specify certain primitive subprograms of 
a type as being task safe. For instance, the Element subprogram of the 
Ada.Containers.Vectors is task safe in the current GNAT implementation. 
If that subprogram were to have the aspect specified as True in some 
future version of Ada, then users of that container would at least know 
that particular call is guaranteed to be task safe by its contract. This 
should be fairly straight forward for similar calls that do not modify 
the container or the elements of the container.

It gets trickier for subprograms that do modify the object, such as the 
Replace_Element subprogram of Ada.Containers.Vectors. That call is 
currently task safe in GNAT, so long as two tasks do not attempt to 
replace the same element.The usage of the container object in that call 
itself is task safe, as it does not modify state global to the container 
object, but the elements contained in the container are not task safe. 
So if we wanted to specify concurrent usage for such a subprogram, maybe 
you'd need two aspects; Task_Safe, and Task_Safe_Components.

    procedure Replace_Element
      (Container : in out Vector;
       Index     : Index_Type;
       New_Item  : Element_Type)
      with Task_Safe=>True,
           Task_Safe_Components => False;

>
> And, just how this contract is supposed to be verified?
>

I see it more as a contract or promise made by the implementer to the 
users of that subprogram that concurrent calls to the subprogram will 
work. In other words, the implementer has designed the call to be task 
safe, using whatever means, and has committed to keep the call task safe 
in the future, by having that property associated with the subprogram 
specification.

At this point, I have doubts that the compiler could 100% guarantee that 
a subprogram call is task safe, but there are likely rules and
restrictions that could be applied that would allow the compiler to 
catch many problems.

In particular, the aspect could restrict the associated subprogram to
disallow:

(1) Calls on other non-protected subprograms that are not Pure or
     Task_Safe;

(2) Dependence on global variables that are neither atomic nor task nor
     protected.

These would be static checks that could be applied at compile time.