Uwe Nestmann

TCS Journal 2022 Journal Article

On distributability

• Kirstin Peters
• Uwe Nestmann
• Anna Schmitt

The Actor model of computation is the backbone for the design of some of the most successful distributed programming platforms, Erlang and Akka. It builds upon asynchronous message-passing (liberating senders from waiting) and unique message-routing (using unique Actor addresses), which enables relatively simple distributed implementations. The Actor model shares these principles with the model of computation underlying JoCaml, which supports the distributed implementation of OCaml components. In this paper, we support the distributability of the two models on theoretical grounds. For this, we investigate three refined variants of the π-calculus that can be understood as the essence of the two models. We show that neither of the three calculi is able to express a synchronization pattern that is known from the world of Petri nets and that was used by us as one criterion in a distributability hierarchy of process calculi. Moreover, we exhibit three encodings between the three calculi and prove that they each preserve the degree of distributability between source and target terms.

I&C Journal 2020 Journal Article

Distributability of mobile ambients

• Kirstin Peters
• Uwe Nestmann

Modern society is dependent on distributed software systems and to verify them different modelling languages such as mobile ambients were developed. They focus on mobility by allowing both a dynamic network topology as well as the movement of code within the network. To analyse the quality of mobile ambients as a good foundational model for distributed computation, we analyse the level of synchronisation between distributed components that they can express. Therefore, we rely on earlier established synchronisation patterns. It turns out that mobile ambients are not fully distributed, because they can express enough synchronisation to express a synchronisation pattern called M. However, they can express strictly less synchronisation than the pi-calculus. For this reason, we can show that there is no good and distributability-preserving encoding from the pi-calculus into mobile ambients and also no such encoding from mobile ambients into the join-calculus, i. e. , the expressive power of mobile ambients is in between these languages. Finally, we discuss how these results can be used to obtain a fully distributed variant of mobile ambients and present one example. Such a fully distributed variant of mobile ambients is a good foundation for distributed computation.

TCS Journal 2007 Journal Article

A formal semantics for protocol narrations

• Sébastien Briais
• Uwe Nestmann

Protocol narrations are a widely-used informal means to describe, in an idealistic manner, the functioning of cryptographic protocols as a single intended sequence of cryptographic message exchanges among the protocol’s participants. Protocol narrations have also been informally “turned into” a number of formal protocol descriptions, e. g. , using the spi-calculus. In this paper, we propose a direct formal operational semantics for protocol narrations that fixes a particular and, as we argue, well-motivated interpretation on how the involved protocol participants are supposed to execute. Based on this semantics, we explain and formally justify a natural and precise translation of narrations into spi-calculus. An optimised translation has been implemented in OCaml, and we report on case studies that we have carried out using the tool.

TCS Journal 2007 Journal Article

Open bisimulation, revisited

• Sébastien Briais
• Uwe Nestmann

In the context of the π -calculus, open bisimulation is prominent and popular due to its congruence properties and its easy implementability. Motivated by the attempt to generalise it to the spi-calculus, we offer a new, more refined definition and show how far it coincides with the original one.

I&C Journal 2002 Journal Article

Aliasing Models for Mobile Objects

• Uwe Nestmann
• Hans Hüttel
• Josva Kleist
• Massimo Merro

In Obliq, a lexically scoped, distributed, object-oriented programming language, object migration was suggested as the creation of a copy of the state of an object at the target site, followed by turning the object itself into an alias, also called surrogate, for the remote copy. We consider the creation of object surrogates as an abstraction of the above-mentioned style of migration. We introduce Øjeblik, a typed distribution-free subset of Obliq, and provide four different configuration-style semantics, which only differ in the respective aliasing model. We show that two of the semantics, one of which matches Obliq's implementation, render migration unsafe, while our new proposal allows for safe migration at least for a large class of program contexts. In addition, we propose a type system that allows a programmer to statically guarantee that programs belong to that class. Our work suggests a straightforward repair of Obliq's aliasing model.

I&C Journal 2002 Journal Article

Mobile Objects as Mobile Processes

• Massimo Merro
• Josva Kleist
• Uwe Nestmann

Obliq is a lexically scoped, distributed, object-based programming language. In Obliq, the migration of an object is proposed as creating a clone of the object at the target site, whereafter the original object is turned into an alias for the clone. Obliq has only an informal semantics, so there is no proof that this style of migration is safe, i. e. , transparent to object clients. In previous work, we introduced Ø, an abstraction of Obliq, where, by lexical scoping, sites have been abstracted away. We used Ø in order to exhibit how the semantics behind Obliq's implementation renders migration unsafe. We also suggested a modified semantics that we conjectured instead to be safe. In this paper, we rewrite our modified semantics of Ø in terms of the π-calculus, and we use it to formally prove the correctness of object surrogation, the abstraction of object migration in Ø.

I&C Journal 2002 Journal Article

Mobile Objects as Mobile Processes

• Massimo Merro
• Josva Kleist
• Uwe Nestmann

I&C Journal 2000 Journal Article

Decoding Choice Encodings

• Uwe Nestmann
• Benjamin C. Pierce

We study two encodings of the asynchronous π-calculus with input-guarded choice into its choice-free fragment. One encoding is divergence-free, but refines the atomic commitment of choice into gradual commitment. The other preserves atomicity, but introduces divergence. The divergent encoding is fully abstract with respect to weak bisimulation, but the more natural divergence-free encoding is not. Instead, we show that it is fully abstract with respect to coupled simulation, a slightly coarser—but still coinductively defined—equivalence that does not enforce bisimilarity of internal branching decisions. The correctness proofs for the two choice encodings introduce a novel proof tech- nique exploiting the properties of explicit decodings from translations to source terms.

I&C Journal 2000 Journal Article

What is a “Good” Encoding of Guarded Choice?

• Uwe Nestmann

The π-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the π-calculus with asynchronous output and no choice. This result was recently proved by C. Palamidessi and, as a corollary, she showed that there is no fully compositional encoding from the former into the latter that preserves divergence-freedom and symmetries. This paper argues that there are nevertheless “good” encodings between these calculi. In detail, we present a series of encodings for languages with (1) input-guarded choice, (2) both input- and output-guarded choice, and (3) mixed-guarded choice, and investigate them with respect to compositionality and divergence-freedom. The first and second encoding satisfy all of the above criteria, but various “good” candidates for the third encoding—inspired by an existing distributed implementation—invalidate one or the other criterion. While essentially confirming Palamidessi's result, our study suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes.