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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 Path: border2.nntp.dca3.giganews.com!backlog4.nntp.dca3.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newspeer1.nac.net!newsfeed.xs4all.nl!newsfeed2a.news.xs4all.nl!xs4all!news.stack.nl!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Safety of unprotected concurrent operations on constant objects Date: Tue, 13 May 2014 18:08:46 +0200 Organization: cbb software GmbH Message-ID: <1tb8my720vum2$.r9u7r03btzqm.dlg@40tude.net> 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: AuYlnUSfTZrfhAkRjyySpQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 X-Original-Bytes: 5867 Xref: number.nntp.dca.giganews.com comp.lang.ada:186384 Date: 2014-05-13T18:08:46+02:00 List-Id: On Tue, 13 May 2014 09:01:44 -0600, Brad Moore wrote: > On 14-05-13 02:56 AM, Dmitry A. Kazakov wrote: >> On Mon, 12 May 2014 22:50:03 -0600, Brad Moore wrote: >> >>> I lumped task safe programs with while loops into the >>> Potentially_Blocking category, because while loops can be used to >>> implement busy spin-loops, which can be considered a form of blocking. >> >> Loops are used in many (if not most) lock-free algorithms. They have >> bounded time, because the loop condition is that the task has been >> preempted during execution of the loop body, which may happen only once, >> provided scheduling is any reasonable. >> >>>> What I had in mind are designs like: >>>> >>>> type T is record >>>> M : aliased Mutex; >>>> ... >>>> end record; >>>> >>>> A safe operation on this type looks like: >>>> >>>> procedure Safe_Search (X : in out T; ...) is >>>> Lock : Holder (T.M'Access); >>>> begin >>>> Unsafe_Search (X, ...); >>>> end Safe_Search; >>>> >>>> Here safe operations call to unsafe ones all the time and never do each >>>> other because M is not reeentrant. >>> >>> Thanks for the example. A good case to consider. By the rules I'm >>> thinking of, this would not be a task-safe construct however, which I >>> think is rightly so. >>> >>> The Task_Safe attribute is about subprograms that can be proven to be >>> safe. This construct is unsafe, because it doesn't guarantee that there >>> aren't direct concurrent calls to Unsafe_Search happening while inside >>> the body of Safe_Search. (It would probably be too difficult to prove, >>> and so its better to assume the worst, when it comes to safety.) >>> Therefore Safe_Search is also not a task-safe call. >> >> This is why I consider these attributes useless as they would work for >> marginal cases only. > > I think most of the code out there that was written for concurrency > would probably satisfy the rules. (i.e. It doesn't seem marginal to me) > In the case of your example, it likely could be made to satisfy the > rules with some simple adjustments. > > For example, you could fold the body of Unsafe_Search into the body of > Safe_Search. Then you would be guaranteeing that there would be no way > to circumvent the lock, as there is only the one entry point to your > function. Your mutex lock function could then have the Task_Safe aspect. > > Another approach would be to put the body of Unsafe_Search inside a > protected object, again guaranteeing that there is no way to circumvent > the protection. No, that does not look the way it is usually used. Typically the unsafe operation is really unsafe, e.g. it does I/O, communicates with a DB and blocks as much as can it be. It is certainly not for a protected action and certainly cannot be looked inside or is too complex for analysis. > 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 am using it this pattern in order to circumvent Ada's deficiency that protected objects cannot be inherited from. This looks the only way to implement an extendable a safe object. It is by delegating public operations to protected actions of some private protected object. Extension is achieved by passing an access to procedure to an entry point of this private object. Of course you could prove nothing useful about this pattern with your rules, in most case. 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de