Symbolic Reasoning for Automatic Signal Placement (Extended Version)

TL;DR

This paper introduces a static analysis-based method to automatically generate efficient explicit signaling code from implicit signaling in concurrent programs, reducing overhead and improving performance.

Contribution

It presents a novel static analysis technique and a tool called Expresso that optimizes thread signaling, outperforming previous automatic methods and matching hand-optimized code.

Findings

Expresso achieves an average 1.56x speedup over previous automatic signaling methods.

Generated code closely matches the performance of hand-optimized explicit signaling.

The approach guarantees semantic equivalence between source and generated programs.

Abstract

Explicit signaling between threads is a perennial cause of bugs in concurrent programs. While there are several run-time techniques to automatically notify threads upon the availability of some shared resource, such techniques are not widely-adopted due to their run-time overhead. This paper proposes a new solution based on static analysis for automatically generating a performant explicit-signal program from its corresponding implicit-signal implementation. The key idea is to generate verification conditions that allow us to minimize the number of required signals and unnecessary context switches, while guaranteeing semantic equivalence between the source and target programs. We have implemented our method in a tool called Expresso and evaluate it on challenging benchmarks from prior papers and open-source software. Expresso-generated code significantly outperforms past automatic signaling mechanisms (avg. 1.56x speedup) and closely matches the performance of hand-optimized explicit-signal code.