Re: Safety of unprotected concurrent operations on constant objects

["Randy Brukardt" <randy@rrsoftware.com>]

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

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.

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.

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

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.