[SystemSafety] Critical systems Linux

Thu Nov 22 15:12:51 CET 2018

Don't agree.  Just because some would like to see the proofs, doesn't mean
they should and doesn't make it any less safe if they don't.  Airbus don't
make their proofs public....but the certifier gets to see them if they
wish.  And it's not all about the proofs per se, it about what you are
trying to prove.

Nick Tudor
Tudor Associates Ltd
Mobile: +44(0)7412 074654
www.tudorassoc.com

*77 Barnards Green Road*
*Malvern*
*Worcestershire*
*WR14 3LR*
*Company No. 07642673*
*VAT No:116495996*

*www.aeronautique-associates.com <http://www.aeronautique-associates.com>*

On Thu, 22 Nov 2018 at 13:40, Olwen Morgan <olwen at phaedsys.com> wrote:

>
> Agreed about sub-sets. AFAI can see, tool-enforced language sub-setting is
> still the most cost-effective way to avoid the majority of problems due to
> poor language definitions.
>
> I'm not so sure about proofs that are not open to public scrutiny. If the
> FOSS camp can produce decent software - regardless of whether it's up to
> snuff for certification purposes - then one hopes that it might one day
> produce the kind of open proofs that would be helpful. ... But I'm not
> holding my breath.
>
> Olwen
>
>
> On 22/11/2018 13:21, Nick Tudor wrote:
>
> I agree with David: just because not every individual sees all the work
> done on semantics (it doesn't have to be 'open' just because some might say
> it should be), it doesn't mean that it is not good work and can support the
> claims for formal proof of C code....or indeed, any other language for that
> matter.  Furthermore, not all C constructs are necessarily useful in
> practical systems and hence it strengthens the argument for use of subsets,
> which are [obviously] easier to formalise and then to automate the proof.
>
> Nick Tudor
> Tudor Associates Ltd
> Mobile: +44(0)7412 074654
> www.tudorassoc.com
>
> *77 Barnards Green Road*
> *Malvern*
> *Worcestershire*
> *WR14 3LR*
> * Company No. 07642673*
> *VAT No:116495996*
>
> *www.aeronautique-associates.com <http://www.aeronautique-associates.com>*
>
>
> On Thu, 22 Nov 2018 at 13:11, David Crocker <dcrocker at eschertech.com>
> wrote:
>
>> 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
>>
>> _______________________________________________
>> The System Safety Mailing List
>> systemsafety at TechFak.Uni-Bielefeld.DE
>> Manage your subscription:
>> https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
>
> _______________________________________________
> The System Safety Mailing Listsystemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety
>
> _______________________________________________
> 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/20181122/7a427287/attachment-0001.html>