Seminars & Visitors

Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties. We present a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that any functional correctness property proven for a choreography also holds for its compiled implementation.

There is no abstract becaue otherwise it wouldn’t be surprising, and it wouldn’t be a mystery.

Data breaches are prevalent. We provide novel insights into individuals’ awareness, perception, and responses to breaches that affect them through two online surveys: a main survey (n = 413) in which we presented participants with up to three breaches that affected them, and a follow-up survey (n = 108) in which we investigated whether the main study participants followed through with their intentions to act. Overall, 73% of participants were affected by at least one breach, but participants were unaware of 74% of breaches affecting them. While some reported intention to take action, most participants believed the breach would not impact them. We also found a sizeable intention-behavior gap. Participants did not follow through with their intention when they were apathetic about breaches, considered potential costs, forgot, or felt resigned about taking action. Our findings suggest that breached organizations should be held accountable for more proactively informing and protecting affected consumers.

Fabrizio and Lovro will be informally presenting several papers that will appear at DisCoTec 2023.

Serverless computing is a Cloud development paradigm where developers write and compose stateless functions, abstracting from their deployment and scaling. In this seminar, we introduce some of the essential elements of serverless platforms and focus on the challenges of configuring and developing serverless systems. We discuss how languages at different levels of the implementation stack can help in dealing with those challenges and present the concrete example of a declarative language we recently introduced to tackle the problem of optimising the scheduling of function execution.

We discuss the challenges of choreography projection and some ideas to improve the state-of-the-art to support news classes of recursive choreographies without resorting to `repair’ techniques that introduce extra communications to make choreographies projectable e.g., amendment. Key to the improvements explored in this talk is the investigation of a semantic characterisation of projection and merging rooted in behavioural theory. This semantic characterisation provides a context for studying concrete syntactic realisations i.e., projection procedures. As an example, we show how a new class of recursive choreographies can be projected leveraging a few classical bisimilarity laws.

The π-calculus, viewed as a core concurrent programming language, has been used as the target of much research on type systems for concurrency. In this paper we propose a new type system for deadlock- free session-typed π-calculus processes, by integrating two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom by forbidding cyclic process connections. The second is Kobayashi’s approach in which types are annotated with priorities so that the type system can check whether or not processes contain genuine cyclic dependencies between communication operations. We combine these two techniques for the first time, and define a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities. This can be seen in three ways: (i) as a new linear logic in which cyclic structures can be derived and a Cycle-elimination theorem generalises Cut-elimination

Continuous queries over data streams often delay answers until some relevant input arrives through the data stream. These delays may turn answers, when they arrive, obsolete to users who sometimes have to make decisions with no help whatsoever. Therefore, it can be useful to provide hypothetical answers - “given the current information, it is possible that X will become true at time t” - instead of no information at all. In this talk we present a semantics for queries and corresponding answers that covers such hypothetical answers, together with an online algorithm for updating the set of facts that are consistent with the currently available information.

We present Hypersequent Classical Processes (HCP), a revised interpretation of the “Proofs as Processes” correspondence between linear logic and the π-calculus initially proposed by Abramsky [1994], and later developed by Bellin and Scott [1994], Caires and Pfenning [2010], and Wadler [2014], among others. HCP mends the discrepancies between linear logic and the syntax and observable semantics of parallel composition in the π-calculus, by conservatively extending linear logic to hyperenvironments (collections of environments, inspired by the hypersequents by Avron [1991]). Separation of environments in hyperenvironments is internalised by ⊗ and corresponds to parallel process behaviour. Thanks to this property, for the first time we are able to extract a labelled transition system (lts) semantics from proof rewritings. Leveraging the information on parallelism at the level of types, we obtain a logical reconstruction of the delayed actions that Merro and Sangiorgi [2004] formulated to model non-blocking I/O in the π-calculus. We define a denotational semantics for processes based on Brzozowski derivatives, and uncover that non-interference in HCP corresponds to Fubini’s theorem of double antiderivation. Having an lts allows us to validate HCP using the standard toolbox of behavioural theory. We instantiate bisimilarity and barbed congruence for HCP, and obtain a full abstraction result: bisimilarity, denotational equivalence, and barbed congruence coincide.

Implementations of choreographic models use message routing technologies distant from their related theoretical models (e.g., CCS/π channels). This drives implementers to mediate discrepancies with the theory through undocumented, unproven adaptations, weakening the reliability of their implementations. We present a framework of Applied Choreographies (AC) where programmers write choreographies in a language that follows the standard syntax and semantics of previous works. Then, choreographies are compiled to a real-world execution model for Service-Oriented Computing (SOC). To manage the complexity of this task, our compilation happens in three steps, respectively dealing with: implementing name-based communications using the concrete mechanism found in SOC, projecting a choreography to a set of processes, and translating processes to a distributed implementation in terms of services.

Presentation to the Concurrency and Logic group, covering previous work on Constraint Programming and portfolio solvers, Cloud deployments, and DevOps practices.

Presentation of Cho-Reo-graphies (CR), a model where choreographies are parametric in the (Reo) connectors through which parties communicate. CR is the first choreography model where different communication semantics (e.g., synchronous and asynchronous) can freely be mixed in the same choreography. We prove that if a choreography respects the rules of the connectors that it uses, then the process implementation that we can synthesise from it enjoys deadlock freedom.

In modern software systems, deployment is an integral and critical part of application development. A natural question arises: to what extent can we automate the deployment of complex, distributed, and scalable software systems? In the first part of this talk, we will try to give an answer to this question providing some insights on the complexity of the problems of dealing with application deployment and describing tools that can be used. We then describe a recent approach to take into account deployment at the modeling level, thus allowing to perform deployment conscious decisions during the early stages of a system development.

Timed automata, and machines alike, currently lack a general mathematical characterisation. We introduce a uniform coalgebraic understanding of these devices. This framework encompasses known behavioural equivalences for timed automata and paves the way for the extension of these notions to new timed behaviours and for the instantiation of established results from the coalgebraic theory as well. Lax functors are the cornerstone of the framework: they allow us to model time flow as a context property and hence offer a general and expressive setting where to study timed systems. In this setting the index category encodes “how step sequences form executions” (e.g. whether steps duration is accumulated or kept distinct) whereas the base category encodes “step nature and composition” (e.g. non-determinism and labels). Finally, we develop the notion of general saturation for lax functors and show how equivalences of interest for timed behaviours are instances of this notion. This characterisation allows us to reason about the expressiveness of said notions within a uniform framework and organise them in a spectrum independent from the behavioural aspects encoded in the base category.

Transactional memory (TM) has emerged as a promising high-level concurrency control mechanism alternative to fine grained lock-based synchronization. However, most TM models admit only isolated transactions, which are not adequate in multi-threaded programming where transactions have to interact via shared data before committing. We present Open Transactional Memory (OTM), a programming model supporting safe, data-driven interactions between composable memory transactions. In this model, different transactions are transparently merged at runtime as soon as they access to shared variables; their threads can then cooperate, until they all either commit or abort together. Thus, this model relaxes the isolation requirement still guaranteeing atomicity; moreover, it allows for loosely-coupled interactions since transaction merging is dynamic and driven only by accesses to shared data, with no need to specify participants beforehand. We present OTM in the setting of the Haskell language, taking advantage of its type system for guaranteeing composability.