[SystemSafety] Critical systems Linux

[David Crocker]

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

On 22/11/2018 12:45, Olwen Morgan wrote:
>
> 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
>
>
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription:
> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety