Project StreamLine

Objectives of the project

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.

Research Team

• João Costa Seco (PI)
• Luís Caires
• Carla Ferreira
• Hugo T. Vieira
• Nuno Parreira (MSc - Out 2010 - Apr 2011)
• Miguel Lourenço (MSc - Out 2010 - Sep 2011) (PhD Out 2011 - … )

• Paulo Ferreira (MSc - Out 2011 - … )

• Sérgio Silva (MSc - Out 2011 - … )

Publications

1. Publicado - Luís Caires, Carla Ferreira, and António Ravara. A simple proof system for lock-free concurrency. In International Workshop on Proof Systems for Program Logics (PSPL), 2010.
2. Em Preparação - Luís Caires and João Costa Seco. Dynamic control of interference. Technical Report DIFCTUNL-5-2010, CITI / DI-FCT-UNL, December 2010.
3. Submetido - Ricardo J. Dias, Dino Distefano, João M. Lourenço, and João Costa Seco. StarTM: Automatic Verification of Snapshot Isolation in Transactional Memory Java Programs. Technical Report UNL-DI-6-2011, Departamento de Informática FCT/UNL, 2010.
4. Concluído - Luís Miguel Lourenço. Implementação de uma linguagem intermédia e máquina virtual para linguagens concorrentes. Master's thesis, 2011.
5. Publicado - Luís Miguel Lourenço, João Costa Seco, and Francisco Martins. Linguagem Intermédia Tipificada para Máquina de Pilha Concorrente com Objectos. In InForum, 2011.
6. Publicado - Filipe Militão, Jonathan Aldrich, and Luís Caires. Aliasing control with view-based typestate. In Formal Techniques for Java Programs FTfJP'10, 2010.
7. Concluído - Nuno Parreira. Implementação de um algoritmo de tipificação para linguagem concorrente com tipos comportamentais. Master's thesis, 2011.
8. Aceite - Cátia Vaz and Carla Ferreira. On the analysis of compensation correctness. Journal of Logic and Algebraic Programming.
9. Publicado - Typing Dynamic Roles in Multiparty Interaction. P. Baltazar, V. T. Vasconcelos, and H. T. Vieira. In InForum, 2011.

Prototypes

• Interpretador e Sistema de Inferência de tipos
• Plugin eclipse para a linguagem de programação
• Linguagem Intermédia Tipificada e Máquina virtual
• Compilador para a linguagem intermédia