Re: Safety of unprotected concurrent operations on constant objects

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Mon, 12 May 2014 22:50:03 -0600, Brad Moore wrote:

> I lumped task safe programs with while loops into the 
> Potentially_Blocking category, because while loops can be used to 
> implement busy spin-loops, which can be considered a form of blocking.

Loops are used in many (if not most) lock-free algorithms. They have
bounded time, because the loop condition is that the task has been
preempted during execution of the loop body, which may happen only once,
provided scheduling is any reasonable.

>> What I had in mind are designs like:
>>
>> type T is record
>>     M : aliased Mutex;
>>     ...
>> end record;
>>
>> A safe operation on this type looks like:
>>
>>     procedure Safe_Search (X : in out T; ...) is
>>         Lock : Holder (T.M'Access);
>>     begin
>>         Unsafe_Search (X, ...);
>>     end Safe_Search;
>>
>> Here safe operations call to unsafe ones all the time and never do each
>> other because M is not reeentrant.
> 
> Thanks for the example. A good case to consider. By the rules I'm 
> thinking of, this would not be a task-safe construct however, which I 
> think is rightly so.
> 
> The Task_Safe attribute is about subprograms that can be proven to be 
> safe. This construct is unsafe, because it doesn't guarantee that there 
> aren't direct concurrent calls to Unsafe_Search happening while inside 
> the body of Safe_Search. (It would probably be too difficult to prove, 
> and so its better to assume the worst, when it comes to safety.) 
> Therefore Safe_Search is also not a task-safe call.

This is why I consider these attributes useless as they would work for
marginal cases only.

[...]

The rules you are proposing seem to me focusing on rather atomicity than
task safety.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de