Project Objectives

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. 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.