Re: Safety of unprotected concurrent operations on constant objects

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

On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote:
> On Wed, 07 May 2014 22:12:13 -0600, Brad Moore wrote:
>
>> On 06/05/2014 2:11 AM, Dmitry A. Kazakov wrote:
>>> On Tue, 06 May 2014 00:00:40 -0600, Brad Moore wrote:
>>>
>>>> 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 you limit it to primitive operations then much simpler to do this:
>>>
>>>      type My_Container is tagged ...; -- All operations are unsafe
>>>
>>>      type My_Safe_Container is protected new My_Container with null record;
>>
>> There's quite a difference from what you propose and what I was
>> suggesting. In a nutshell, your idea is to *prescribe* an implementation
>> (by wrapping an existing implementation in mutexes, whereas my wish is
>> to be better able to *describe* an implementation.
>
> To me description that does not prescribe is a lie.

It is true that the Task_Safe aspect would be prescribing some 
restrictions that are meant to enforce the intent as best as possible, 
but it also documents the intent of the programmer. So to be more 
precise, the Task_Safe mechanism doesn't prescribe a specific 
implementation for the programmer. It only prescribes that whatever 
implementation the programmer chooses, it should be task safe.

The "new protected" feature you described, if it were implemented would 
be one possible implementation the programmer could choose, of many.

>
>> Now that Ada has the new contract capabilities in Ada 2012,
>
> You know what I think about these...
>

I take it that you're not a fan of these, but I think there are lots of 
fans out there. In that regard, it's good that contracts aren't mandatory.
If you don't like them, you don't have to use them.


>> it seems
>> like a large hole that there is no way to specify the task safety in the
>> contract as well, so I am wondering about what can be done to improve
>> that situation.
>
>  From the program correctness POV, yes, it is fine to provide some axioms
> for the prover which would use them.

Not just for provers, but also for human readers of the source code. It 
conveys the intent of the programmer to the reader, which might be 
another programmer who wants to use that abstraction.

>
> But this is not the case here. In fact, proving "safety" of an operation is
> easier than proving safety of a combination of "safe" operations.
>
> And you are not going to prove it to hold, as a contract must do. Not even
> to check it at run-time, to annoy the programmer, as Ada 2012 "contracts"
> do.

I think it could be a static check, done at compile time, so it'd be 
similar to a Static_Predicate check, which is another form of contract.
And like a type invariant, which is another form of contract, it doesn't 
"prove" that the invariant can never be false, but it would do
a reasonable amount of checking to catch hopefully most problems, and it
captures the intent of the programmer.

>
>> For example, someone interested in processing a Vector container in
>> parallel would likely not want to use such a feature, because it applies
>> a mutex to every access to the container, when a much more efficient
>> implementation would break the index range into chunks, and
>> a group of worker tasks could process each chunk of the array without
>> any synchronization.
>
> Right, that is a common method, with read-write mutexes used.
>
> Though note, this as well applies to the container library in general. In
> such an application you would not use standard library Vector anyway.
> Because fine-grained locking would not work, while more coarse and
> efficient locking will require interaction with the container inner
> architecture and outer interface.
>
> If you accept language-provided containers without much consideration, you
> can also accept the proposed way to make them kind of safe.
>
>> A worry I'd have is that such a feature might encourage programmers to
>> become lazy and start writing poorer abstractions in lieu of taking the
>> time to write a better one, in respect to functionality, readability,
>> safety, etc.
>
> Yes. As I said, I would prefer delegation support over a specific case of
> compiler-generated wrappers.

Probably an idea that should be explored...

>
>>>> 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;
>>>
>>> But calling a task-safe subprogram from another task-safe subprogram were a
>>> much bigger problem than calling a non-safe subprogram. Protected
>>> operations specifically forbid to do exactly this.
>>
>> That's not correct. Protected procedure's and protected functions are
>> not potentially blocking. A protected procedure of one PO can call
>> another protected procedure of another PO.
>
> I meant 9.5.1 (15). The rationale to have it, IMO, was to ease
> implementations not to care about deadlocks upon locking multiple mutexes.
>
> Same problems will arise when composing task-safe operations. Surely there
> are means to prevent deadlocking whenever the synchronization is done per
> mutexes or per monitors, but these means are not for free.
>
>>> The rules you propose actually are good only for lock-free concurrency.
>>
>> There's million's of simple functions and procedures that do not involve
>> any locking. Integer "+" for example, is completely task safe.
>
> Maybe yes, maybe no. E.g. purely theoretically, consider 64-bit integer "+"
> on i686 in 32-bit mode. The implementation could use movq instruction and
> alike which in turn would have effect on the FPU (turning it off). It will
> restore FPU state upon return, but that would make it unsafe.
>
> In other subthread Randy provided a real-life story for integer "/".
>
>>> Unfortunately only few things can be done lock-free, and most types of
>>> containers certainly not.
>>
>> Containers maybe not in general, but a constant container object without
>> tamper checks could easily be made to be task safe, for functions that
>> query the container, as per the original OP's request.
>
> Yes, but this a very rare scenario (static container), which does not
> deserve special treatment.
>