Re: How to get Ada to ?cross the chasm??

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 18-05-10 01:03 , Paul Rubin wrote:
> Niklas Holsti <niklas.holsti@tidorum.invalid> writes:
    ...
>>> for which I'm surprised the methods we're discussing are ever viable.
>> Which methods are these? I'm perhaps lost.
>
> Applicative data structures, and methods in general that use dynamic
> memory allocation extensively.  I'm used to the idea of a realtime
> program as being something you could reasonably write in MISRA C or
> Forth, i.e. it would tend to have completely static storage, mostly
> straight-line code in fixed-sized loops, even with not too many "if"
> statements past some kind of event dispatch.  That is probably a little
> too constrained though.

Well, there is a scale: real-time system; hard real-time system; 
life-critical hard real-time system. The fixed-size loops and other very 
strong constraints on control structures are perhaps required at the 
last level. But at that level the usual practice is to omit even the 
real-time kernel and use a single thread.

(Your mention of Forth I don't understand. I see Forth as one large step 
below C in language level -- cripes, one even has to manage the stack 
manually! -- and requiring extremely careful coding to avoid the program 
going off the rails. Moreover, I don't see any particular support in 
Forth for real-time aspects or control-flow restrictions such as loops 
with static iteration bounds.)

The concept of "dynamic allocation" is interestingly vague. All 
real-time applications I've seen have dynamic allocation in various data 
buffers and queues, even if they never use the system heap. Of course, 
the designers foresee that the buffers and queues can become full, and 
design the application to be robust and degrade gracefully if that happens.

The problem with heap allocation, I think, is that is hard to foresee 
and describe the conditions under which the heap might overflow, in part 
because of fragmentation. This could be mitigated by using 
application-defined storage pools, in Ada or other languages. Dedicating 
a storage pool of a defined size to a specific kind of objects, perhaps 
with a fixed size, can avoid or reduce fragmentation and lets one define 
a memory budget for that kind of objects, which can help SW operators 
avoid overflows.

> I've played around with this and it's cool:
> https://github.com/tomahawkins/atom

"Compile-time task scheduling" probably means fixed task frequencies, 
rather than event-driven, preemptive tasks, am I right?

>>> I'd still like to know if there is careful analysis about max structure
>>> depth and WCET, particularly formal analysis.
>> Sorry, I don't understand what you want to know. Clarify, please.
>
> E.g. I look at that GADT-checked Haskell red-black tree indexed using
> zippers, and can imagine that being implemented with a refcounted
> system.  Some bounds on the tree size give consequent bounds on its
> depth, so it could conceivably be used in a system with a WCET analysis.
> What I wonder is whether anyone does that in practice.

Balanced tree structures are certainly used in real-time systems, but 
the ones I've seen have not been applicative. As you say, there are 
bounds on the tree size, from which WCET bounds can be computed (usually 
based on measurements of test cases, followed by analytical 
extrapolation to the maximum depth).

> I imagine working on a realtime system like your satellite stuff, and
> going into the office saying I wanted to use something like that.
> My boss would probably tell me I was crazy.

There are certainly two aspects: technical feasibility, and the need for 
qualification and acceptance by product assurance. New ideas as hard to 
get past product assurance people, who tend to be quite conservative 
(with good reason).

Ideally, one should show that although the new idea adds complexity at 
one point (eg. reference counting or GC) it will reduce complexity in 
other places (eg. by making some data structures applicative and 
therefore simplifying high-level task/timing interactions). It may still 
be necessary to put more than normal effort in the verification and 
validation of the new type of SW.

-- 
Niklas Holsti
Tidorum Ltd
niklas holsti tidorum fi
       .      @       .