A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs
The authors develop a framework for computing two foundational analyses for concurrent higher-order programs: (Control-) Flow Analysis (CFA) and May-Happen-in-Parallel analysis (MHP). They pay special attention to the unique challenges posed by the unrestricted mixture of first-class continuations and dynamically spawned threads. To set the stage, the authors formulate a concrete model of concurrent higher-order programs: the P(CEK)S machine. They find that the systematic abstract interpretation of this machine is capable of computing both flow and MHP analyses. Yet, a closer examination finds that the precision for MHP is poor.