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.

• João Costa Seco (Coordinator)
• Carla Ferreira
• Hugo Torres Vieira
• José Pacheco
• Luis Caires