Automated synthesis of asynchronizations

DOI10.1007/978-3-031-22308-2_7MaRDI QIDQ6164424zbMATH OpenOpenAlexFDO

Authors Sidi Mohamed Beillahi, Ahmed Bouajjani, Constantin Enea, Shuvendu K. Lahiri

Publication date 28 July 2023

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2209.06648

Mathematics Subject Classification ID

Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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

Recommendations

• Synthesis of asynchronous reactive programs from temporal specifications
• Synchronizing the asynchronous
• Interprocedural analysis of asynchronous programs
• Verifiable design of asynchronous software
• scientific article; zbMATH DE number 6774232

Cites work

• Abstraction-guided synthesis of synchronization
• Analysis of Boolean Programs
• Analysis of recursively parallel programs
• From non-preemptive to preemptive scheduling using synchronization synthesis
• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• Inferring Synchronization under Limited Observability
• Succinct representation of concurrent trace sets
• Synthesis of Communicating Processes from Temporal Logic Specifications
• Verifying robustness of event-driven asynchronous programs against concurrency

Cited in

(7)

• scientific article; zbMATH DE number 6687767 (Why is no real title available?)
• scientific article; zbMATH DE number 3880599 (Why is no real title available?)
• scientific article; zbMATH DE number 3976309 (Why is no real title available?)
• scientific article; zbMATH DE number 554484 (Why is no real title available?)
• Algorithms and Complexity of Automata Synthesis by Asynhcronous Orchestration With Applications to Web Services Composition
• Compositional synthesis of asynchronous automata
• scientific article; zbMATH DE number 3310916 (Why is no real title available?)

This page was built for publication: Automated synthesis of asynchronizations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6164424)