Re: Advantages

[Peter Amey <peter.amey@praxis-cs.co.uk>]

Andrew Carroll wrote:
[snip]
> 
>>Quite a lot of the really nasty pitfalls associated with parallel
>>programming in other languages are made either impossible or much more
>>easily detected and debugged by Ada.
> 
> 
> Okay Marin and Nick, I want to learn more.  Where can I find the
> statistical and practical proof?  I'm not trying to snub your comments,
> I just want to be able to provide the proof when I talk to my co-workers
> about Ada.  Thanks!
> 
> 

Not Marin or Nick but unsolicited 2c anyway.

You could take a look at the Ravenscar profile.  This is a subset of Ada 
95's built-in tasking constructs that guarantees schedulability analysis 
and freedom from deadlocks.  Using SPARK in conjunction with this allows 
lots of other nice properties to be proved as well.  Ravenscar is 
interesting because it is existential proof that Ada facilitates 
reliable use of concurrency.  I don't know of any equivalent in any 
other language.  Flight critical software to DO-178B level A has been 
written using these Ada tasking constructs.  The profile will be a 
defined part of the Ada language after the current 2005 revision process.

Some references:
Pofile definition:  <http://polaris.dit.upm.es/~ork/documents/RP_spec.pdf>
Crosstalk article:
<http://www.stsc.hill.af.mil/crosstalk/2003/11/0311dobbing.html>
Aonix Raven link:
<http://www.aonix.com/pdf/ravensc.pdf>
RavenSPARK link:
<http://www.praxis-cs.co.uk/sparkada/pdfs/high_integrity_ravenscar.pdf>

Peter