[SystemSafety] Critical systems Linux

[Olwen Morgan]

So it is. MEA CULPA! Just goes to show how even experienced people (25 
years with C) can fluff things in this area. Such are the delights of 
ageing memory and of having to use 300-page long (for C99) language 
standards.

C's implementation-specific categories are pretty unhelpful here. 
Several of the things categorised as undefined could more sensibly be 
categorised as implementation-defined. Multiple modifications between 
sequence points are a case in point. The simplest thing for an 
implementor to do is to choose some order for the sequence points and 
leave it at that - there's no point in bombing out with an error if you 
don't have to. IMO there should be no latitude for abnormal termination 
where it's unnecessary. I still think that the developers of gcc do not 
actually intend the behaviour that my test elicits and that it is due to 
over-aggressive optimisation. It is, as you say, strictly-speaking not 
wrong but if it is what the gcc developers intend, then IMO it is 
exceptionally perverse.

As regards the categorisation of implementation-specific behaviours, C 
and the C-derived languages do, IMO, a worse job than the Pascal-derived 
languages. The original Pascal standard had the categories of;

1.    Implementation-defined - meaning not defined by the standard but 
defined in every implementation.

2.    Implementation-dependent - meaning not defined by the standard and 
not necessarily defined in every implementation.

3.    Errors.

AFAI recall, Ada does something similar (?????) ... anyway, these 
categories are rather easier to work with when trying to produce tests 
of implementation-specific characteristics. When trying to diagnose C's 
implementation-specific behaviours, one tries AFAP to exploit behaviours 
that are implementation-defined or unspecified rather than undefined. 
Leaving undefined things that would more sensibly be made 
implementation-defined or unspecified is, IMO, one of the C standard's 
worst own-goals. The whole point of standardisation is to limit 
*unnecessary* variation. Alas, politics drives standards-making. It 
becomes a chaotic democracy on occasions when it would do better to be 
authoritarian. (I said before that I'm becoming a Stalinist in my old age.)

Nevertheless, what you say actually reinforces my point about the 
unhelpfully wide latitude left to C implementors and why subsets for 
critical applications do well to be ultra-strict - if only to mitigate 
the effects of buggy optimisation AFAI can see, the way forward for 
analysis of C programs is to emulate SPARK Ada. It's a two-stage 
approach whereby (possibly draconian) subset checkers flag up usages 
that make life unnecessarily hard for proof tools and then the proof 
tools get to work on code that is, hopefully, more tractable to analyse.

And as regards compiling Ada to C, I can only suggest that Ada compilers 
that use other C compilers as back ends start migrating to using back 
ends based on (possibly subsetted) LLVM or something similar as soon as 
they become available for the target hardware. C has served us 
undeservedly well as a compiler target language but its weaknesses 
should, IMO, now be left behind in the quest for high-integrity software.


Olwen


On 23/11/2018 15:30, Olivier Andrieu wrote:
>
> On Fri, Nov 23, 2018 at 4:05 PM Olwen Morgan olwen at phaedsys.com 
> <http://mailto:olwen@phaedsys.com> wrote:
>
>
>     On 23/11/2018 12:33, Olivier Andrieu wrote:
>>
>>     I’m not sure why you’re making this about the compilers. This
>>     program has unequivocally an undefined behavior, so, whatever a
>>     compiler does, it’s not wrong.
>>
>>     Clang doesn’t even require an explicit warning option to point it
>>     out:
>>
>>     |$ clang se.c se.c:14:19: warning: multiple unsequenced
>>     modifications to 'i' [-Wunsequenced] PrintEvalOrder((++i), (++i),
>>     (++i)); ^ ~~ 1 warning generated. |
>
>     gcc gives a similar warning but still gets the compiled code
>     wrong, AFAI can infer, by being gung-ho with optimisation.
>
>     As regards behaviour, AFAI can see it's not "undefined" but is
>     covered by "unspecified" or "implementation-defined" behaviour
>     (Derek Jones may correct me here.)
>
> It’s undefined, it corresponds to this case from the ‘Portability 
> issues’ annex of C99:
> /« Between two sequence points, an object is modified more than once, 
> or is modified and the prior value is read other than to determine the 
> value to be stored (6.5) »/
> —
> Olivier
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181123/6120c3f2/attachment-0001.html>