[SystemSafety] C for OSs

[Olwen Morgan]

I agree with your point about different compilers. It's a hefty 
challenge for any C tool developer to come up with retrofitted formal 
semantics that fit many compilers.

As regards the lack of features in C, again I agree. AFAI recall QAC can 
produce diagnostics that make up for the lack of named type equivalence. 
Functions can make up to a significant extent for the lack of 
first-class Boolean and array types. One can program around the lack of 
user-defined scalar types. But of course, C simply does not have packages.

But for all the possibility of workarounds, they remain just that. It 
takes effort to give yourself anything approaching the convenience of 
Ada's superior language design.

Your comment about an acceptable false-positive rate is illuminating. 
Very early in my use of QAC, I simply decided to live with a high 
false-positive rate as the price of getting good diagnostics. Only 
gradually did I reduce the false positives by adopting the 
paranoid-critical C programming style that I use today - and here the 
surrealist overtones are not entirely frivolous.

For the avoidance of doubt, _IMO yo__u _*_c_**_annot _**_equal_*_SPARK 
Ada code quality in C_. I've only ever said that you can approach it 
(albeit, I'm confident, fairly closely) by using different best-of-breed 
tools and exercising a severe coding discipline that takes a long time - 
and perhaps a peculiar mindset - to acquire.

And all that hassle really shouldn't be necessary in the first place.

Olwen


On 09/09/2019 10:29, Roderick Chapman wrote:
>
> On 08/09/2019 18:23, Olwen Morgan wrote:
>> Rod Chapman and I have a long-standing (and exceedingly civilised :-) 
>> difference of opinion in this area. If you have the right tools, and 
>> if you are prepared to observe draconian coding discipline, then I 
>> believe that you can in C approach a SPARK Ada level of code quality. 
>> Rod, if I am not traducing him, has lingering doubts about this. IMO 
>> tools are no longer the problem since those who write them simply 
>> retrofit sensible formal semantics to (annotation-extended subsets 
>> of) C and then perform verifications accordingly.
>
> I still have reservations. The big challenge is to come up with a 
> formal semantics that is implemented by both your favourite 
> verification tool and all versions of all compilers that you might 
> have to use during the lifetime of a project. If you can "lock in" to 
> exactly ONE compiler, then things are significantly simpler... but 
> this is not a good place to be when, in twenty years time, you really 
> do have to change compiler for a hardware update or some other reason, 
> but the vendor has long since gone out of business. I see far too many 
> projects stuck in this particular rut.
>
> In SPARK, it works by the complete removal of undefined behaviours and 
> any dependence on unspecified behaviour. This requires subsetting and 
> forms of analysis, which you need to be demonstrably sound and 
> efficient enough to scale up to large programs.
>
> I am currently engaged in writing some highly critical C code, using 
> the latest Frama-C toolset. I find the experience rather 
> frustrating... the problem seems to be two-fold:
>
> 1. C is lacking some fundamental features that make SPARK work. (The 
> short version: user-defined scalar types, named type equivalence, a 
> first-class Boolean type, packages, formal parameter modes, and 
> first-class array types).
>
> 2. Some very basic things in C are undefined. Worst-offender: signed 
> integer overflow.
>
> The upshot is that I find it's very hard to get to an acceptable 
> false-positive rate from the Frama-C WP tool. On a recent SPARK 
> project, the "acceptable" false alarm rate for type-safety proof was 
> ZERO.. so perhaps my expectations are set too high?
>
> Example: in SPARK, we use user-defined scalar types all over the place 
> to describe invariants from the problem domain which apply to every 
> parameter, constant and variable of each type. That info is used by 
> the VC generator to constrain the values of variables, so that proving 
> non-overflow becomes tractable. I don't know how to do that in C... 
> (if anyone does know how, please help me out...)
>
>  - Rod
>
>
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: 
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190909/c109b575/attachment.html>