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: 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!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: Mon, 12 May 2014 10:13:05 +0200 Organization: cbb software GmbH Message-ID: <1qq0ryc8c4l2m.1driqwwiwwl02.dlg@40tude.net> 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: QTaafVZuunHujkJPndFR7g.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 Xref: news.eternal-september.org comp.lang.ada:19782 Date: 2014-05-12T10:13:05+02:00 List-Id: On Sun, 11 May 2014 12:01:20 -0600, Brad Moore wrote: > On 10/05/2014 2:27 PM, Dmitry A. Kazakov wrote: >> On Sat, 10 May 2014 06:30:14 -0600, Brad Moore wrote: >> >>> On 09/05/2014 1:00 PM, Dmitry A. Kazakov wrote: >>>> On Fri, 09 May 2014 07:14:09 -0600, Brad Moore wrote: >>>> >>>>> On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote: >>>> >>>>>> To me description that does not prescribe is a lie. >>>>> >>>>> It is true that the Task_Safe aspect would be prescribing some >>>>> restrictions that are meant to enforce the intent as best as possible, >>>>> but it also documents the intent of the programmer. So to be more >>>>> precise, the Task_Safe mechanism doesn't prescribe a specific >>>>> implementation for the programmer. It only prescribes that whatever >>>>> implementation the programmer chooses, it should be task safe. >>>> >>>> In other words is a comment. I prefer old -- -style comments. >>> >>> It'd be far, far better than a comment, in my mind. A comment doesn't >>> cause compilations to fail. >> >> Neither the aspect should, because, as I said, neither task-safety nor >> unsafety follows from safety of called operations. > >> There is no reasonable rules to verify. Safety of an operation is *not* >> related to the safety of called operations, not transitive nor >> antitransitive. > > A couple more thoughts and refinements to throw in, for consideration. > > This got me thinking about what could be done to be able to say with > more confidence that a Task_Safe subprogram is in fact task safe (i.e > Safe to call concurrently). > > What if we threw in a couple more restrictions. > > - A Task_Safe subprogram does not contain any backwards jumping goto > statements, nor does it contain while loops. (Or at least while loops > that cannot be easily proven to be guaranteed to exit. For loops however > are OK, since they are guaranteed to exit) > > - A subprogram that does contain backwards jumping goto statements or > while loops are considered to be potentially blocking, for the purpose > of the Potentially_Blocking aspect, so applying the Potentially_Blocking > aspect to such a subprogram would be allowed. > > It would be OK for the main body of a task to have while loops of > course. The compiler would just statically warn about calling > subprograms that have while loops. > > Now it seems to me that when we say Task_Safe, it is more than just > documenting the intent of the programmer, it is provable. > > Such a subprogram for example could not deadlock because it does not > contain any endless loops, and does not call anything that blocks. It > also does not refer to any global variables. > > With such restrictions, can you provide any example that you would > consider unsafe? I am having difficulty coming up with one. This looks a useless subprogram to me. 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. 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de