[SystemSafety] Critical systems Linux

Olwen Morgan olwen at phaedsys.com
Thu Nov 22 14:40:02 CET 2018 

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 <http://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 
> <mailto: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
>     <mailto: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
>     <mailto: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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181122/87c18e07/attachment.html>

More information about the systemsafety mailing list