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!peer02.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post02.iad.highwinds-media.com!fx21.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> In-Reply-To: <1i6pyg077xlrv.vnwotzzgb0ut$.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: 1399724947 68.145.219.148 (Sat, 10 May 2014 12:29:07 UTC) NNTP-Posting-Date: Sat, 10 May 2014 12:29:07 UTC Date: Sat, 10 May 2014 06:30:14 -0600 X-Received-Bytes: 7599 X-Received-Body-CRC: 3978911830 Xref: news.eternal-september.org comp.lang.ada:19771 Date: 2014-05-10T06:30:14-06:00 List-Id: 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. A comment does not improve the safety of a program, only the quality of the code in the sense that uncommented code tends to be harder to read and understand. While it goes too far to say that the Task_Safe aspect would prove task safety, it would prove that the subprogram does not refer to any unprotected, non-atomic variables in a global scope. It also proves that the subprogram does not call any other subprograms that do the same. That goes a long way on the task safe spectrum If Foo calls Bar, and both Foo and Bar have the Task_Safe aspect, but some time later the maintainer of Bar decides to change its implementation to refer to some global variable or call some other subprogram that doesn't have the Task_Safe aspect, the compiler would force the programmer to remove the Task_Safe aspect from Bar. This would have a ripple effect, so that a program that calls Foo would fail compilation, and force the maintainer of Foo to remove the Task_Safe aspect on that subprogram. The maintainer of Bar would realize that he is breaking its contract, and might decide to revert his change, or choose a different implementation that allows him to leave Bar's contract intact. With comments, this would have been a maintenance hazard. It's not always obvious to a programmer when such a change is made, that it breaks such assumptions in the client usage of the subprogram. It's also error prone to expect the programmer to exhaustively examine all client usage of that subprogram to check for such assumptions that might have been broken. The maintainer of Bar might also not be aware that some of the subprograms that Bar calls have dependencies on global variables. The maintainer of Bar should not have to recursively look at the implementation of every subprogram it calls, and every subprogram those subprograms call to see if there are unsafe dependencies on unprotected global variables. Further, these aspects (Task_Safe, and Potentially_Blocking) would improve the safety of other parts of the standard. The compiler could be used in a stricter rules checking mode that forbids protected subprograms or entries from calling subprograms that are not Task_Safe, or that are Potentially_Blocking. (At the very least, the compiler could issue warnings) Rather than only relying on a run time check to raise an exception when a protected subprogram or entry calls a subprogram that blocks (possibly only in rare circumstances that might be missed during testing), it is much more likely that the problem would have been caught during compile time. Also, since the compiler cannot prove that calls to other languages such as C are not referring to variables unsafely, the Task_Safe aspect would likely forbid calls to other languages. A Task_Safe subprogram is one written in pure Ada. Some would argue that that alone says a lot about the safety quality of the subprogram. Brad >>>> it seems >>>> like a large hole that there is no way to specify the task safety in the >>>> contract as well, so I am wondering about what can be done to improve >>>> that situation. >>> >>> From the program correctness POV, yes, it is fine to provide some axioms >>> for the prover which would use them. >> >> Not just for provers, but also for human readers of the source code. It >> conveys the intent of the programmer to the reader, which might be >> another programmer who wants to use that abstraction. > > No. It is not the intent. Intent to me is about program semantics, the > meaning of the program, what the program is supposed to do. Safety or > unsafety is a usage constraint, how you should use the program in order to > retain its meaning. Safety is a constraint which, differently to > preconditions, interfaces, types of entities etc, has a nasty nature that > makes it impossible to spell in a language of Turing-complete power. > >>> But this is not the case here. In fact, proving "safety" of an operation is >>> easier than proving safety of a combination of "safe" operations. >>> >>> And you are not going to prove it to hold, as a contract must do. Not even >>> to check it at run-time, to annoy the programmer, as Ada 2012 "contracts" >>> do. >> >> I think it could be a static check, done at compile time, so it'd be >> similar to a Static_Predicate check, which is another form of contract. >> And like a type invariant, which is another form of contract, it doesn't >> "prove" that the invariant can never be false, but it would do >> a reasonable amount of checking to catch hopefully most problems, and it >> captures the intent of the programmer. > > No. > > Ada 2012 "dynamic invariant" (which is not an invariant, but an arbitrary > expression) is *computable*. > > Invariant proper is *provable*. > > Task safety is neither computable nor provable. The only way of ensuring > task safety is per construction, when you would prove, usually using more > powerful apparatus than machine prover (i.e. with pen and paper) that given > method of construction yields safety under specified conditions. >