[SystemSafety] Critical systems Linux

[Olwen Morgan]

On 22/11/2018 12:05, Peter Bernard Ladkin wrote:
> On 2018-11-22 11:47 , Olwen Morgan wrote: 
>> <snip>
>> There is, of course, a massive problem with the proof, namely that 
>> the target language C does not have formal semantics. 
> I wouldn't categorise this as a "massive problem". It is an issue that 
> is and was well-recognised.

I think we'll have to agree to differ civilly on that one. Without 
codification of semantics in a formal system, there can, by definition, 
be no formal proof. The mathematician in me regards that as a massive 
problem.


> The question is rather more direct than whether any given PL has a 
> "formal semantics". Put bluntly: for any code X which your 
> code-generator generates; does X have an unambiguous behavioural 
> semantics?
C *does not* have unambiguous semantics. In the following program (which 
I have posted before) the order of evaluation of the operands of the 
assignment = operator is RL in the first instance and LR in the other 
for both clang and gcc. Here both compilers are taking advantage of C's 
latitude in leaving things implementation-defined or unspecified and 
choose different orders according to context:

#include <stdio.h>

int incr(int n) { return n+1; }

int main(void)
{
     char a[2] = {'R', 'R'};
     int  i    = 0;

     char b[2] = {'R', 'R'};
     int j     = 0;

     a[i] = (++i, 'L');
     b[j] = (incr(j), 'L');

     printf("\nEvaluation of = in \"a[i] = (++i, 'L');\"     is %c%c\n", 
a[0], a[1]);
     printf("\nEvaluation of = in \"b[j] = (incr(j), 'L');\" is %c%c\n", 
b[0], b[1]);

     return 0;
}

Moreover, the compiler is free to do this differently in different 
compilation runs since not even that would contradict the standard. In 
fact, AFAI can see, a JIT C compiler would be free to change the order 
of evaluation dynamically within the same program, again without 
contradicting the standard. Worse still, the standard allows an 
implementation to omit the evaluation of any operator if the 
implementation can determine that no "needed side effect" is thereby 
lost. Unfortunately, the standard does not defined what is meant by the 
phrase "needed side effect". Unless you have absolute contol over how 
optimisers work, this completely screws any attempt to avoid ambiguity.

The developers of the SCADE C code generator are indeed aware of these 
problems but the last time I spoke to one of them about the order of 
evaluation issue shown above, he didn't seem to be sure how the tool 
dealt with it. If their subset avoids these problems, then strictly 
speaking, they need to give a proof of it - whereat again they will 
collide with the lack of formal mathematical semantics for C.

The galling thing is that all this uncertainty is wholly unnecessary. 
One could devise a language that looked exactly like C but had 
unambiguous formal semantics. Though this would be a large task, it 
would pose neither new nor insuperable problems, given the current state 
of the art in formal methods.

Olwen