Projects •
Static Verification of Safe Parallelism
Full Title
Static Verification of Safe ParallelismDescription
The project, that celebrates a formal collaboration between Rice University from USA and University of Lisbon from Portugal, under the FLAD/NSF 2015 Portugal-U.S. Research Networks Program, will focus on compile time verification of programs written on the Habanero Java (HJ) programming language, that is being being developed at Rice University as an extension to the original Javabased definition of the X10 language.
In particular, the research team plan to study the impact of the various HJ’s concurrency primitives on the expected properties of parallel programs.
The properties we are interested in include the following:
- Deadlock freedom A program is free from deadlocks if no computation leads to a situation where a subset of the tasks are waiting for one another, in a circular fashion.
- Data-race freedom A program is free from data races if no computation leads to a situation where one task is trying to write on a variable, while a different task is trying to access (read or write) the same variable.
- Determinism A program is deterministic if all runs of a program lead to a common outcome.
- Serializability A program is serializable if it can be converted to an equivalent sequential program.
The HJ’s concurrency primitives we are interested in include the following:
- Finish The finish primitive causes a new task to execute and then waits until all tasks created within the task have completed.
- Phasers A phaser allows a group of tasks to synchronize ensemble repeatedly. Phasers can also be used for producer-consumer style computations where producer tasks need not wait for consumer tasks (which wait for each other).
- Futures A futures defines a way for a program to schedule a parallel computation, and a way for a program to await the termination of this scheduled computation, retrieving its output.