Tags:Actor, Cooperative Scheduling, Deadlock Detection, Predicate Abstraction and Transition System
Abstract:
In this paper we introduce a new method for detecting deadlock in the coroutine mode of the method execution of a single actor. The underlying actor-based language features asynchronous method calls and supports coroutines which allow for the cooperative scheduling of the tasks belonging to an actor. We model the local behavior of an actor as a well-structured transition system by means of predicate abstraction and derive the decidability of the occurrence of deadlocks caused by the coroutine mode of method execution.