From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!gandalf.srv.welterde.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Safety of unprotected concurrent operations on constant objects Date: Tue, 13 May 2014 15:27:02 -0500 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <83ha6vuynrzs.1jk08faxb8mnl.dlg@40tude.net> <1jebi7cf92ak4.1trmstj8qi3wm.dlg@40tude.net> <1i6pyg077xlrv.vnwotzzgb0ut$.dlg@40tude.net> <10pk27v48vhcb$.1qkf6roq2yzjn$.dlg@40tude.net> <1qq0ryc8c4l2m.1driqwwiwwl02.dlg@40tude.net> <%vhcv.255737$s87.168969@fx11.iad> <1tb8my720vum2$.r9u7r03btzqm.dlg@40tude.net> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1400012823 21085 69.95.181.76 (13 May 2014 20:27:03 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 13 May 2014 20:27:03 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:19813 Date: 2014-05-13T15:27:02-05:00 List-Id: "Dmitry A. Kazakov" 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.