Re: Safety of unprotected concurrent operations on constant objects

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

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 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. 

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