StreamLine - Thread-Safety by Typing for Mainstream Concurrent Object-Oriented Programming
Jan 2010 - Dec 2012
As shared-memory multi-threaded programming is becoming pervasive it is crucial to conceive enhanced, yet easy to use,
programming tools allowing programmers to take full advange of multi-processors.
The goal of our project is fairly focused: to develop a Java-like concurrent programming language, stripped down to key object-
oriented features, but equipped with a flexible type system and constructs supporting the efficient static verification of
multithreaded programs with fine-grain, monitor-based, dynamic concurrency control. The programming environment will besupported by a suitable runtime system compatible with a mainstream environment such as Java SDK. How are we to approach
this challenge, and what would be new about it?
True, concurrent programs seem to be so difficult to get right now as decades ago, even for competent programmers. Concurrent
programming is inherently difficult, and many approaches to simplify and reason about concurrent programming have been
proposed for decades. However, the approach we intend to explore in this project is fresh, leveraging on foundations previously
developed by the team on spatial-behavioral type systems.
Since the early phases of concurrent programming research, fundamental questions started to get sensible answers, such as what
synchronization primitives one might consider (e.g., locks, conditions), how should one reason about shared memory programs
(e.g., invariants, rely-guarantee), what abstractions one may want to adopt in a high-level programming language design (e.g.,
monitors, futures, threads). Most of these concepts have strongly influenced the whole field of research until now, but the
underlying questions keep motivating now more than ever many fundamental and applied developments (see e.g. [28, 19]).
Unfortunately, clean programming language abstractions developed for shared variable concurrency did not sneak into the
mainstream, unlike, say developments on data and object types, such as polymorphism and generics [13]. Programmers tend to
think too much in terms of lock aquisition and control flow, rather in terms of behavioral, spatial separation, and ownership
invariants, as highlighted long time ago by Hoare [24]. This focus on ownership control and spatial separation have been recently
reintroduced by systems researchers such as Doug Lea (author of java.util.concurrent), programming language researchers such
as Reynolds [32], O’Hearn [29], and ourselves, as captured by spatial logics for concurrency and related notions of typing [2, 1].
The key idea (our magic wand) to explore in this project is the introduction of type operators able to express fine-grained
dynamic concurrency control constraints on objects, seen as resources, by combining parallel, sequential, sharing, and ownership
type operators. Sequential operators have already been introduced in types for object oriented languages (cf. session types [25]),
and allow the static validation of protocols of resourceful objects, such as files, linear cells, etc. We want to go much beyond: the
possibility of freely defining parallel/sequential usage protocols for objects is specific to our approach, and brings a surprising
degree of expressiveness, in particular
when combined with dynamic ownership types. Ownership transfer types allow the programmer to express fine grained sharing
constraints on object references, and enable the type system to statically check complex scenarios of aliasing and object reference
delegation, as present in real concurrent OO programs. Using our approach, it is possible to convey at the interface level usage
patterns of objects that are either difficult or impossible to capture with existing approaches. Consider a Future java object, where
the get() and cancel() methods are certainly not supposed to be called by the same calling thread. For another example, the type
of an sequential hash table is the same as a thread-safe hash table (using a monitor), enabling a sequential hash table to be
used (unsafely) in a concurrent context. Our type system forbids these kinds of errors, and others, such as interferences, races,
usage protocol violations, and dangling references, in a uniform way.
To achieve our goals, we will build on the team’s previous experience on spatial logics and type systems (Caires, Vieira), type
systems for components and objects (Caires, Vieira, Seco), transactions (Ferreira), and compiler implementation (Seco, Caires),
counting with the collaboration of internationally leading teams (in the project topics) headed by our consultants Peter O’Hearn at
Queen Mary University London, and Sophia Drossopoulou at Imperial College London. We expect the concrete results of the
project to produce a substantial impact, given the combination of theoretical advances with the delivery of a public-domain
implementation of a compiler-runtime system prototype it provides.
The core theme of this project is to provide programming language constructs and program verification techniques and tools for
race-free multithreaded programming by construction. We focus on the object-oriented paradigm as a model where objects are
shared resources and object types are contracts that discipline their usage. This model can be instantiated in several settings such
as a multithreaded object-oriented language, a typed service oriented language, or a distributed object calculus.
In our proposal, we aim at defining behavioral types for objects based on spatial logic operators to specify which views of
objects may be used independently (i.e. sets of methods that do not interfere and can be called concurrently), which parts of the
objects’ behavior must be used in sequence (there is causal dependence between method calls), and which parts of the object can
be referred exclusively and delegated to others without any further synchronization (ownership). One goal is to define type
systems with spatial operators that can be freely combined to express complex object behaviors and synchronization patterns. We
also foresee that extra flexibility can be added to this type system by means of a rich subtyping relation between behavioral types. In this subtyping relation, interleaving of concurrent behaviors is captured by an universal subsumption law and the explicit
synchronization of threads by language constructs can be seen as an explicit type coercion from a sequential to a concurrent
behavior. Furthermore, we propose to explore the interactions between behavioral typing and several concurrency control
mechanisms such as synchronized and shared methods (locks), monitors, and software transactional memory systems [19]. We
also propose to address some open issues such as the semantic integration of transactions in object-oriented languages, focusing
on the integration of transactions with exception handling constructs, and the behavior of nested transactions.
