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: backlog4.nntp.dca3.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!goblin3!goblin2!goblin.stu.neva.ru!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: Fri, 9 May 2014 21:00:36 +0200 Organization: cbb software GmbH Message-ID: <1i6pyg077xlrv.vnwotzzgb0ut$.dlg@40tude.net> 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> 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 Xref: number.nntp.dca.giganews.com comp.lang.ada:186338 Date: 2014-05-09T21:00:36+02:00 List-Id: 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 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de