ATSMP - Advanced Type Systems for Multicore Programming

January 2012 to June 2014
Funded by: 
FCT (PTDC/EIA-CCO/122547/2010)
Principal Investigator: 
Vasco T. Vasconcelos

Even though multicore machines now lay on our desks and laps, software construction has failed to keep the pace with the advances in hardware. Current programming languages were conceived for sequential and centralized programming. Concurrency primitives, when available, were added as an afterthought. Challenged by this state of affairs, a number of programming languages have been either adapted or designed from scratch. In the former category we find ML, Haskell, Scala and Cilk, increasingly sophisticated concurrency Application Programming Interfaces (API) for Java and C#, and standard APIs for C, C++ and Fortran, such as OpenMP and MPI. Examples in the latter include Chapel, Fortress, and X10 (the outcome of DARPA's High Productivity Computer Systems project), as well as Erlang.

The above languages either exhibit strong, sophisticated type systems but poor support for high-level concurrency (ML, Haskell, Java, C#, Scala), or else present some form of concurrency support backed up by poor to absent type abstractions (Cilk, OpenMP, MPI, Erlang). Examples of high-level concurrency primitives and idioms include software barriers, clocks, phasers and work stealing techniques. These are in direct opposition with low-level primitives such as locks, monitors or futures.

Endowed with the hardware and the lower software levels (operating systems, standard APIs for system's programming), and with concurrency idioms and abstractions, we are left with very little support to "get concurrency right". Among the sources for this problem, we highlight the facts that a) programmers cannot easily express the program properties they have in mind, and b) they are not equipped with tools that help in certifying these properties.

The thus identified problem must be attacked from multiple directions, including rigorous language specifications (opening the possibility for formal reasoning about programs), static analysis methods (usually incorporated in compilers or in tools to be run on source code before deployment), and runtime monitoring (where program invariants are checked while applications execute). The challenge here is to statically make sure that components (e.g., threads, concurrent objects, or processes) safely cooperate while using the given concurrency abstractions.

This project concentrates on the development of new concurrency abstractions, together with the associated static analysis methods. We build on our past experience on the development of type systems for concurrency, including singleton, session, and assertion type systems, and we aim at advanced type systems able to combine three properties: expressivity, ease of use, and decidability (in particular good integration with property verification systems, Satisfiability Modulo Theories provers). The expected results include the proposal of concurrency abstractions, formal proofs of their properties, implementation (in compilers) of the associated static analysis tools, the assessment via benchmarking of the theories and tools developed.