Authored by Roland Kuhn, from Actyx, and Carla Ferreira, João Costa Seco, from NOVA University Lisbon
This year’s 37th European Conference on Object-Oriented Programming was held in Seattle (USA — with the exception of the 4th ECOOP in Beijing and the 26th ECOOP in Ottawa it is usually held in Europe). From the TaRDIS consortium there were three papers accepted, plus one tool demonstration at the collocated ISSTA conference (with a focus on testing and analysis). Hence, we travelled to the state of Washington to attend the conference and give presentations.
The first one was about Behavioural Types for Local-First Software, including TaRDIS work as well as fruits of the BehAPI EU project (Horizon 2020 RISE). This paper describes how to tie together a global workflow specification (here called swarm protocol ) with the local implementation of business logic on members of a heterogeneous swarm — you may picture this as a peer-to-peer system with no central database, message broker, or other coordination. The ISSTA tool demonstration was about an implementation of the paper’s theory that allows a programmer to immediately see whether their code correctly implements the workflow’s part played by a single device, so that when all parts work together the whole process will run as designed, even though all devices act in full autonomy.
Next, it was the time for the paper Hoogle*: Synthesis of Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution by Henrique Guerra, João Costa Seco and João Ferreira that was the result of Henrique’s Master Thesis developed in the GOLEM project. Hoogle* is a program synthesiser for Haskell that starts with a type-based description for the desired piece of code and some input/output examples, it then produces an actual program that fulfils the expectations. Program synthesis is a really flexible technique that can be applied in TaRDIS to automatically generate parts of code given high-level specifications provided by the developers of integrated ML mechanisms.
The last TaRDIS paper was about fully automated verification of replicated data types (RDTs). These data types are crucial components for the development of distributed systems that operate over geo-replicated databases under weak consistency. Relaxing consistency is needed to ensure high availability and low latency. The disadvantage is that state convergence is hard to guarantee due to concurrent update conflicts. Enter RDTs, which resemble sequential data types but embed conflict resolution mechanisms that ensure convergence. The issue is that designing RDTs is challenging as their correctness depends on subtleties such as the ordering of concurrent operations. The paper proposes a high-level programming language with fully automated proof capabilities that can be transpiled to mainstream languages. This work is a step towards the correctness-by-design approach proposed by TaRDIS, by delivering a tool that supports developers in implementing correct RDTs.
Overall, the ECOOP crowd seemed a little thinned out due to the remote location, but we met many familiar faces. And most importantly, there was inspiring progress on multiple fronts. Sophia Drossopoulou used her keynote (congratulations to the Dahl-Nygaard prize!) to give a sneak preview of her upcoming work on actually putting software modules to work in ensuring security properties, like preventing untrusted code from subverting a trusted object’s guarantees. Then there was good news on compositionality of choreographies and their modular compilation presented by Eva Graversen, moving another inch towards the ability of using distributed systems as building blocks of larger distributed systems without losing all correctness properties. Petar Maksimović presented work on Exact Separation Logic, which will help in figuring out whether a system behaves as you want without rejecting correct ones nor accepting incorrect ones (of course some will not be decidable). Magnus Madsen spoke about a precise way of accounting for the possible set of variants an enumeration can have at a given location in the program, which would be really interesting to consider adding to the Rust language — because sometimes it is statically known that an optional value is indeed present.
Collocated with ECOOP was — among others — the VORTEX workshop. Here, it was a surprise to learn that a group of researchers mostly from Italy has recently developed a theoretical framework called Aggregate Computing for analysing the qualities of homogeneous swarm systems, offering a similar system model to what TaRDIS requires, i.e. devices can come and go, a single device may be unreliable but the overall swarm should be reliable.
Another surprise was that multiple attendees and some speakers at the conference expressed worry or guilt over the environmental cost of attending ECOOP from faraway places. During the pandemic of 2020–2022 we involuntarily studied the effects of meeting only virtually, with the unanimous conclusion that meeting in person yields much better results in terms of transferring knowledge and ideas as well as sparking collaborations. This goes for long standing relationships as well as for new acquaintances — our whole societies would miss out on a lot of progress if we stopped this horizon-widening practice. More likely than not, those crucial discoveries that allow us to better protect our environment will originate in the unforeseen exchange of ideas through personal interaction!
