Towards an alternate characterisation of the actor safety preorder

Abstract

In this work, we consider the Actor Model of concurrency, more precisely, how actor systems relate to each other. We use the widely accepted notion of safety testing as a starting point, where we compare two actor systems by the tests they are able to pass. If they are able to pass all the same tests, we can conclude they are related, otherwise they are not. While intuitive to reason about, this method finds its shortcoming at its core: to show that two actor systems are related we must consider all possible tests, of which there are an infinite number. We therefore shift to relating actors by their traces, considering only the possible traces of two actor systems. A particular trace-based technique proven to be correct in previous work with respect to safety testing is examined, and shown to be a significant improvement over safety testing since dealing with the number of traces an actor system can make versus the number of tests it can pass is generally easier to automate. However, we identify its weakness with systems producing an infinite number of traces, in particular recursive systems, and we therefore construct a new method of relating actors based on coinductive techniques. Rather than comparing traces, we compare the intermediary states of the actor systems. Consequently, when dealing with recursive systems, once a state has been examined, we do not have to examine its traces again if it is looped back to. This technique is finally shown to be sound with respect to the trace-based technique. respect to the trace-based technique.