Tasking in safety-critical software (!) (was Re: Need help with PowerPC/Ada and realtime tasking)

["Kevin F. Quinn" <kevq@banana.demon.co.uk>]

JP Thornley wrote:
> 
> Richard Riehle <rriehle@nunic.nu.edu> writes:
>     [well argued case for tasking mostly snipped]

> Several studies into safety-critical subsets have all rejected tasking:-
>         Safe Ada
>         SPARK Ada
>         High Integrity Ada Study (YSE/BAe)
>         CSMART Ada
> so there is going to be a major credibility problem convincing a
> qualification authority to go along with tasking.
> 
> Allow also for the relevant personnel from that authority to have an
> unknown level of mathematical and computer system literacy.

It's worth noting at this point, that IME even the majority of software
engineers have difficulty with the complexity of proving things about
systems using tasks, in anything but the most trivial of cases.  Especially
given that there's little or no tool support.  And the reason there's no
tool support (i.e. the reason why tasks are excluded from those subsets) is
that it's mathematically complex, in the extreme, to perform automated proofs.
Many language features are excluded from those subsets largely on grounds
of being difficult to analyse, rather than any inherent danger from dynamic
behaviours.


> >   A cyclic executive does not guarantee schedulability.  It does not
> even
> >   guarantee predictability.  In fact, a cyclic executive can guarantee
> >   that one actually fails to trap events as they occur.
> 
> But safety-critical systems I'm talking about have *no* interrupts (see
> my original response - perhaps not sufficiently emphasised) so this
> argument does not apply.  (Actually there is one - the timer that drives
> the minor cycle - and this has to be explicitly justified in the safety
> case.)

Agreed.  The cyclic executive _can_ be used to guarantee schedule periods.
In a real-time, safety critical system, a major part of the various analyses
performed are to prove termination of a subprogram, and in the case of real
time applications to prove upper limits on execution times.  This enables
worst-case schedule times to be proven to a high level of confidence.  Of
course, essentially the cyclic executive approach takes control away fro
the "black box" tasking system, and places control explicitly throughout
the application, which helps one to "know" what's happening at various points.

> >   An additional problem with the cyclic executive model is ist lack of
> >   portability.  Since it is dependent on the timings of the platform
> to
> >   which it is targeted, it can fail to meet its goals when ported to a
> >   new platform.
> 
> Agreed - any hardware or software change that affects the timing
> analysis means that you have to do it all again, and you may have to
> redesign the schedule.  (But if it comes to a trade-off between safety
> and portability there's not much doubt as to which way I'd go.)

Portability is largely a non-issue, w.r.t. safety critical software, IME.
As you say, any change in hardware necessitates large volumes of analysis
to be performed again.  Another point is that when hardware changes
substantially (e.g. processor "upgrade", possibly the only real case where
portability would be useful) then the opportunity is often taken to implement
additional requirements that mean large-scale modifications to the software
anyway.

> >   ....  Remember that I speak here of Ada 95 tasking.
> 
> I was beginning to wonder whether I was the only reader of cla still
> using Ada 83 until there were some recent posts from others in the same
> situation in another thread.

Reading this group does, IMO, give a false impression as to the market
penetration of Ada95, certainly in the defence industry.  Large sections
of the industry are still only vaguely aware that it even exists as a
standard, let alone that GNAT is now an almost complete implementation.
Certainly most people I work with (and have worked with), who work with
Ada every day, know little or nothing about GNAT.  Another issue is that
the sort of projects we're talking about have long development periods,
of the order of many years, and of course Ada95 compilers don't have
anything like the maturity of existing Ada83 compilers.

Having said all that, it'll be interesting to see whether GNAT gets used
in very safety-critical systems.  All the source-code analysis in the world
won't help in the slightest if the compiler isn't correct - and with commercial
compilers the best you can expect to get is some kind of statement from
the vendor as to the correctness of the compiler.  Ada95 does have the extra
pragmas to assist in object-code verification, but with GNAT, you have
the complete source code to the compiler - something commercial compiler
writers are unlikely to release, so there are possibilities for actually
including the compiler itself into the proofs.  Not that I'd relish the
task of proving much about the compiler, of course :)

Hmm; that's quite enough for now...

Kev.
Speaking for (and no doubt to ;) ) himself.