Re: Safety of unprotected concurrent operations on constant objects

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

On 14-05-07 11:03 PM, Brad Moore wrote:
> On 06/05/2014 1:07 PM, Dmitry A. Kazakov wrote:
>> On Tue, 06 May 2014 12:22:59 -0400, Robert A Duff wrote:
>>
>>> Brad Moore <brad.moore@shaw.ca> writes:
>>>
>>>> However, it might make sense to specify certain primitive
>>>> subprograms of
>>>> a type as being task safe.
>>>
>>> What exactly do you mean by "task safe", either for a type, or for
>>> a subprogram?  E.g. if Element is task safe, does that mean calls
>>> to Element are atomic with respect to each other?
>>
>> It means, in my interpretation, that the post-condition of the operation
>> [and the object's invariant] is true for any number of tasks Wi
>> calling the
>> operation independently at any point Ti of real-time.
>
> That's a nice definition. It does cover a broad set of cases including
> pure functions, protected operations, sets of function calls whose
> parameters do not conflict, mutex guarded calls, etc.
>
>
>>
>>> If both Element
>>> and Replace_Element are task safe, does that mean calls to Element
>>> and Replace_Element are atomic; i.e. if one task calls Element,
>>> and another calls Replace_Element, those two calls are serialized?
>>
>> No. It could be atomic in order to ensure the post-condition.
>>
>>> Why primitive subprograms?  What about class-wide subprograms
>>> declared in the same package?
>
> As explained in another email, I was worried about non-tagged types.
> eg.
>     type T is record ... end record with Task_Safe => True;
>     type U is record ... end record with Task_Safe => False;
>
>     function Bar (X1 : T; X2 : U) return Integer;
>
>     It might be confusing or onerous for the reader to determine if Bar
>     is task safe or not, particularly if there is a long list of
>     parameters.
>
> I think Class-wide subprograms declared in the same package however
> could probably be lumped in with the primitive functions, and the aspect
> could apply to those as well..
>
>
>>
>> That was my question too. Presumably, primitive operations were
>> considered
>> building blocks for class-wide operations, which, under this assumption,
>> would be safe per design for some, rather, weak [as you pointed below]
>> post-conditions.
>>
>>> Does task safety imply absence of deadlock?
>>
>> Pragmatically, the answer could be no, if more than one object involved.
>> Yes, for single object.
>>
>> Safety of any subset of a set of objects is stronger than safety of
>> individual objects.
>>
>
> It would be nice if it could imply the absence of deadlock, but I think
> that might be too lofty a goal.
>
>>> Suppose we have an atomic increment function (calls to it are
>>> serialized), and Counter is initially 0, and one task does
>>> "X := Incr (Counter);" and another task does "Y := Incr (Counter);".
>>> A third task waits for those two to terminate, and then calls
>>> procedure P, which prints X followed by Y.  Is P task safe?
>>
>> See above, that depends on the post-condition of P.
>
> I think non-determinism is a different property that is independent of
> task safety. There is no reason to believe P is incorrect. It may very
> well satisfy it's post-condition. as Dmitry says.
>
>>
>>> I understand task safety in an informal way, but I'm not sure
>>> how to decribe it formally.  And if the definition depends on
>>> the intent of the programmer (perhaps expressed in comments),
>>> we can't expect a compiler to check it.  ;-)
>>
>> Right. Minimally, the semantics must be stated formally using pre- and
>> post-conditions.
>>
>
> Even without a formal definition of task safety, the compiler could
> check that a task safe subprogram only calls other task safe
> subprograms.  (Subprograms that have been explicitly marked by the
> subprogrammer as being task safe). That'd be a good start actually.
>
> But I think it would be better if the compiler could provide more safety.
>
> A task safe call should probably not be a potentially blocking call, I
> think.
>
> A task safe subprogram should also not modify global variables that
> aren't protected, or atomic.
>
> This would add quite a bit of safety, I think but maybe there are other
> restrictions that could be added also.

Actually, I have second thoughts about disallowing calls to entries from 
a "task_safe" subprogram. It should be allowed, as the rules about 
potentially blocking operations would help prevent calling an entry from 
another entry.

But I think the idea could be carried further. Another property of a 
subprogram that is important to know is whether it is a blocking call or 
not. That is another attribute that would be nice to capture in the 
contract. I think it would be useful to have a Blocking aspect that 
could be similarly applied to a subprogram specification.

I see it working something like the following;

- A Blocking call is viewed conceptually as being a Task Safe call (as 
it should). It is a more specific kind of a task safe call.

- The Blocking aspect may be optionally applied to any subprogram, 
whether it is actually blocking or not. If the subprogram is not 
blocking, it might mean that the programmer is reserving the right to 
make it a blocking call in the future, or that other implementations of 
the specification might be blocking.

- If a subprogram directly has task or protected object entry calls, 
then it cannot be explicitly specified as having the Task_Safe aspect. 
It must instead be specified as having the Blocking aspect. 
(Alternatively the subprogram can be left without any aspect 
specification. It is only used if the programmer wants to capture these 
details in the contract of the subprogram, but then the subprogram is 
not Task Safe, i.e. the Task_Safe aspect is false)

- A Task Safe program can only call other Task_Safe subprograms or 
Blocking subprograms. If the Task_Safe subprogram calls a Blocking 
Subprogram, then it cannot be explicitly specified as having the 
Task_Safe aspect. It must instead have the Blocking Aspect specified.
(or no aspect specification, or specified as false meaning that the 
subprogram is not Task Safe, i.e. the Task_Safe aspect is false)

-- Examples
function Foo return Integer with Blocking;
function Bar return Integer with Task_Safe;

Bar cannot call Foo, unless the specification is modified to either;
    function Bar return Integer with Blocking
or
    function Bar return Integer with Task_Safe => False;
(or)
    function Bar return Integer;

Regards,
Brad