[SystemSafety] Critical systems Linux

[Olwen Morgan]

Rod,

That depends on your degree of confidence in the preservation of 
semantics. With C as the target language and a C compiler as the back 
end, you are translating into something whose standard gives so much 
latitude to the implementor that it's anyone's guess whether or not 
you've introduced ambiguity.Although one can guard against ambiguity to 
a substantial extent by ultra-strict sub-setting and usage rules, I 
don't have and I've not yet seen a convincing demonstration that 
ambiguities can be entirely avoided even by draconian sub-setting - 
especially given the latitude that the C standard permits to optimisers. 
The C standard permits an implementation to omit any evaluation provided 
that it can deduce that no needed side effect is thereby omitted - but 
since the standard does not actually define what constitutes a "needed 
side effect", one ends up in a no-man's land where implementations 
generally appear to behave sensibly but none is actually obliged to.

Although I usually program in a paranoiacally strict subset of C - and 
I've not yet come unstuck with it - I wouldn't be first in the queue to 
claim it's foolproof. When programming for bare-metal targets, you 
sometimes have to examine generated code manually to ensure that nothing 
silly has happened. One example of this is an idle loop at the end of a 
cycle in a cyclic executive with a timed interrupt triggering each 
cycle. You might code the loop as:

     i = 1;

     while (i) { i = 1-i; i = 1-i };

but the standard does not forbid a C implementation from generating no 
code at all for this. I've never known this to happen in C but I've been 
told on good authority that some FORTRAN compilers have been known to 
optimise such loops away to nothing.

One could try:

     volatile int i = 2;

     while (3 != i) { i = (i+i)%7; }

in a two-prong attack to defeat an optimiser. If it ignores the volatile 
qualifier, you hope that it cannot deduce that i cycles through only 
quadratic residues mod 7 and therefore can never be equal to 3. Yet, in 
a really adverse case you might have to code such a loop using gotos to 
avoid stack problems.

On the other hand, a lot of embedded programmers might simply avoid the 
faffing and resort to embedding in-line assembler in the C giving a 
self-looping instruction such as:IDLE: JMP IDLE

where this instruction simply jumps to itself - and there are some 
circumstances in which this may be technically preferable.

With C there can never be the solidity of technical guarantee that one 
might like. You might recall my earlier-posted piece of C mischief:

#include <stdio.h>

void PrintEvalOrder( int p1, int p2, int p3)
{
     printf("\np1, p2, p3 evaluated in order: p%i, p%i, p%i\n", p1, p2, p3);
     return;
}

int main(void)
{
     int i = 0;

     /* next line tests order of eval. of args to a function call */

     PrintEvalOrder((++i), (++i), (++i));

     return 0;
}

Compiled under gcc version 5 and then run, this outputs: "p1, p2, p3 
evaluated in order: p3, p3, p3" - thereby revealing over-agressive 
optimisation even in a simple program.

One hopes that CCG steers clear of such problems but I'd challenge 
anyone to give a rock-solid proof that that is the case.


Olwen


On 22/11/2018 22:41, Roderick Chapman wrote:
> On 22/11/2018 14:44, Olwen Morgan wrote:
>
>> Of course, CCG will still face the same problems that I mentioned in 
>> previous postings. 
>
> I don't understand that... the compiler should be semantics-preserving,
>
> so verified, unambiguous SPARK becomes C with the same semantics.
>
> Why would a compiler _introduce_ ambiguity when there's no need to do so?
>
>  - Rod
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: 
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety