Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.arch.embedded > #28032
| Subject | Re: arm-gcc: pointer to constant string |
|---|---|
| Newsgroups | comp.arch.embedded |
| References | (11 earlier) <3ranD.175206$_V.125892@fx32.am4> <%xknD.109563$tK2.88866@fx42.iad> <uPnnD.241275$l21.134548@fx46.am4> <F5qnD.17687$oH2.2568@fx10.iad> <O4rnD.458658$T%2.115904@fx06.am4> |
| From | Clifford Heath <no.spam@please.net> |
| Message-ID | <YVrnD.102764$RN2.92597@fx40.iad> (permalink) |
| Date | 2018-09-16 22:22 +1000 |
On 16/09/18 21:25, Tom Gardner wrote: > On 16/09/18 11:18, Clifford Heath wrote: >> On 16/09/18 17:42, Tom Gardner wrote: >>> On 16/09/18 04:58, Clifford Heath wrote: >>>> On 16/09/18 02:28, Tom Gardner wrote: >>>>> I know of three languages where subsetting is a practical >>>>> necessity: C, C++, and the SPARK subset of Ada. That's >>>>> significant. >>>>> >>>>> However SPARK's objective and *ability* is something that >>>>> C/C++ cannot even dream of: provably correct implementation >>>>> for use in high integrity systems. To get that you would have >>>>> to subset /any/ language (except possible NewSpeak!). >>>> >>>> You must be unfamiliar with the *formally proven* C compiler >>>> that was part of the sel4 (formally-proven microkernel) project. >>>> I've met some of the people, who work here in Sydney. >>>> >>>> They proved the operating system guarantees *down to the silicon* >>>> for a specific ARM 9 chip (with MMU). >>> >>> Reference please, and has the claim withstood knowledgeable >>> scrutiny? >>> >>> How did they formally prove the compiler? That in itself is >>> "entertaining" for an incompletely defined language such as C. >>> >>> Does "down to the silicon" include the silicon itself? >>> >>> The A9s are complex devices with caches, interrupts etc. >>> How was the effect of those taken into account in the proof? >> >> It it too hard for you to type "sel4" into Google? > > Google orders results on what it thinks you are interested > in :( It is easy for you to provide a definitive link. > > >> The first hit is <https://sel4.systems>, but there are >> many resources for this, including the backgrounder >> on L4 family microkernels on Wikipedia. > > The sel4 FAQ includes "The reduced proof assumptions mean > that we do not need to trust the compiler or linker, but > there may still be faults remaining in specific low-level > parts of the kernel (TLB, cache handling, handwritten > assembly, boot code). These parts are thoroughly manually > reviewed." and "From C code to binary code, we employ a > set of automated widely-used verification tools. These > are: SONOLAR, Z3, Isabelle/HOL, and HOL4." > > That looks like the *compiler* isn't formally verified. The C code is annotated with special comments that contain guidance for the automated provers. The provers analyse the C code, and the final binary, and (using knowledge of both C and the ARM instruction set) can formally prove the equivalence. So no, the compiler is not proven - but all of its specific outputs are proven to be an accurate translation of the respective inputs. That's good enough. It might not work for all possible C code, but it doesn't need to; it just needs to work for the actual code being compiled. > It also makes me ask the question as to whether C is > "merely" an intermediate language autogenerated from a > HOL spec. No. However the specification (the invariants that must be proved) are written in literate Haskell. >> This is the culmination of a massive multi-decade effort >> by some of the world's smartest people. It's not some >> maverick's hobby. > > I've seen many such activities since the early 80s, some > of them also based on LCF. They went nowhere. There has been no result like this anywhere before, period. Besides that, sel4 and its precursors are already in significant deployments, but guess what? They're all secure systems and don't tend to talk about it. Clifford Heath.
Back to comp.arch.embedded | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
arm-gcc: pointer to constant string pozz <pozzugno@gmail.com> - 2018-09-14 09:50 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 11:18 +0200
Re: arm-gcc: pointer to constant string pozz <pozzugno@gmail.com> - 2018-09-14 13:05 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 13:25 +0200
Re: arm-gcc: pointer to constant string Nils M Holm <nmh@ananda.local> - 2018-09-14 09:47 +0000
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 12:26 +0200
Re: arm-gcc: pointer to constant string Stef <stef33d@yahooI-N-V-A-L-I-D.com.invalid> - 2018-09-14 14:52 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 16:04 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-14 15:48 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 17:02 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-14 18:45 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 20:37 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-14 20:51 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-15 16:24 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-15 17:28 +0100
Re: arm-gcc: pointer to constant string Clifford Heath <no.spam@please.net> - 2018-09-16 13:58 +1000
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 08:42 +0100
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 08:47 +0100
Re: arm-gcc: pointer to constant string Clifford Heath <no.spam@please.net> - 2018-09-16 20:18 +1000
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 12:25 +0100
Re: arm-gcc: pointer to constant string Clifford Heath <no.spam@please.net> - 2018-09-16 22:22 +1000
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-16 15:00 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 14:33 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-16 22:06 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-16 21:42 +0100
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-17 21:24 -0500
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-18 08:49 +0200
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-21 22:15 -0500
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-22 11:53 +0200
Testing (Was: arm-gcc: pointer to constant string) Jacob Sparre Andersen <jacob@jacob-sparre.dk> - 2018-09-22 12:16 +0200
Re: Testing (Was: arm-gcc: pointer to constant string) David Brown <david.brown@hesbynett.no> - 2018-09-22 13:31 +0200
Re: Testing (Was: arm-gcc: pointer to constant string) Clifford Heath <no.spam@please.net> - 2018-09-23 09:26 +1000
Re: arm-gcc: pointer to constant string Niklas Holsti <niklas.holsti@tidorum.invalid> - 2018-09-22 20:06 +0300
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-23 14:39 +0200
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-22 13:50 -0500
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-23 15:21 +0200
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 16:06 +0100
Re: arm-gcc: pointer to constant string julio@diegidio.name - 2018-09-23 08:41 -0700
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 16:49 +0100
Re: arm-gcc: pointer to constant string julio@diegidio.name - 2018-09-23 08:56 -0700
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 18:20 +0100
Re: arm-gcc: pointer to constant string julio@diegidio.name - 2018-09-23 12:05 -0700
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 20:50 +0100
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-23 12:04 -0500
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-23 18:27 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-23 19:37 +0200
Re: arm-gcc: pointer to constant string Jacob Sparre Andersen <jacob@jacob-sparre.dk> - 2018-09-24 12:53 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-24 13:49 +0200
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-28 20:17 -0500
Re: arm-gcc: pointer to constant string Tom Gardner <spamjunk@blueyonder.co.uk> - 2018-09-18 08:32 +0100
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-18 10:02 +0200
Re: arm-gcc: pointer to constant string Les Cargill <lcargill99@comcast.com> - 2018-09-21 22:17 -0500
Re: arm-gcc: pointer to constant string Stef <stef33d@yahooI-N-V-A-L-I-D.com.invalid> - 2018-09-14 18:30 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 20:46 +0200
Re: arm-gcc: pointer to constant string Stefan Reuther <stefan.news@arcor.de> - 2018-09-14 19:57 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-14 20:56 +0200
Re: arm-gcc: pointer to constant string Stefan Reuther <stefan.news@arcor.de> - 2018-09-15 18:32 +0200
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-16 15:06 +0200
Re: arm-gcc: pointer to constant string Richard Damon <Richard@Damon-Family.org> - 2018-09-14 19:59 -0400
Re: arm-gcc: pointer to constant string David Brown <david.brown@hesbynett.no> - 2018-09-15 16:25 +0200
Re: arm-gcc: pointer to constant string Tauno Voipio <tauno.voipio@notused.fi.invalid> - 2018-09-14 13:49 +0300
csiph-web