research-article

Open access

Algorithmic verification of asynchronous programs

Authors:

Pierre Ganty,

Rupak MajumdarAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 34, Issue 1

Article No.: 6, Pages 1 - 48

https://doi.org/10.1145/2160910.2160915

Published: 04 May 2012 Publication History

PDF eReader

Abstract

Asynchronous programming is a ubiquitous systems programming idiom for managing concurrent interactions with the environment. In this style, instead of waiting for time-consuming operations to complete, the programmer makes a non-blocking call to the operation and posts a callback task to a task buffer that is executed later when the time-consuming operation completes. A cooperative scheduler mediates the interaction by picking and executing callback tasks from the task buffer to completion (and these callbacks can post further callbacks to be executed later). Writing correct asynchronous programs is hard because the use of callbacks, while efficient, obscures program control flow.

We provide a formal model underlying asynchronous programs and study verification problems for this model. We show that the safety verification problem for finite-data asynchronous programs is expspace-complete. We show that liveness verification for finite-data asynchronous programs is decidable and polynomial-time equivalent to Petri net reachability. Decidability is not obvious, since even if the data is finite-state, asynchronous programs constitute infinite-state transition systems: both the program stack for an executing task and the task buffer of pending calls to tasks can be potentially unbounded.

Our main technical constructions are polynomial-time, semantics-preserving reductions from asynchronous programs to Petri nets and back. The first reduction allows the use of algorithmic techniques on Petri nets for the verification of asynchronous programs, and the second allows lower bounds on Petri nets to apply also to asynchronous programs.

We also study several extensions to the basic models of asynchronous programs that are inspired by additional capabilities provided by implementations of asynchronous libraries and classify the decidability and undecidability of verification questions on these extensions.

References

[1]

Abdulla, P. A., Cerans, K., Jonsson, B., and Tsay, Y.-K. 1996. General decidability theorems for infinite-state systems. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS'96). IEEE Computer Society, 313--321.

Abstract

References

Cited By

Index Terms

Recommendations

Context-bounded verification of liveness properties for multithreaded shared-memory programs

Verifying liveness for asynchronous programs

Verifying liveness for asynchronous programs

Comments

Information

Published In

Publisher

Publication History

Permissions

Check for updates

Author Tags

Qualifiers

Funding Sources

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations