2012-08-31

parasail is big win for reliable concurrency

12.7.2: news.adda/co/ParaSail
(Parallel Spec and Impl Lang) is by Ada's Tucker Taft:

first siting of parasail:
11/09/11 Language Lessons: Where New
Parallel Developments Fit Into Your Toolkit

By John Moore for Intelligence In Software
The rise of multicore processors and programmable GPUs
has sparked a wave of developments in
parallel programming languages.
Developers seeking to exploit multicore and manycore systems
-- potentially thousands of processors --
now have more options at their disposal.
Parallel languages making moves of late
include the SEJITS of University of California, Berkeley;
The Khronos Group’s OpenCL;
the recently open-sourced Cilk Plus;
and the newly created ParaSail language.
Developers may encounter these languages directly,
though the wider community will most likely find them
embedded within higher-level languages.

. ParaSail incorporates formal methods such as
preconditions and post-conditions,
which are enforced by the compiler.
In another nod to secure, safety-critical systems,
Taft says garbage collection isn’t a
good match for high-integrity systems,
noting the difficulty of proving
that a garbage collector is “correct.”
“It is also very difficult to test a garbage collector
as thoroughly as is required by high-integrity systems,” he adds.
Taft’s experience in the high-integrity area
includes designing Ada 95 and Ada 2005.
As for distribution methods,
Taft says he is working with other companies,
including one with a close association with the GCC.
Taft says hooking the ParaSail front end
-- parser, semantic analyzer and assertion checker --
to the GCC back end would be a natural way to
make the language widely available.
Another possibility:
making ParaSail available as a modeling language.
In that context, ParaSail could be used to
prototype a complex system
that would be written in another language.
SofCheck 's current activities? merged with AdaCore:
. SofCheck’s staff has joined the AdaCore technical team,
and SofCheck Founder Tucker Taft
has been named as AdaCore’s
Director of Language Research.
AdaCore has acquired SofCheck’s products,
including static error detection tools, and also ParaSail,
a new Parallel Specification and Implementation Language
intended for high-reliability applications
on multicore target platforms.
S. Tucker Taft is currently
director of language research at Adacore,
and is also founder and CTO, SofCheck, Inc.,
which he started in 2002
to focus on providing tools and technology
to enhance software development quality and productivity.
Prior to that Mr. Taft was a Chief Scientist at Intermetrics, Inc.
and its follow-ons for 22 years.
He graduated from Harvard College in 1975,
Summa Cum Laude in Chemistry.
where he has since taught compiler construction
and programming language design.
From 2001 to the present[2011.8],
Mr. Taft has been a member of the ISO
Rapporteur Group that developed Ada 2005,
and more recently is finalizing Ada 2012.
In September 2009
Mr. Taft embarked on the design of PARASAIL,
(PARAllel Specification And Implementation Language)
a new language that marries pervasive parallelism
with formal methods .


2011.08 parasail's author interviewed
by Clay Breshears (my BASIC teacher)
[8.31:
. Clay Breshears was my 1980's
BASIC language teacher at EWU;
I liked moving up from BASIC to Pascal,
and I was infatuated with the new Ada lang;
so I was shocked when Prof Breshears said
-- on multiple occasions --
that one could never learn all of Ada;
and, ironically, I never did,
because my driving ambition was to
create my own language, adda,
that was concurrent, safe, and rich like Ada,
but also terse like math,
and fun like Lisp (now Python).]
Taft's intro:
 I have been doing language design
 for the past 35 to 40 years.
 Much of that has been associated with Ada
 (particularly Ada 95, where I was the technical lead
 for 5 years of a full-time design team),
 but I was also involved a bit with the
 hardware design language VHDL,
 and with DARPA's Common Prototyping Language),
. I wanted to design a language to address
the "multicore" [GPGPU] revolution
--[ ada was targeting custom chips ]--
along with [Ada's requirement that it be]
inherently safe and secure .
As far as parallelism,
I believe that as long as it's easier to
write a sequential program than a parallel one,
we will continue to write sequential programs.
ParaSail was designed with the goal
that it would be harder to
*not* write a parallel program!

The language is specifically designed to be
very "familiar" to current
Java, C++, C#, Ada, ML, etc. programmers.
You should be able to sit down
and read a ParaSail program on day one,
and start programming soon thereafter.
Fundamentally there are only four concepts:
modules, types, objects, and operations.
All code is parameterized, in the sense of a
generic template (or an ML functor),
so there is no distinction between
generic and non-generic code.
Parallelism is pervasive,
but because the compiler [polices] race conditions,
concurrency doesn't add to debugging complexity.

ParaSail complements scripting languages:
ParaSail is a strongly typed language.
In that sense, it is not expected to be
used as a "scripting" language.
ParaSail is great for rock-solid executables
that take full advantage of multicore .
2012.06: Less is more with multicore:
S. Tucker Taft, AdaCore: [paraphrased]
. here are the biggest impediments to
efficient and safe use of multicore:
* Global Variables
* Garbage-Collected Global Heap
* Parameter Aliasing
* Run-Time Exception Handling
* Explicit Threads
* Explicit Lock/Unlock
* Explicit Wait/Signal
* Race Conditions
* Pointers -- worst of all .

ParaSail is designed specifically to eliminate
impediments to easy parallel programming.
Pointers are eliminated in favor of
expandable and shrinkable objects.
Race conditions are eliminated at compile-time,
as are other possible run-time errors
such as use of null values or uninitialized data,
indexing outside of an array,
numeric overflow, dangling references, etc.
The net effect is
a language that feels familiar,
is a pleasure to program in,
but nevertheless results in
highly parallel, race-condition-free,
well-structured programs.

a ParaSail function doesn't appear to be
doing anything in parallel,
but in fact the basic semantics of ParaSail
imply that the two recursive calls of Word_Count
can in fact be evaluated in parallel.
Those recursive calls then continue the
divide-and-conquer approach to
counting the words in the string,
with the net effect that for a string of length N,
N picothreads are spawned,
with their results added together in a
computation tree of depth log2(N),
providing a potential speedup in the order of
N/log2(N) relative to a sequential algorithm.
No Global Variables
Sometimes globals aren’t globally visible,
but anything that represents global state,
such as a static variable in C, C++, or Java,
or a singleton object in Scala [2],
can create the same kinds of problems
associated with unexpected side-effects,
hidden algorithmic coupling, etc.
In a parallel program,
global variables can create race conditions,
or synchronization bottlenecks.

So how do we live without global variables?
The ParaSail model is very straightforward
– a function may only update data that are
one of its var[out.mode] parameters .
-- the specification of a function
shows us all of its possible effects .

. a pseudo-random number generator
is often implemented using a global variable;
here's the same in ParaSail:
[. as my adda translation: ]
random.type:
<.  start(seed.int`= 1), (obj)`next.int .>
--. start a new random, and tell random to next itself .

 . the first parameter in a call in ParaSail
 may optionally be expressed as an object;
 so instead of Next(Ran),
 one could write Ran.Next().
 [. in adda,
 ran`next means ran may be self modifying,
 whereas next(ran) indicates a pure function:
 ran can't be modified because it's copied;
 although for large structures,
 there can be tricks to get around a copy,
 like giving each obj a read-only capability tag,
 so type mgt knows when to
 disallow modifying operations . ]
 . types can be inferred from context,
 though they could be given explicitly.
 [. my adda translation: ]
 first.: ran`next mod 6 +1
 -- first is obviously const of type int .
 diceSum.type: integer`2..12;  -- parasail's syntax is
 integer<2..12>; 
  (all parameterized types express their arg as <...>)

 Univ_Integer.type features unlimited length;
 --[. is he trying to discourage the use of this type?
 Ada's authors said long names were reader-friendly;
 but, in math, universal integer is abundant,
 it gets its own letter! Z .]
 No Garbage-Collected Global Heap
Using a single garbage-collected heap
is a common language feature;
but a single global heap can be a problem
for a highly parallel application.
. the cache is vital to performance;
so, locality of reference
is important within a single thread,
while separation is important for
threads operating in parallel
to avoid cache interference effects,
such as false sharing .
Unfortunately, a single global heap
[ destroys locality of reference .]

. but users need not resort to
completely manual storage management:
ParaSail uses a variant of
region-based storage management,
pioneered in the Cyclone language,
--[ and featured in adda ]--
where each function or scope
has its own local heap
that is reclaimed automatically
when the scope is deallocated .

ParaSail objects are dynamically resizable
and the storage needed for the growth
comes out of the local heap,
and the storage released by shrinkage
goes back into the local heap .

No data is shared between objects,
so the allocation and release happen
automatically and immediately.
There is no need for an asynchronous
garbage collection process;
because, there is never any garbage to collect.
When a function returns an object to its caller,
it automatically allocates it from
the region determined by the caller.
--[adda uses an implicit
out.mode parameter for this;
eg, every function is assigned to something,
and that something is the out.mode's actual param .]
No Parameter Aliasing
If a function takes two or more parameters
that are passed by reference,
and at least one of them can be
updated within the function,
there is the possibility that
changing the updatable parameter
might affect the value of the other one
[ie, one might be aliasing the other ]
and that can interfere with optimizations,
including the function's parallelization .
In ParaSail, the compiler disallows
parameter aliasing at the point of call,
which ensures that every function
can be fully parallelized.
ParaSail actually goes further,
ensure it can parallelize all expressions.
The following alternative implementation of
Roll_The_Dice is illegal in ParaSail
[. translating this to adda,
I'm assuming the "(var) qualifier
means an inout.mode param, x,
which I write as x`f .]
(ran.random)`rollDice().int:
( (ran`next mod 6 +1),
+ (ran`next mod 6 +1) ).
The above is illegal because
the two operands of the outermost “+”
both involve the Ran variable,
which if evaluated in parallel,
might result in unsafe concurrent updates to the Ran variable.
[ parasail's non-overlapping slices:
( a .. b, b <.. c ) are disjoint enum sequences;
for now I'm using  ( a .. b, b+1 .. c )
but that wouldn't work for floats .]
The net effect of these rules
is that any (legal) ParaSail expression
can be evaluated in parallel:
ParaSail disallows parameter aliasing,
and more strictly,
it disallows two references to the same variable
in different parts of the same expression,
if either one might result in an update .
No Run-Time Exception Handling
Many modern languages provide support for
the raising of exceptions in an inner scope,
and then handling them in an outer scope.
. exceptions serve several purposes:
First,
it means that errors cannot simply be ignored,
unless the programmer takes explicit action to do so
by handling and then ignoring the exception.
Second,
exceptions help avoid a race condition between
checking on the state and then acting on the state,
in the case where the state might be
updated in the interim.
For example, checking whether a file exists
and then opening it as two separate operations
leaves room for the file to be deleted
between the test and the actual open.
The problem is eliminated if the open operation
itself performs the check
and either raises an exception
indicating the file doesn’t exist,
or opens the file and thereby
prevents it from being deleted until it is later closed.
Finally,
exceptions are also useful for signaling
bugs or unanticipated situations,
such as indexing outside the bounds of an array,
attempting to read an invalid data value,
dereferencing a null pointer,
or running out of memory.
The handling for such exceptions is generally limited to
some kind of reset and restart,
perhaps in a degraded mode.

Run-time exception handling,
while clearly useful, has its downsides.
An exception handler creates the potential
for a large number of additional
paths of execution through a function,
and these paths are generally very hard to
test thoroughly.
if the exception was raised before or during
the initialization of the object,
it may be possible for a handler to
access an object that wasn't properly initialized .

And in a highly parallel environment,
exception handling is notoriously troublesome,
because it is not always clear
what should happen
when one thread raises an exception
but does not handle it locally,
while other concurrent threads are proceeding normally.
Should the whole computation be abandoned?
Should the exception be propagated when
all of the other threads complete their work?
Should the exception be swallowed and ignored?

So how does ParaSail provide solutions for
the situations where exceptions are useful,
without incurring some of the downsides
of run-time exception handling?
The primary solution in ParaSail
is that potential run-time errors
are identified at compile time
using types or preconditions,
or an explicit range check guarding a call .

In ParaSail, preconditions, postconditions, assertions, etc.,
are all specified using a notation inspired by Hoare logic,
using one or more Boolean expressions enclosed in {...}.
. S’ refers to the state after the operation is complete,
S by itself refers to the initial state .

. we have to provide some postconditions for the
operations of the Stack module.
In particular we need to say
what the Count and Max_Stack_Size are
of a newly created stack object,
and how they might change as a result of a Push or a Pop.

Here is a fully annotated interface for the Stack module:
[. in my translation to adda,
the syntax is |(pre- or post-condition)
instead of {...};
and to avoid cluttering,
the pre-post-conditions of parameter
are declared after the function
not in the parameter .
]
stack(Compon.type(Assignable)).type:
<.
maxStackSize(s).int;
count(s).int
| (count in 0..maxStackSize(s));
create(max.int)
| (max>0);
(s)`push(x.compon)
| ( count(s) < maxStackSize(s)
  , count(s') = count(s) + 1
  );
(s)`pop.compon
| ( count(s)>0
  , count(s') = count(s) -1
  )
.>
The above pre- and postconditions
should allow the user of the Stack module
to use its operations properly,
and give the ParaSail compiler enough information
to check that calls on Push and Pop
will not cause a stack overflow or underflow.

The ParaSail compiler will also check that
the operations satisfy the postconditions,
given the preconditions.
The programmer may need to provide
additional annotations, such as
an invariant on the state of the
components of the object,
to enable the compiler to prove that the
postconditions are always satisfied.

ParaSail has other features that help obviate
the need for run-time exception handling.
In particular, every type has a null value
in addition to the “regular” values.
The null value can be used for situations like
opening a file – a null file handle
may be returned if the file does not exist.
The null value can be checked for by
[ subtyping x as optional,
and the using a pre- or post-condition of
X is null
or X not null .]
In the absence of being subtyped(optional),
there is an implicit assertion that
the value of the object satisfies {X not null}.

In the Stack module, we used optional
when specifying the
component type of the Data array
to indicate that the values in the array
may have the null value.
However, we did not specify optional
for the Component parameter of Push,
or the Component result of Pop.
This means that the ParaSail compiler
will need to prove that
when S.Data[S.Cur_Len] is retrieved in Pop
it is not null.
. this will require an invariant
of the following form:
{(for all I in 1..Cur_Len => Data[I] not null)}
If such an invariant is specified in the class,
it will be implicitly added to every precondition,
and will need to be proved
in addition to any postcondition,
for every operation of the Stack module.
With this invariant,
the ParaSail compiler can prove
that the value returned by Pop
will not be null.

exceptions indicate resource is exhausted:
. In ParaSail a computation can be split into
a part that does the real work,
and a part that monitors for resource exhaustion
or another important event, at which time,
the overall computation can be terminated
with a return or exit statement
which specifies a value for the computation
that indicates the cause for the early termination.
DrQuine 7/4/2012 12:34 AM EDT
The devil is always in the details.
How does this system address the unexpected?
What happens when one of the threads never returns?
[8.31:
. shouldn't that work like a browser does?
if a web access hangs,
the browser times out,
so, if your child threads return timeouts,
you return failure .
. it works like this all the way to root .
. failure is possible, hanging is not .
. the problem with that hope,
is that the lang depends on the OS:
it can be hard to ensure a pre-emptive OS,
if the os doesn't have a microkernel .]
What happens when a variable overflows?
Traditional programs often return
error codes or conditions,
will we now receive 2^N error codes
at the end of a run
and have to work through the entire array of problems?
[8.31:
. he wasn't listening to the compiler intro:
there are no overflows possible in this compiler .]
Debugging may increase in complexity
faster than the improved throughput delivers benefits.
Already most applications are
replete with bugs;
Reproducing and correcting the bugs
will become ever more difficult
because the context of different runs
may cause the pattern of data assignments
to processors to be slightly different
[8.31:
. is he assuming parasail's claims are baseless?
the whole point of the article
was to point out what a language needs
in order to avoid complexity during concurrency .
. what that voice really said was:
do you expect us to give up java?
we haven't even given c, or c++ yet!
that is a $trillion tool industry!!! ]

the author responds 7/28/2012 3:02 PM EDT:
The debugging challenge for parallel programming
is one of the main reasons ParaSail strives to
eliminate many sources of complexity,
including pointers, global variables, aliasing,
explicit lock/unlock and signal/wait,
and run-time exception handling.
Instead of run-time exception handling,
the compiler helps the programmer to ensure that
all possible error conditions are properly handled,
providing what might be called
"compile-time" exception handling .
No Explicit Threads, Lock/Unlock, Wait/Signal
Languages such as Java and Ada
that have some built-in support for concurrency,
traditionally have provided
the explicit notion of a thread or a task,
along with some mechanism for
synchronizing the threads,
using locks and signals of some sort.
In Ada, locks are associated with protected objects,
and locking and unlocking are automatic
as part of calling any operation
defined as part of defining the protected type.
In Ada, waiting and signaling are implicit in
special operations on protected objects called entries.
These operations explicitly specify
an entry barrier that must be true
before a caller of the entry is permitted to
execute the entry body.

By making the un/locking, waiting, and signaling
implicit in the language construct,
various synchronization errors are
automatically eliminated.
ParaSail takes this approach one step further.
As we have seen in the Word_Count example,
threads or tasks are themselves
implicit in the language .

In other respects,
ParaSail adopts a model similar to that of Ada,
where an object as a whole is either
designed for concurrent access or not;
only if a ParaSail object is a concurrent object
will simultaneous access by parallel computations be permitted.

A ParaSail object becomes concurrent
either by being an instance of a type that is
defined by a concurrent module,
or by having the concurrent qualifier
specified explicitly at the point the object is declared.
. When an individual object is declared as concurrent,
effectively what happens is
a concurrent module is implicitly created
to act as a wrapper of the specified
non-concurrent module defining the object.
No Race Conditions
. eliminate race conditions by construction .
A race condition is a situation in which
two concurrent computations
manipulate the same object
without adequate synchronization,
resulting in potentially unexpected
or undefined behavior.
. the no race conditions rule is implied by
the sum of these other rules:
No Parameter Aliasing section,
No global variables,
and the rules for concurrent objects.

. intentional race conditions can occur
only if some concurrent objects are created
and then manipulated concurrently;
otherwise, ParaSail is deterministic;
but, in a real-time or interactive environment,
determinism is already compromised
by the non-deterministic nature of the domain .
. the results will never be undefined
due to inadequate synchronization;
concurrent access is only permitted to
concurrent objects,
which have well-defined semantics
in the presence of concurrent callers.
No Pointers
[. adda calls this value orientation
in contrast to object orientation .]
. pointers interfere with concurrency's
divide-and-conquer approach .
If pointers are used to represent the
fundamental data structures,
cleanly dividing one half of a data structure
from another is not so easy.
The programmer may “know”
that the structure is a binary tree,
but what happens if there is actually some
sharing happening between parts of the tree?

Is it safe to send one thread off to
update the left “half” of the tree
while simultaneously sending another
to update the right “half,”
if there is some possibility of them
meeting up somewhere later
in the middle of their updates?

So how does ParaSail avoid pointers?
If we look back on the sections above,
we see that ParaSail is a flexible language
with a familiar class-and-interface-based oop model,
but it has no need for pointers.

The region-based storage management model,
the availability of a null value for any type,
the ability to assign a non-null value
into a previously null component (or vice-versa),
makes it possible for objects to grow and shrink
over their lifetime without any explicit use of pointers.

Other ParaSail features we have not discussed above,
such as the uniform ability to define how the
indexing and slicing operations (A[I] and A[I..J])
work for any container-like type,
mean that constructs like directed graphs
are easily represented in ParaSail without pointers.

The graph would be a container object,
a node identifier would be used for
indexing into the graph container,
and edges in the graph would be represented by
pairs of node identifiers.

If an “indexing” operator is defined as above,
then we can use the A[I] notation
with objects of a type defined by the given module.
Conclusion
ParaSail’s region-based,
pointer-free data structuring model
makes it easy to create data structures that
naturally support a divide-and-conquer approach,
and the checking provided at compile time
eliminates many of the run-time failures
and race conditions that can dramatically
slow down the development and testing
of a complex, parallel application.
ParaSail blog:

Why design a new programming language?
I[Taft] still believe that a well-designed language
can result in more productive programmers
building higher quality software.
This new language is meant to address
the goals of producing inherently
safe and secure software,
while taking advantage of the wider availability of
true parallel processing in the form of multi-core chips.
It is intended to promote a formal approach to software,
where the program text includes pre- and postconditions,
liberal use of assertions and invariants, etc.,
with tool-supported proof of correctness
with respect to the formal annotations.
The language is tentatively named ParaSail,
for Parallel Specification and Implementation Language.
I would have spelled it "ParaSAIL"
but for the danger of confusion with the original
Stanford AI Language, "SAIL,"
and its more modern follow-on "MAINSAIL"
(for Machine Independent SAIL).
I don't mind making the connection with SAIL,
as it was a very interesting language in its day,
and MAINSAIL remains worth a look today.
ParaSail is a completely new language,
but it steals liberally from other programming languages
, including the ML series (SML, CAML, OCAML, etc.),
the Algol/Pascal family (Algol, Pascal, Ada,
Modula, Eiffel, Oberon, etc.),
the C family (C, C++, Java, C#),
and the region-based languages (especially Cyclone).
Perhaps one significant deviation from the excellent baseline
established by SAIL, ML, Eiffel, Java, etc.
is that ParaSail is intended to avoid
"fine-granule" garbage collection
in favor of stack and region-based storage management.
philosophy behind ParaSail:
. ParaSail tries to minimize implicit occurrence of
operations, parameters, initializations, conversions,
dynamic binding (virtual function calls), .. .
This is both in the name of clarity for the human reader,
and in the name of
formal testability and verifiability.
On the other hand,
ParaSail allows many things to proceed in parallel by default,
effectively inserting implicit parallelism everywhere.
Parameter evaluation is logically performed in parallel.
In all cases, the language disallows
code that could result in race conditions due to
inadequately synchronized access to shared data,
either by using per-thread data,
structured safe synchronization,
or a handoff semantics (similar to that of linear types,
distributed languages like Hermes,
or the UVM virtual memory system).
Of course much of this implicit parallelism
is possible in pure functional languages,
and ParaSail will support a functional programming style
where it works naturally.
Unfortunately, doing some relatively
straightforward things in pure functional languages
can require mind-bending (for me) concepts like monads,
while a good old assignment statement
is something that most programmers understand.
With apologies to the political world,
ParaSail will try to make assignments statements
safe, legal, and rare.
ParaSail described to AdaEurope:
    Implicit parallelism
        Parameters evaluated in parallel with "hand-off" semantics,
        "for" loops unordered by default,
        must work to force explicit sequencing between statements;
        Can request explicit parallelism with "||" and "concurrent loop"
    Both Lock-free and Lock/Queue-based concurrent data structures
        Operations on concurrent data structures
presumed unordered by default;

        Can use "dequeue conditions"
to control ordering for queued operations;

        Can wait simultaneously on multiple queued operations,
        selecting first one that is ready to be dequeued to proceed.
    Small number of concepts:
        Module, Type, Object, Operation
        You get a Type by instantiating a Module (all Modules are "generic").
        You get an Object by instantiating a Type.
        An Operation takes inputs and produces outputs;
no up-level variables

            Operation names generally usable without any prefix,
            presuming some input or output is of type defined by
            module enclosing operation definition.
        Nesting of entities uses distinct syntax:
            type::nested_entity
            object.component
            object.operation(...) equiv to operation(object,...)
    No global variables and no aliasing of (non-concurrent) variables
        Read-write access only via parameters;
        "Context" parameter provided to
        gain access to operating system, database, user, etc.
        Compiler prevents aliasing between parameters
using "handoff" semantics.

    Encourages formal approach to software
        Preconditions, Postconditions, Assertions,
        Subtype constraints all use consistent syntax:
            {boolean_expression}
            c.f. {P}S{Q} in Hoare logic
        Compile-time enforcement of assertions
and all other language-defined "checks"
            no run-time exceptions to worry about.
        [[Expr]] notation (c.f. denotational semantics)
        used to define semantics of operations in terms of "universal" types.
    Minimal need for pointers:
        Generalized containers support indexing and aggregate syntax
            A[I], [X, Y, Z], ["abc" => M, "def" => N]
        Expandable objects with optional back/encloser references
        Pointers only to stable or concurrent objects
        Safe region-based/object-based storage management.
    Five kinds of literals, all usable with user-defined types.
        Integer, Real, Character, String, and Enumeration.
        Corresponding Univ_XXX type for each kind of literal
with full run-time semantics.
        Syntactically distinct from other names used for entities
            42, 3.1459, 'X', "Hello", #red
        User-defined types can use literals
            provide conversion operation from Univ_xxx type
to allow use of literals

            provide conversion operation to Univ_xxx
to allow "[[...]]" denotational semantics notation.
    Declarations syntactically distinguished from statements
        Allows intermingling of statements and declarations within a block
        var X [: T] [:= Expr];
        const K [: T] := Expr;
        type T is [new] Queue;
        function F(A : P; B : Q) -> R;
        [abstract] [concurrent] interface Queue is ...
-- site:adacore.com/ AdaEurope_ParaSail_2010.pdf

parasail vs other concurrency tech:
. Khronos-Apple`OpenCL is the
hardware-independent alternative to NVIDIA`CUDA
for general purpose parallel processing (GPGPU)
. Cilk and OpenCL seem to be emerging as
two important, rather distinct approaches
to parallel programming.
Cilk makes it easy to spawn threads off
to compute an arbitrary expression,
and then uses a set of worker processes to service the threads,
using the approach we discussed in an earlier post,
where threads spawned by a given worker
are serviced LIFO (last-in, first-out -- stack-like)
but when a worker runs out of threads,
it steals from other workers using a FIFO
(first-in, first out, customer-waiting-line) strategy.
OpenCL, on the other hand, is focused on
data parallelism, [ applying Y = f(X)
where X,Y are arrays,
and f is applied to each item of the array .]
-- the SPMD (Single Program, Multiple Data) approach
fostered by the Connection Machine folks.

In some ways, Cilk and OpenCL
can be seen as lower-level languages:
# in Cilk:
the programmer has to identify
where threads should be spawned .
# in OpenCL:
the programmer has to [identify each f,
and launch each Y = f(X) .]

ParaSail on the other hand,
[designs the language so that compiler
can figure out your algorithm's concurrent .
thereby offering greater programmer productivity]

One of the key advantages that ParaSail provides
is that there is no hidden aliasing,
unlike in C, C++, Java, etc.,
where aliasing is everywhere.
(Cilk and OpenCL are both
piggy-backed on C/C++;
various threading APIs are available to
Java, C#, Python, etc.)
ParaSail's rules make it dramatically easier
for a compiler or run-time to automatically
partition computations into [concurrencies] .

Furthermore, the ParaSail compiler
detects all race conditions at compile time,
has no exceptions,
allows memory to be partitioned into
non-overlapping regions, etc.,
which simplify both the programmer's model
and the process of automatic parallelization.
first complete draft of ref'man 2011.05
. the first complete draft of the reference manual
(among several other resources)
for the ParaSail programming language is available
at the ParaSail newsgroup .