## Interprocedural Analysis of Asynchronous Programs

*
Ranjit Jhala and
Rupak Majumdar
*
An *asynchronous program* is one that contains procedure
calls which are not directly executed from the callsite, but
stored and ``dispatched" in a non-deterministic order by
an external scheduler at a later point.
We formalize the problem of interprocedural dataflow
analysis for asynchronous programs as AIFDS problems, a generalization
of the IFDS problems for interprocedural dataflow analysis.
We give an algorithm for computing the precise meet-over-valid-paths
solution for any AIFDS
instance, as well as a *demand-driven* algorithm for solving the
corresponding demand AIFDS instances.
Our algorithm can be easily implemented on top of any existing
interprocedural dataflow analysis framework.
We have implemented the algorithm on top of \blast, thereby
obtaining the first safety verification tool for unbounded
asynchronous programs.
Though we show the problem of solving AIFDS instances to be
EXPSPACE-hard, we find that in practice our technique can efficiently
analyze programs by exploiting standard optimizations of
interprocedural dataflow analyses.

* Proceedings of the 34th
Annual ACM Symposium on the Principles of Programming Languages, 2007.*
(POPL), 2007 * (to appear)*.

Eye-friendly PostScript
Eye-friendly PDF
PDF
PostScript
© 2007.