T1: Experimenting with ParaSail – Parallel Specification and Implementation Language

Monday morning
S. Tucker Taft, SofCheck, Inc.

 

This tutorial will provide a chance to experiment with a new language designed to support the safe, secure, and productive development of parallel programs. ParaSail is a new language targeted at safety-critical and high-security systems development in a “multi-core” world, with pervasive parallelism coupled with extensive compile-time checking of annotations in the form of assertions, preconditions, postconditions, etc. ParaSail does all checking at compile time by incorporating an advanced static analysis engine, allowing it to eliminate race conditions, null dereferences, uninitialized data access, numeric overflow, out of bounds indexing, etc. as well as statically checking the truth of all user-written assertions.

The tutorial will begin with a short introduction to the language. After that, the attendees will receive a prototype ParaSail compiler and an accompanying ParaSail Virtual Machine interpreter for writing and testing ParaSail programs. A set of sample programs will be provided as a starting point for experimentation. The tutorial/workshop will finish with a group discussion and feedback on the experience of using this new language, and ideas about next steps.

Level

The tutorial includes an introduction to the language. No specific prerequisites other than an interest and ability in learning a new language, plus a basic understanding of parallelism, assertions, preconditions and postconditions.

Reasons for attending

This is a chance to experiment with a new programming language oriented around parallelism and formal verification. The language is still in development, so it is also an opportunity to help improve and refine the language, and perhaps gain some insights that might contribute to other language design efforts.

Short Biography

The presenter has been involved with language design since 1975, and with Ada since 1980. He was the technical lead for the design of Ada 95, and was heavily involved in the design of Ada 2005 and the ongoing design of Ada 2012. In addition to language design, the presenter has been the technical lead on the development of an Ada 83 and an Ada 95 compiler, as well as of an advanced language-independent static analysis technology.