2011/03/26 by Matthew Might, David Van Horn, Might, Matthew +1 · 1 citation
Computer Science · #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Formal Methods in Verification
paper · pdf · doi:10.48550/arxiv.1103.5167
We develop a framework for computing two foundational analyses for concurrent\nhigher-order programs: (control-)flow analysis (CFA) and may-happen-in-parallel\nanalysis (MHP). We pay special attention to the unique challenges posed by the\nunrestricted mixture of first-class continuations and dynamically spawned\nthreads. To set the stage, we formulate a concrete model of concurrent\nhigher-order programs: the P(CEK*)S machine. We find that the systematic\nabstract interpretation of this machine is capable of computing both flow and\nMHP analyses. Yet, a closer examination finds that the precision for MHP is\npoor. As a remedy, we adapt a shape analytic technique-singleton abstraction-to\ndynamically spawned threads (as opposed to objects in the heap). We then show\nthat if MHP analysis is not of interest, we can substantially accelerate the\ncomputation of flow analysis alone by collapsing thread interleavings with a\nsecond layer of abstraction.\n