Re: Safety of unprotected concurrent operations on constant objects

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

On 09/05/2014 1:00 PM, Dmitry A. Kazakov wrote:
> On Fri, 09 May 2014 07:14:09 -0600, Brad Moore wrote:
>
>> On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote:
>
>>> 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.
>
> In other words is a comment. I prefer old -- -style comments.
>

It'd be far, far better than a comment, in my mind. A comment doesn't 
cause compilations to fail. A comment does not improve the safety of a 
program, only the quality of the code in the sense that uncommented code 
tends to be harder to read and understand.

While it goes too far to say that the Task_Safe aspect would prove task 
safety, it would prove that the subprogram does not refer to any 
unprotected, non-atomic variables in a global scope. It also proves that 
the subprogram does not call any other subprograms that do the same. 
That goes a long way on the task safe spectrum

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. This would 
have a ripple effect, so that a program that calls Foo would fail 
compilation, and force the maintainer of Foo to remove the Task_Safe 
aspect on that subprogram. The maintainer of Bar would realize that he 
is breaking its contract, and might decide to revert his change, or 
choose a different implementation that allows him to leave Bar's 
contract intact. With comments, this would have been a maintenance 
hazard. It's not always obvious to a programmer when such a change is 
made, that it breaks such assumptions in the client usage of the 
subprogram. It's also error prone to expect the programmer to 
exhaustively examine all client usage of that subprogram to check for 
such assumptions that might have been broken.

The maintainer of Bar might also not be aware that some of the 
subprograms that Bar calls have dependencies on global variables.
The maintainer of Bar should not have to recursively look at the 
implementation of every subprogram it calls, and every subprogram those 
subprograms call to see if there are unsafe dependencies on unprotected 
global variables.

Further, these aspects (Task_Safe, and Potentially_Blocking) would
improve the safety of other parts of the standard.

The compiler could be used in a stricter rules checking mode that 
forbids protected subprograms or entries from calling subprograms that 
are not Task_Safe, or that are Potentially_Blocking. (At the very least, 
the compiler could issue warnings)

Rather than only relying on a run time check to raise an exception when 
a protected subprogram or entry calls a subprogram that blocks (possibly 
only in rare circumstances that might be missed during testing), it is 
much more likely that the problem would have been caught during compile 
time.

Also, since the compiler cannot prove that calls to other languages such 
as C are not referring to variables unsafely, the Task_Safe aspect would 
likely forbid calls to other languages. A Task_Safe subprogram is one 
written in pure Ada. Some would argue that that alone says a lot about 
the safety quality of the subprogram.

Brad

>>>> 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.
>
> No. It is not the intent. Intent to me is about program semantics, the
> meaning of the program, what the program is supposed to do. Safety or
> unsafety is a usage constraint, how you should use the program in order to
> retain its meaning. Safety is a constraint which, differently to
> preconditions, interfaces, types of entities etc, has a nasty nature that
> makes it impossible to spell in a language of Turing-complete power.
>
>>> 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.
>
> No.
>
> Ada 2012 "dynamic invariant" (which is not an invariant, but an arbitrary
> expression) is *computable*.
>
> Invariant proper is *provable*.
>
> Task safety is neither computable nor provable. The only way of ensuring
> task safety is per construction, when you would prove, usually using more
> powerful apparatus than machine prover (i.e. with pen and paper) that given
> method of construction yields safety under specified conditions.
>