[SystemSafety] Critical systems Linux
Olwen Morgan
olwen at phaedsys.com
Thu Nov 22 15:42:24 CET 2018
We'll have to differ on that one :-)
A very interesting paper was published on the topic of program proofs
nearly 40 years ago:
de Millo, R. A., Lipton. R. J, and Perlis, A., J., "Social Processes and
Proofs of Theorems and Programs", CACM, V22, No.5 May 1979 (.pdf
available on the net - just google for it).
It argues that program proofs will never have the status of proofs in
mathematics because acceptance of a proof in mathematics depends on
publication and acceptance by a relevant community of mathematicians.
The authors did not see that this would necessarily be the case for
program proofs.
To be honest, I wouldn't trust current regulators to muster enough
expertise to do their job properly when examining a claimed proof of a
program. At the moment, they do a rickety enough job of much simpler
things. That may be unduly pessimistic. Either way, I think that we
shall have to develop some kind of institutional arrangement that allows
greater scrutiny than regulators currently provide - although I wouldn't
like to see this view end up by promoting the better at the expense of
the good.
Olwen
On 22/11/2018 14:12, Nick Tudor wrote:
> 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 <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:40, Olwen Morgan <olwen at phaedsys.com
> <mailto: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 <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 <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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20181122/2ef4eab4/attachment-0001.html>
More information about the systemsafety
mailing list