Re: Safety of unprotected concurrent operations on constant objects

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

On 10/05/2014 2:27 PM, Dmitry A. Kazakov wrote:
> On Sat, 10 May 2014 06:30:14 -0600, Brad Moore wrote:
>
>> 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.
>
> Neither the aspect should, because, as I said, neither task-safety nor
> unsafety follows from safety of called operations.
>

> There is no reasonable rules to verify. Safety of an operation is *not*
> related to the safety of called operations, not transitive nor
> antitransitive.
>

A couple more thoughts and refinements to throw in, for consideration.

This got me thinking about what could be done to be able to say with 
more confidence that a Task_Safe subprogram is in fact task safe (i.e 
Safe to call concurrently).

What if we threw in a couple more restrictions.

- A Task_Safe subprogram does not contain any backwards jumping goto 
statements, nor does it contain while loops. (Or at least while loops 
that cannot be easily proven to be guaranteed to exit. For loops however 
are OK, since they are guaranteed to exit)

- A subprogram that does contain backwards jumping goto statements or 
while loops are considered to be potentially blocking, for the purpose 
of the Potentially_Blocking aspect, so applying the Potentially_Blocking 
aspect to such a subprogram would be allowed.

It would be OK for the main body of a task to have while loops of 
course. The compiler would just statically warn about calling 
subprograms that have while loops.

Now it seems to me that when we say Task_Safe, it is more than just 
documenting the intent of the programmer, it is provable.

Such a subprogram for example could not deadlock because it does not 
contain any endless loops, and does not call anything that blocks. It 
also does not refer to any global variables.

With such restrictions, can you provide any example that you would 
consider unsafe? I am having difficulty coming up with one.

Keep in mind also that Task_Safe is not a term defined in the RM. We can 
pretty much define it to mean whatever we want, including something that 
is provable.

Regards,
Brad