[SystemSafety] Critical systems Linux

[Olwen Morgan]

David,

I agree that proof up to "well understood" semantics is valuable - as 
is, IMO, using a language subset of draconian severity (you and I, of 
course, have had some quite civil disagreements on this one). And you're 
right, IMO, that fitness-for-purpose or lack of it for s/w 
specifications is a bigger problem.

Much of my uber-quibbling arises from experience in testing compilers. A 
few years ago, I said to someone that it would be perverse of a compiler 
to evaluate an operator in two different orders at different points of a 
program - only to find that a simple test demonstrates just that. And 
having seen some of the results that John Regehr gets using Csmith to 
mount "Battle-of-Stalingrad" assaults on C compilers, I find it 
dispiriting that modern compilers can still be found to be so flaky. One 
hopes that by using LLVM, clang might (ultimately) exhibit fewer 
problems than gcc has in this respect.

Olwen


On 22/11/2018 13:11, David Crocker wrote:
> Olwyn,
>
> While it's true that C doesn't have a formal semantics, in practice the
> semantics of C is well-understood by experts, who write static analysis
> tools to help ordinary users avoid the undefined and unspecified bits
> and most of the implementation-defined bits (including of course order
> of evaluation). So formal proof that the software specification has been
> mapped accurately to the semantics of C as understood by tool vendors
> and compiler writers is still very valuable.
>
> A much bigger problem IMO is ensuring that the formal (or other)
> specification of the software is fit for purpose.
>
> David Crocker, Escher Technologies Ltd.
> http://www.eschertech.com
> Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486