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!news.glorb.com!peer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post01.iad.highwinds-media.com!fx02.iad.POSTED!not-for-mail From: Brad Moore User-Agent: Mozilla/5.0 (Windows NT 6.1; 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: <7403d130-8b42-43cd-a0f1-53ba34b46141@googlegroups.com> <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> In-Reply-To: <10pk27v48vhcb$.1qkf6roq2yzjn$.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: NNTP-Posting-Host: 68.145.219.148 X-Complaints-To: internet.abuse@sjrb.ca X-Trace: 1399831281 68.145.219.148 (Sun, 11 May 2014 18:01:21 UTC) NNTP-Posting-Date: Sun, 11 May 2014 18:01:21 UTC Date: Sun, 11 May 2014 12:01:20 -0600 X-Received-Bytes: 4588 X-Received-Body-CRC: 2117187895 Xref: news.eternal-september.org comp.lang.ada:19775 Date: 2014-05-11T12:01:20-06:00 List-Id: 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. Keep in mind also that Task_Safe is not a term defined in the RM. We can pretty much define it to mean whatever we want, including something that is provable. Regards, Brad