An LAGC Semantics for Timed Rebeca

Abstract

Multithreading and actors offer different models of concurrency to the programmer. With multithreading, the programmer needs to deal with shared-state and data races, which make programs complex to understand, error-prone and challenging to verify, but potentially very efficient if these issues are mastered to perfection. On the other hand, actors — and their object-oriented incarnation as active objects, — which are inherently concurrent and protect their internal state against races, seem easy to understand and intuitive, but programs may be exposed to deadlocks due to callbacks. Is it possible to simply transition programs from the one concurrency model to the other at will, and thereby get the best of both worlds? We believe such a seamless transition between these concurrency models opens an interesting direction of research that remains to be investigated. As a step in this direction, this paper provides a high-level, informal outline of the translations between multithreading and active object concurrency, highlighting how intuitive or non-intuitive it is to move from one concurrency model to the other

Publication
In: Rebeca for Actor Analysis in Action. LNCS 15560. © Springer 2025.