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

TL;DR

This paper introduces a method to analyze message-passing concurrent programs with selective receives by using execution traces to identify message races and generate race variants, aiding in program verification.

Contribution

It presents a novel trace-based approach to detect message races and produce race variants in message-passing languages with selective receives, enhancing state-space exploration.

Findings

Trace abstraction effectively identifies message races.

Race variants enable exploration of new execution paths.

Method supports verification of concurrent message-passing programs.

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.