Re: Safety of unprotected concurrent operations on constant objects

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

On 14-05-13 02:27 PM, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:1tb8my720vum2$.r9u7r03btzqm.dlg@40tude.net...
> ...
>>> I think most protected objects typically do not call unsafe subprograms.
>>
>> They do. It is an unrelated case, as I said, task safety needs to support
>> blocking, but still it is a usable pattern, that is to pass an unsafe
>> operation to a protected object's entry in order to execute it on the
>> context of a protected action.
>
> I don't think you guys are even talking about the same problem. Brad's
> Task_Sfae idea (which is similar to an idea I had years ago is aimed at
> providing idiot-proof concurrency. This is necessarily going to be a rather
> small subset of all of the possibilities of concurrency. Ada surely does not
> need new ways to do complex concurrency; it has lots of ways to shoot
> yourself in the foot now, and all of the flexibility one could possibly
> want.

Agreed. The Aspects I had in mind are not about coming up with new ways 
of doing concurrency, only about presenting a better picture to the 
client of the subroutine (both the compiler and the programmer), so that 
programmers can make use of concurrency or parallelism hopefully with 
less chance of shooting themselves in the foot. (i.e more safely)

>
> But for a lot of problems, bog-simple parallel execution of code is enough,
> and for that, one wants to allow a very restricted set of operations which
> prevent trouble by construction. That's the purpose of Task_Safe and similar
> ideas.

Right.

>
> In the long run, the Ada has to have an easier way to construct parallel
> programs. Raw tasks are pretty much like programming in C, given the lack of
> any protection from making mistakes -- it's not at all like Ada in other
> areas. Whether one can do everything that they might want safely is not
> relevant.
>
> Something like Task_Safe can be very restrictive, simply because one can
> always write separate tasks if they need something more complex. It
> certainly don't have to allow everything.

And also the use of Task_Safe is optional. If one wants to work in a 
less restrictive environment, they dont have to use the aspect.

>
>> In any case, before messing up with attributes we should IMO concentrate
>> efforts on integrating SPARK into Ada and having language mandated provers
>> and language infrastructure supporting provers on programmer's demand,
>> like
>> proper pre-/postconditions, axioms etc. Once this is in place and working
>> we could start thinking how to formalize concurrency aspects within this
>> framework. Otherwise it is putting the cart before the horse.
>
> I'm hestitant to say "never", but I think it is highly unlikely that Ada
> (the programming language) will ever include any proof technology. That's
> because it's simply too difficult to formally describe the rules involved.
> Even relatively simple rules (such as errors for always out of range values)
> are too hard to add to Ada without pages of rules or far too many false
> positives (or usually both).

And to be clear, when I mention proving task safety with these aspects, 
I do not mean formal proof or mathematical proof. I only mean in an 
informal manner that allows us to reason, similar to how applying pragma 
Pure to a package spec allows us to reason that the subprograms in such 
a package are safe for remote subprogram usage with the distributed 
annex. The public (visible) view of Pure on a package means the compiler 
of a client unit does not need to look into the implementation of the 
Pure package, since it knows the rules of pragma Pure have been applied 
to that package.

Brad
>
> If one doesn't formally describe the rules (what must and most not be
> detected), then all Ada portability is lost. In such a case, no language
> standard is needed at all (it's only real purpose is to provide an avenue
> for portability between implemetations).
>
> With Ada 2012, we provided a framework for contracts. We have to enforce
> those at runtime in the language definition because no other solution is
> practically possible. But one hopes that implementations take those further
> and provide mechanisms to use those contracts in proof settings.
>
> Certainly, future versions of Ada can add things that will provide
> additional help (exception contracts are near the top of the list, IMHO),
> but I don't think that we can do much to mandate proof. (Besides, I think
> that mandating proof would have the effect of driving all Ada vendors other
> than AdaCore out of the Ada business -- I very much doubt that any of the
> other compiler vendors could afford the investment. Perhaps that will happen
> anyway, given the slow uptake of Ada 2012 by other vendors.)
>
>                                                Randy.
>
>