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).