Our research focuses on the theory and practice of models, languages, and tools for the development of concurrent systems, i.e., systems where multiple computations are executed in parallel and can interact with each other.
Concurrent systems are pervasive. We can find trends both on the level of a single computer and on that of, naturally, computer networks.
Even in a single computer, user workflows may require the coordination of many software applications to reach an overall goal. Examples are: major web browsers seamlessly incorporate the functionalities of other applications to display content not defined with web standards (e.g., PDF viewers); in some scenarios, changes to a filesystem have to be communicated by e-mail to users; and, modern operating systems have supervising processes that load and unload resource-hungry services on demand.
Scaling to multiple computers, the rise of computer networks has enabled the development of innovative solutions based on the composition of services running in separate computers.
Examples are: different companies can programmatically define their respective business processes and integrate them to engage in electronic commerce; sensor networks can be coordinated by data centers to collect and share information, in order to monitor environments or offer services to citizens in smart cities; users can access web-based services regardless of their location and with different devices.
The two trends that we described above are challenging because they go beyond the barrier of software applications with a single point of control. Instead, programmers are now confronted with systems where multiple applications run concurrently, have their own data but may also share it by interacting, and are deployed on independent execution units.
This setting made it evident that the mature methodologies designed for the development of sequential (non-concurrent) software have to be re-evaluated and potentially replaced, as they do not deal with the typical problems that arise from concurrent systems.
In this group we are particularly interested in three macro-areas: productivity, integration, and correctness.
In concurrent systems, the order in which communications are performed among different components is the key to implementing software requirements.
For example, a web application may require that a user has to authenticate itself (login) before being able to change some content in a server;
or, an E-Commerce system should send a product to a client only after it received some money from a bank.
The order in which communications should be executed is usually not explicit in software: it is implemented by means of bookkeeping variables in, e.g., session data structures (as in PHP) or objects (as in JavaEE).
This makes programming error-prone and complicated, as these bookkeeping variables are accessed concurrently (race conditions) and it is hard to see whether their usage actually implements the requirements when there are many communications involved.
In contrast to this, our aim is to make the structure that communications have to follow explicit in our tools, providing developers with native programming primitives for the ordering of communication actions that can be easily mapped to informal requirements such as those described above.
Concurrent systems are usually heterogeneous: different components, or services, are implemented with different technologies that are best suited to their respective tasks.
One of the holy grails of development tools for such systems is therefore the ability to build and compose components as black boxes:
it should be possible to compose components by referring only to their interfaces, abstracting from their respective internal implementations and the technologies they are built with.
There are two main obstacles to reaching this objective.
The first obstacle is that of communication mediums among components: different components may use different communication mediums, e.g., TCP/IP sockets or Bluetooth channels.
The second obstacle is that of data formats: each component may use a different representation of data, e.g., XML, JSON, or efficient binary formats.
These two obstacles can easily lead to unmaintainable spaghetti code, as the developer has to deal with multiple ways of communicating data and the transformations among different data formats.
We are interested in frameworks that allow programmers to abstract from specific data formats, by providing automatic transformations and compatibility layers among different technologies. Ideally, concurrent programs developed for using one specific communication technology should not need to be changed when replacing said technology with another one.
In concurrent systems, the typical interfaces for composition -- e.g., data types, object types, or remote procedures -- are unsatisfactory, because they do not deal with the coordination of independently running components. More specifically, this is because these abstractions do not deal with the critical aspects of concurrency: the order in which communications are performed. Getting the order of communications wrong in a complex system is easy and can have catastrophic consequences, such as crashes (due to race conditions) or complete system blocks (e.g., due to deadlocks).
In general, concurrent systems are inherently more complicated to analyse due to the many possible interleavings of actions performed by separate actors.
Moreover, even though there is a general agreement that it is useful to specify how communications should proceed in a system by defining protocols, there is little to no tool support helping programmers to actually guarantee that their software correctly implements such protocols.
These aspects make it difficult to check whether some concurrent software is free of bugs.
We are interested in developing methodologies for accurately defining communication protocols and ensuring that they are correctly implemented by software. We then investigate how these methodologies, which make the behaviour of a program clearer, can be used to guarantee general and desirable safety properties such as freedom from deadlocks.
Our main approach is using high-level descriptions of protocols as new forms of types or language primitives, defining interfaces for composition where communications are first-order citizens.
The group is involved in the research and development of the following major software projects:
- The Jolie programming language: a language and framework for the development of concurrent systems, focusing on productivity and integration.
- The Chor programming language: a language for the development of correct concurrent software.
Topics of Interest
- Business processes
- Choreographic programming
- Data transformation
- Frameworks and tools for developing concurrent software
- Logics for communications
- Network protocols
- Process calculi
- Session types
- Web services and applications
The group actively collaborations with many international partners, among which:
- INRIA (France)
- Imperial College London (UK)
- italianaSoftware s.r.l. (Italy)
- IT University of Copenhagen (Denmark)
- New University of Lisbon (Portugal)
- Technical University of Denmark (Denmark)
- University of Bologna (Italy)