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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 2002:a24:1147:: with SMTP id 68-v6mr2777271itf.48.1524275430381; Fri, 20 Apr 2018 18:50:30 -0700 (PDT) X-Received: by 2002:a9d:2281:: with SMTP id y1-v6mr765167ota.14.1524275430131; Fri, 20 Apr 2018 18:50:30 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!feeder.eternal-september.org!weretis.net!feeder4.news.weretis.net!news.roellig-ltd.de!open-news-network.org!peer01.am4!peer.am4.highwinds-media.com!peer02.iad!feed-me.highwinds-media.com!news.highwinds-media.com!k65-v6no1347284ita.0!news-out.google.com!u64-v6ni2361itb.0!nntp.google.com!k65-v6no1347282ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 20 Apr 2018 18:50:29 -0700 (PDT) In-Reply-To: <87k1t1s9lx.fsf@nightsong.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=76.113.16.86; posting-account=lJ3JNwoAAAAQfH3VV9vttJLkThaxtTfC NNTP-Posting-Host: 76.113.16.86 References: <1c73f159-eae4-4ae7-a348-03964b007197@googlegroups.com> <878t9nemrl.fsf@nightsong.com> <87h8o7lowg.fsf@nightsong.com> <8736zqkwat.fsf@nightsong.com> <6839088c-f221-4650-a6ea-1841ae539486@googlegroups.com> <1e5f5681-0e2a-43cc-9437-2bd38078da08@googlegroups.com> <87604lvkqp.fsf@nightsong.com> <0bd80336-595a-45b6-b4e5-26c13d5859cb@googlegroups.com> <87o9idsh7f.fsf@nightsong.com> <87k1t1s9lx.fsf@nightsong.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: =?UTF-8?B?UmU6IEhvdyB0byBnZXQgQWRhIHRvIOKAnGNyb3NzIHRoZSBjaGFzbeKAnT8=?= From: Shark8 Injection-Date: Sat, 21 Apr 2018 01:50:30 +0000 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 10563 X-Received-Body-CRC: 1434447639 Xref: reader02.eternal-september.org comp.lang.ada:51655 Date: 2018-04-20T18:50:29-07:00 List-Id: On Friday, April 20, 2018 at 6:10:06 PM UTC-6, Paul Rubin wrote: > Shark8 writes: > >> Why do you say that? Even for ordinary testing, not extraordinary? > > Meltdown and Spectre -- which stem from caching and speculative executi= on. >=20 > What does that have to do with anything? =20 >=20 > > It's about the *properties* here, not just whether "A:=3D 1 + A;" > > correctly generates an increment, or whether it can overflow. >=20 > I can't tell what you mean by this. I may be missing something basic. What I mean by both of these is there are other items in-play, in such a co= mbined HW/SW environment, than mere "correctness". There are properties tha= t are absolutely crucial to specify and ensure: the Spectre and Meltdown bu= gs are examples of this (regarding the property of "access control" being v= iolated because of the implementation of 'caching' and 'speculative executi= on' and interactions between them). Proving properties is going to be one of the major things to allow for effi= cient parallelization, possibly chosen at runtime, to move things back to t= he realm of software. (The video https://www.infoq.com/presentations/Thinki= ng-Parallel-Programming is an excellent progression into parallelism and cu= lminates in just how important properties [algebraic in the talk, but gener= alizable] are.) >=20 > > In such an IDE the VHDL has to have some manner of proving properties; >=20 > That sounds like you're talking about proofs embedded in the VHDL code, > that prove SPARK-like VC's about the circuit being described. That's > fine and necessary. But the topic I asked about is the proofs used in > the compiler, not the proofs embedded in the compiled program. That [proof in VHDL] would be good, too. But having the compiler, the translator (VHDL-to-circuit), provable is nece= ssary in order to ensure that the circuit you get *IS* the circuit describe= d by the VHDL. Full implementation conformance to H.3.2 (Pragma Inspection_Point) and H.3.= 1 (Pragma Reviewable) of Ada requires a lot of information; and H.3.1 (13) = & (14) in particular thrust in the direction, though only requiring reporti= ng, whereas this method is fully automatable and could produce exact, prova= ble correspondence between source and object. >=20 > > Never crashing is a good thing; it's far better to have a controlled > > exit than possibly leave things in a inconsistent state. >=20 > 1. Of course it's a good thing, but is it CRITICAL? How is it not? Just because "best practices" of "the industry" says it's a-ok to have to c= lean and rebuild because the previous output was corrupted [perhaps a bad b= uild-system] somehow doesn't mean it's not critical. You have to keep rebuilding until it's *RIGHT*. (It's not hard real-time; b= ut what happens to your SW company [I'll assume a SW-dev company because th= is is C.L.A.] if you never have any runnable executable? It'll die because = it's not producing SW.) But even disregarding hypotheticals, how important is it that your tools gi= ve you the right answer? [Often, very.] Now, how important is it that the computer CPU be accurate [within its digi= tal constraints]? (Intel FP error) How about that your computer HW be correct? (Meltdown, Spectre; Phenom's TL= B; Pentium F00F) What we're talking about here is a system that produces both the software a= nd the hardware; and so in order to have any assurance that you-as-a-progra= mmer are getting what you specify (either HW or SW) as the output [if there= is any output] the system-as-a-whole should be reliable. -- And, transitiv= ely, the criticality of software and hardware that would produced is part o= f the criticality of the compiler. There are too many variables, too many outputs and possible inputs to make = such an endeavor viable with testing methodologies -- it simply doesn't sca= le -- the only way that does scale is proof: the ability to say "here are t= he properties that must hold", feed the program to your provers, and verify= that they do. If we do the above with our compiler, then we have the excellent property t= hat any modification we make to the IDE (and compiler(s)) retain the proper= ties we proved and retain their correctness and, therefore, produce correct= output. And, after producing this verified compiler, we can have full confidence in= what we compile with it is indeed what was specified -- for everything, re= gardless of its own criticality.=20 >=20 > 2. What inconsistent state is left if the compiler crashes? It's just a > usermode program. There's an error message saying that the compiler > crashed, and hopefully some diagnostic info saying how the crash > happened. Or you're left with a incorrect object. (I've had this happen, w/o an error= message; then it dissapears when you clean/rebuild.) But see above about the transitivity of criticality. >=20 > 3. There are many ways compilation can fail, even if the compiler > software is perfect, such as a power failure in the office, problems > with the computer hardware, the building being hit by a meteor or > tsunami, or the above-described mischievous billionaire showing up. At > a typical office there's maybe 1e-3 chance that one of those things > happens on a given day (the billionaire is the least likely of course), Those things are part of the variance of life and there's nothing we can do= to eliminate them [esp. in the realm of SW], but we can [and do] mitigate = them... like UPS in the case of power outage. > With a well-tested compiler (verified like CompCert, but not SPARK > verified), you have at worst 1e-6 chance of hitting an input that it > can't compile (you get an error message instead, not wrong code). Errors are fine, your compiler saying "Hey, I can only handle 128 parenthes= is nestings" or "I can't represent 2**65" or "Hey, quit feeding me crap!" -= - not that hose would be the actual error-text. But that's qualitatively different than being able to say: this code that i= s output is provably correct in translation from the input. > How much are you willing to pay to decrease the 1e-6 to 1e-10 by using > SPARK? If the amount is more than zero, what are you doing about the > 1e-3 chance of other problems? >=20 > Anyway, you have not explained how it's even conceptually possible to > write a SPARK verified Ada compiler that compiles every possible Ada > program, rather than a restricted subset. Every possible program WITHIN THE LIMITATIONS OF THE COMPUTER *AND* provabl= y correct translation. The key is in the intermediate representation -- you have the representatio= n only able to represent syntactically (and, also, ideally) semantically co= rrect Ada programs... Then you just need to prove production of the IR. (Le= t's assume that tokenizing is proved in a state-machine consuming character= s or whatever.) Lastly, you prove the code-generation of IR-to-target. Done. > If there's a VC requiring the > compiler to never use more than N bytes of memory, then what do you do > with an input that uses N+1 levels of nested parentheses (rejecting it > and printing an error message is no different than crashing and printing > an error message)? (1) I reject the idea that /CRASHING/ is at all in the same category as a c= ontrolled exit. You know the GNAT bug box? _THAT_ is a crash, you *don't* g= et the [should-be] actual error message from that. (2) Why should there be a VC for maximum memory? (3) Depending on the design, we could reduce a lot of memory usage. [There'= s a reason multiple passes were used in early resource-constrained machines= .] (4) But maybe it would be good to have an upperbound for what the compiler = proper could use. [As opposed to, say, the IDE's own implementation of prov= ers; which I imagine would only need correctness proof.] > If there's not such a VC, how can you guarantee that > your compiler never crashes from memory exhaustion? Why are you so hung up on memory exhaustion? > Really, SPARK is great, but I think I'm seeing some overreaching claims > for it in this thread. Perhaps so; but the state of the industry is shameful. I mean look at how t= he filesystem is used as an ad hoc database in programming, or build-system= s. Or the monstrosities called Continuous Integration [See the Experimental= -DB/Workspaces paper upthread]. I believe there needs to be a bigger push towards correctness, and Ada prob= ably needs a couple of good "killer apps" to really "cross the chasm", and = a proven compiler/IDE would hit the mark on both of those.