Re: Safety-critical development in Ada and Eiffel

[donh@syd.csa.com.au (Don Harrison)]

Ken Garlington wrote:

:Don Harrison wrote:

[...]

:> The problem is many Ada developers misuse priorities to acheive correct
:> synchronisation. Realtime systems that misuse priorities in this way tend
:> (not surprisingly) to be very fragile, suffering from race conditions.
:> The basic problem with using priorities for syncronisation is that you cannot
:> guarantee correct behaviour. It is the *wrong* tool for the job. So, what's
:> the right tool?
:
:Possibly true, although I've never seen it done (for the obvious reason
:you cite!)

I find that hard to believe. Judging by the sort of problems that have been 
raised in this thread alone, that's *exactly* how a lot of Ada software works.

[...]

:> Now, back to the priority issue..
:> 
:> Because, under SCOOP, you can apply such synchronisation assertions to any
:> separate object, you are able to specify precisely the assumptions relevant
:> to the operations offered by those objects and guarantee correct use.
:> This leaves priorities to be used for what their proper use - expressing
:> relative importance of threads for facilitating timeliness. Consequently,
:> I expect a system implemented using SCOOP would have more "priority-less"
:> threads.
:
:Unfortunately, systems that represent digital models of analog functions (e.g.
:flight controls, IRSs) will confound your expectations :)

..in spite of not having any expectations of them. If you say so.

What I *do* expect is that more prioritisation is required the more numerous 
and more stringent timing constraints become. 


[...]

:>  I'm not aware of any published information
:> about how this is intended to work but imagine it could use abslolute priorities
:> (so implying relative ones):
:> 
:>   set_priority (p: PRIORITY) is ..        -- set absolute priority
:>   yield (p: PRIORITY) is ..               -- yield to priority p or greater
:>   etc.
:> 
:> :That would be a serious maintainability issue, I would think.
:> 
:> Yes, if it were true - but it isn't.
:
:See above. If the relative priority of each interaction is distributed, then
:it's true.

Perhaps you haven't grasped what I'm saying here. I'm saying that's exactly 
what you *wouldn't* do. You would use absolute priorities (as you do in Ada)
to *imply* relative ones.


:> :>   - A thread which absolutely must execute (possibly driven by a timer) can
:> :>     issue a challenge for a resource.
:> :
:> :If, while another thread is operating, it cannot be interrrupted (as your
:> :previous note said, a thread cannot be interrupted even between object calls),
:> :then how does the other thread begin execution to issue the challenge?
:> 
:> We're talking single processor here, of course (the issue doesn't arise with
:> multi-processors). An executing thread will give up the processor to another
:> thread if it blocks on a synchronisation condition (a precondition on a
:> separate object). 
:
:Not in the real word of embedded systems. Think about non-maskable hardware
:interrupts.

Not sure what you mean by "non-maskable .. interrupts". Care to explain?
However, wrt interrupts generally, a SCOOP implementation could provide 
an external mechanism for attaching routines to interrupts. This information 
would appear in an external configuration file as for non-benign functions (see 
below).


:> :> I was also concerned about this issue initially but came to the conclusion
:> :> that objects would be locked for just as long as they (safely) need to be.
:> :> Where it's important to release a frequently used shared resource quickly,
:> :> various design strategies can be applied to minimise locking.
:> :
:> :Don't these "design strategies" cause the same uncertainly that you said
:> :you didn't want?
:> 
:> No.
:
:Why not? Can't the developer (whom you don't trust) fail to properly implement
:these "design strategies"?

Here it is again (since you obviously missed it the first time)..

:> Also, these techniques can be applied to *any* concurrent system - they
:> are not SCOOP-specific. Hence, they're not relevant to any discussion about
:> the relative merits of different concurrency models.
:
:Are there deployed systems that use these techniques?

Yes, you probably use them yourself. :)

:> :For example, if a lower-priority thread agrees to give up control
:> :of an object to a higher-priority thread, then race conditions are possible
:> :if the threads are not designed properly.
:> 
:> Assertions would help you to design them properly and avoid such conditions.
:
:... Your original position was that the compiler should take care of
:all of this, so that the designer would not make an error. 

Rubbish! Report accurately what I say or forget about discussing anything.

What I *did* say was something like "Under SCOOP, race conditions would not
be an issue..". "Under SCOOP" implies not just using the mechanism but using
it to its full potential. If you use (synchronisation) assertions to document 
your assumptions, race conditions shouldn't exist. Naturally, race conditions
*will* exist in the absence of such specifications.

Having said that, I need to clarify what I mean by "race conditions". I mean 
incorrect behaviour resulting from inadequate (or non-existent) synchronisation.
I *don't* mean thread starvation or deadlock. These are avoided by designing 
correctly.

:Now you depend upon the designer to implement the timing process properly 
(and write the proper assertions; 

No, that was always implied. You incorrectly *assumed* I meant something else.


:> Also, invariants will guarantee that an object yielding in a duel will end
:> up in a consistent state.
:> 
:> :This seems counter-intuitive. Consider the simple protected object discussed
:> :earlier with the Read and Write operations. It would seem that the object
:> :itself, with its internal knowledge of how Read and Write works, would be
:> :the better place to control when blocking needs to occur.
:> 
:> That *is* how blocking works under SCOOP. The operation of the supplier object
:> contains the precondition, so the supplier determines the (synchronisation)
:> contract.
:> 
:> :In order for the
:> :threads that use this object to decide the outcome of their "duel", don't
:> :they have to know the internal operation of the object -- an object contract
:> :violation?

Sorry, I should have pointed out here you're confusing blocking and duels.

In the case of blocking, the callee determines how a caller will synchronise 
with it. In the case of callers duelling for a callee, their relative 
"priorities" (probably inferred from absolute priorities) will determine the 
outcome of the duel.

:> No, only the object has to know (and how to restore its invariant - ie. how
:> to return to a consistent state).

Sorry, I gave you a bum steer here. :(

The state of a called object has nothing to do with the outcome of a duel - 
it's determined by the relative "priorities" of the callers (duellers). My 
explanations of blocking and duels may make more sense to you now if you re-read 
them.

:You've pretty much worked me around in circles. 

Thank you. :)


:> :Describe the general-purpose algorithm used to determince this by a compiler.
:> 
:> Ask Robert Dewar because that's what happens with protected types.  :)
:
:ABSOLUTELY NOT. The developer of the protected type explicitly provides the
:criteria; there's no magic going on in the compiler. I think your understanding
:of Ada is at least as hazy as my understanding of SCOOP :)

We may be talking about different things here. I'm talking about the ability
to have concurrent reads (queries). This is precisely what happens with 
protected types (where functions can be executed concurrently) so the 
optimisations I say are possible in SCOOP would be materially no different from
those implemented for protected types.


:> :> :You claimed that the compiler could optimize the timing properties of
:> :> :the system; I would be interested in seeing such a compiler..
:> :>
:> :> I don't think it would be too hard. The compiler just has to verify that
:> :> queries (functions) are truly benign
:> :
:> :Define "benign"! For example, is a read of a memory location "benign"?
:> :Maybe not, if it's memory-mapped I/O. Some devices, for example, don't take
:> :kindly to starting a read and being interrupted in the middle to do a new
:> :read.

A function is "benign" if it has no side-effects. That is calling it (and,
possibly, interrupting it in the middle) will not change the state of the 
system - software *and* hardware.

:> This issue is common to any concurrency model.
:
:Which is why it's a situation that the _developer_, not the compiler,
:must address. It is also why the language has to give the _developer_
:the flexibility to address it (even if he is still capable of shooting
:himself in the foot).

Sure. A SCOOP implementation could provide for this in an external configuration
file, for example. This would be a better option, IMO, than some language 
construct. An appropriate mechanism will give you both efficient sharing of 
resources and safety.


:> :You may not think it's too hard, but I suspect you haven't encountered
:> :many of these real-life systems.
:> 
:> You could be right. Perhaps, I've learnt nothing from my 8 years realtime
:> experience (including 3 years hard realtime). (I think combat systems qualify
:> for hard realtime - at least, I found it quite hard. :)
:
:Absolutely not, if the combat systems (1) were not _embedded_ (which is where
:many of these problems come up), (2) had minimal OS support (I've seen workstation
:programmers with over ten years experience with realtime systems that have
:never had to worry about these issues), and (3) had to deal with hard realtime
:in the sense that the system _totally fails_ if a complex set of deadlines
:fail -- as opposed to the user getting irritated that the system is too slow.

My combat systems qualifies on all counts but, frankly, its quite irrelevant
to whether what I have to say has any substance.

IMHO, sprouting one's experience (or academic credentials) as though it is the 
final arbiter of truth is just pissing on power poles. Rather than adding weight 
to one's arguments, it betrays the fact you think you know it all. Sadly, anyone 
with that sort of attitude is impervious to learning anything new.


Don.
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-
Don Harrison             donh@syd.csa.com.au