Automated Synthesis of Asynchronizations

TL;DR

This paper presents a method for automatically converting sequential programs into asynchronous ones using async/await, ensuring data race freedom and analyzing the complexity of enumerating all safe asynchronizations.

Contribution

It introduces a novel approach for safe program refactoring into asynchronous code with polynomial delay complexity and practical implementation on real-world C# programs.

Findings

The approach guarantees data race freedom during refactoring.

The delay complexity of enumerating all safe asynchronizations is polynomial.

The method has been successfully implemented and evaluated on open-source C# projects.

Abstract

Asynchronous programming is widely adopted for building responsive and efficient software, and modern languages such as C# provide async/await primitives to simplify the use of asynchrony. In this paper, we propose an approach for refactoring a sequential program into an asynchronous program that uses async/await, called asynchronization. The refactoring process is parametrized by a set of methods to replace with asynchronous versions, and it is constrained to avoid introducing data races. We investigate the delay complexity of enumerating all data race free asynchronizations, which quantifies the delay between outputting two consecutive solutions. We show that this is polynomial time modulo an oracle for solving reachability in sequential programs. We also describe a pragmatic approach based on an interprocedural data-flow analysis with polynomial-time delay complexity. The latter approach has been implemented and evaluated on a number of non-trivial C# programs extracted from open-source repositories