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 X-Received: by 10.236.112.12 with SMTP id x12mr5098571yhg.56.1399956603646; Mon, 12 May 2014 21:50:03 -0700 (PDT) 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!news.bbs-scene.org!border4.nntp.dca.giganews.com!backlog4.nntp.dca3.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!hw13no2923117qab.0!news-out.google.com!du2ni3053qab.0!nntp.google.com!peer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post01.iad.highwinds-media.com!fx11.iad.POSTED!not-for-mail From: Brad Moore User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.5.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Safety of unprotected concurrent operations on constant objects References: <6c2cd5d4-a44c-4c18-81a3-a0e87d25cd9e@googlegroups.com> <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> In-Reply-To: <1qq0ryc8c4l2m.1driqwwiwwl02.dlg@40tude.net> Message-ID: <%vhcv.255737$s87.168969@fx11.iad> NNTP-Posting-Host: 68.145.219.148 X-Complaints-To: internet.abuse@sjrb.ca X-Trace: 1399956603 68.145.219.148 (Tue, 13 May 2014 04:50:03 UTC) NNTP-Posting-Date: Tue, 13 May 2014 04:50:03 UTC Date: Mon, 12 May 2014 22:50:03 -0600 X-Received-Bytes: 4541 X-Received-Body-CRC: 1707689584 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Original-Bytes: 4919 Xref: news.eternal-september.org comp.lang.ada:19794 Date: 2014-05-12T22:50:03-06:00 List-Id: On 14-05-12 02:13 AM, Dmitry A. Kazakov wrote: > As a side note safety is not about > halting or time constraints. A never ending subprogram could be still safe. > Overstretching this a bit, a task body running infinite loop is task-safe. Right. And that would still be the case by the rules I have been suggesting. (Note the distinction between "task safe" proper and Task_Safe the aspect, with an underscore.) The idea is that subprograms that have either Task_Safe or Potentially_Blocking aspects are task safe. 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. > > 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. Another rule I haven't stated is that any subroutine that modifies a variable (or internal state) that isn't via a protected object, atomic, or volatile and a type that can be atomically updated (such as Integer), is not Task_Safe. This would only need to be checked directly in the body of the task-safe subprogram, since any subprograms called by that subprogram also need to be Task_Safe, and would have been checked during their compilation. So for example, a spinloop on a regular integer would not be considered Task_Safe, but a spinloop on a volatile integer would be considered task safe (assuming there were no other rule violations). The rules are meant to be static checks, that are relatively easy to implement (I hope) and they shouldn't introduce any run-time overhead. They would only generate a compiler warning or suppressable error. (i.e No runtime exception) So such a construct as you have above wouldn't be disallowed. It'd only be that in a mode of stricter checking, the programmer would need to suppress the warning or error and indicate that the usage is OK.