[SystemSafety] C for OSs

[Olwen Morgan]

On 08/09/2019 09:39, David MENTRÉ wrote:

> -<snip>-
> As Olwen Morgan suggested, you can often resort to design system using
> simple formalisms like automata or petri-nets. In that case, you have
> option to use graphical tools like SCADE that will generate C code with
> reasonable safety features. But again, you might have many issue to
> convince people to use SCADE.
Well, I ought to qualify myself somewhat here. I think I've said before 
that I prefer to work on small-to-medium microcontroller systems, 
because that way it's not too difficult (if circumstances allow) for you 
to model and verify all of the code in your application. This does not 
scale up well to cases where you've decided you need a big-processor 
target, because then you need at least a basic OS just to handle the 
complexity of that kind of bare metal - and that's quite apart from 
application support functionality. I am, however, strongly inclined to 
believe that the availability of industrial x86_64 boards is blinding 
systems designers to hardware solutions that run several lesser-powered 
microcontrollers in parallel on a single board. With the right approach 
to design, such cellular systems architectures can be made readily 
extensible and, at least in principle, be easier to model and verify 
than more monolithic efforts heaved onto a single leviathanesque CPU. 
IMHO big-processor hardware is having perverse effects on a great deal 
of systems design in areas just outside the reach of single 
lesser-powered CPUs.
>
> But I fully agree with quote from Tom van Vleck: simply banning C
> language would probably help a lot to improve the situation. Of course,
> it will never happen.

On a more constructive note, it would not be particularly difficult to 
modify C the standard to work around it's more troublesome features. I 
have indeed suggested to BSI panels and ISO WGs that a provision in the 
C standard of requirements for a canonical implementation - preferably 
supporting proof annotations - could more or less achieve the desired 
effect in itself. Needless to say, I was p!ssing into a hurricane.

Rod Chapman and I have a long-standing (and exceedingly civilised :-) 
difference of opinion in this area. If you have the right tools, and if 
you are prepared to observe draconian coding discipline, then I believe 
that you can in C approach a SPARK Ada level of code quality. Rod, if I 
am not traducing him, has lingering doubts about this. IMO tools are no 
longer the problem since those who write them simply retrofit sensible 
formal semantics to (annotation-extended subsets of) C and then perform 
verifications accordingly. The real obstacle is that very few C 
programmers are actually prepared to exercise the level of coding 
discipline required. I find this puzzling, because I am by now so used 
to it that it's actually hard for me to program in a looser style. Alas, 
not all of us are autistic, parlously gaffe-prone geeks who are unable 
to think much about anything without also thinking about it 
mathematically. (But just to confirm, I *don't* think about sex that way.)

Shooting of - and/or gulags for - some of the more unwashed among the C 
lumpenprogrammariat might help. I've looked into it but decided that I 
couldn't remove enough of them from the meme pool before the authorities 
caught up with me. ... :-O


Not that I've become a Stalinist in my old age ... no ... never ...

Olwen


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190908/70c43bad/attachment.html>