Active Objects with Deterministic Behaviour

Ludovic Henrio (1) , Einar Broch Johnsen (2) , Violet Ka I. Pun (3)

1 CASH - CASH - Compilation and Analysis, Software and Hardware
2 UiO - University of Oslo
3 Western Norway University of Applied Sciences

Active objects extend the Actor paradigm with structured communication using method calls and futures. Active objects are, like actors, known to be data race free. Both are inherently concurrent, as they share a fundamental decoupling of communication and synchroni-sation. Both encapsulate their state, restricting access to one process at a time. Clearly, this rules out low-level races between two processes accessing a shared variable. However, is that sufficient to guarantee de-terministic results from the execution of an active object program? In this paper we are interested in so-called high-level races caused by the fact that the arrival order of messages between active objects can be non-deterministic, resulting in non-deterministic overall behaviour. We study this problem in the setting of a core calculus and identify restrictions on active object programs which are sufficient to guarantee deterministic behaviour for active object programs. We formalise these restrictions as a simple extension to the type system of the calculus and prove that well-typed programs exhibit deterministic behaviour.

Domaines: Calcul parallèle, distribué et partagé [cs.DC]

Ludovic Henrio, Einar Broch Johnsen, Violet Ka I. Pun. Active Objects with Deterministic Behaviour. Integrated Formal Methods. IFM 2020, Nov 2020, Lugano, Switzerland. pp.181-198, ⟨10.1007/978-3-030-63461-2_10⟩. ⟨hal-03008405⟩