Computing Race Variants in Message-Passing Concurrent Programming with Selective Receives

Abstract

Message-passing concurrency is a popular computation model that underlies several programming languages like, e.g., Erlang, Akka, and (to some extent) Go and Rust. In particular, we consider a message-passing concurrent language with dynamic process spawning and selective receives, i.e., where messages can only be consumed by the target process when they match a specific constraint (e.g., the case of Erlang). In this work, we introduce a notion of trace that can be seen as an abstraction of a class of causally equivalent executions (i.e., which produce the same outcome). We then show that execution traces can be used to identify message races. We provide constructive definitions to compute message races as well as to produce so-called race variants, which can then be used to drive new executions which are not causally equivalent to the previous ones. This is an essential ingredient of state-space exploration techniques for program verification.