ParaSail -- A new language for race-free parallel programming

This presentation will provide an introduction to ParaSail. ParaSail is a new programming language which is designed 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 compile-time checks of correctness with respect to the formal annotations. A blog on the design of ParaSail can be found here:
http://parasail-programming-lang...

The language is named ParaSail as an acronym for Parallel Specification and Implementation Language. ParaSail is a new language, but it borrows concepts from other programming languages, including the ML/OCaml/F# family, the Lisp/Scheme/Clojure family, the Algol/Pascal/Modula/Ada/Eiffel family, the C/C++/Java/C# family, and the region-based languages (especially Cyclone). A significant deviation from the excellent baseline established by ML, Eiffel, Java, Scala, etc. is that ParaSail attempts to dramatically simplify the model where possible, with only four basic concepts, modules, types, objects, and operations. ParaSail omits pointers, exceptions, and garbage-collection in favor of stack/region-based storage management. A second major deviation from the above-named language families is that ParaSail is inherently parallel. The programmer has to work harder to force sequential evaluation. By default, evaluation proceeds in parallel for essentially all constructs. And finally, in ParaSail, all checking is done at compile-time. A ParaSail program is rejected by the compiler if it cannot prove there are no race-conditions, no use of uninitialized variables, no out-of-bound array references, no null-pointer dereferences, no numeric overflows, etc.

This presentation will provide examples of the features of ParaSail, compare and contrast it with other existing languages, and discuss the rationale behind the choices made in its design. We will also describe the ongoing implementation activities, including the development of a prototype compiler and a ParaSail Virtual Machine to support the spawning of hundreds or thousands of pico-threads during execution.