Abstract
We develop a framework for computing two foundational analyses for concurrent higher-order programs: (control-)flow analysis (CFA) and may-happen-in-parallel analysis (MHP). We pay special attention to the unique challenges posed by the unrestricted mixture of first-class continuations and dynamically spawned threads. To set the stage, we formulate a concrete model of concurrent higher-order programs: the P(CEK*)S machine. We 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. As a remedy, we adapt a shape analytic technique—singleton abstraction—to dynamically spawned threads (as opposed to objects in the heap). We then show that if MHP analysis is not of interest, we can substantially accelerate the computation of flow analysis alone by collapsing thread interleavings with a second layer of abstraction.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221–239. Springer, Heidelberg (2006), http://dx.doi.org/10.1007/11823230_15 , doi:10.1007/11823230_15
Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: PLDI 1990: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementationm, PLDI 1990, pp. 296–310. ACM, New York (1990)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1979, pp. 269–282. ACM Press, New York (1979)
Feeley, M.: An Efficient and General Implementation of Futures on Large Scale Shared-Memory Multiprocessors. PhD thesis, Brandeis University (April 1993)
Felleisen, M., Friedman, D.P.: Control operators, the SECD-machine, and the lambda-calculus. In: 3rd Working Conference on the Formal Description of Programming Concepts (August 1986)
Flanagan, C., Felleisen, M.: The semantics of future and its use in program optimization. In: POPL 1995: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 209–220. ACM, New York (1995)
Flanagan, C., Felleisen, M.: The semantics of future and an application. Journal of Functional Programming 9(01), 1–31 (1999)
Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: PLDI 1993: Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, pp. 237–247. ACM, New York (1993)
Hudak, P.: A semantic model of reference counting and its abstraction. In: LFP 1986: Proceedings of the 1986 ACM Conference on LISP and Functional Programming, pp. 351–363. ACM, New York (1986)
Jagannathan, S., Thiemann, P., Weeks, S., Wright, A.: Single and loving it: must-alias analysis for higher-order languages. In: POPL 1998: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1998, pp. 329–341. ACM, New York (1998)
Jones, N.D.: Flow analysis of lambda expressions (preliminary version). In: Proceedings of the 8th Colloquium on Automata, Languages and Programming, pp. 114–128. Springer, London (1981)
Might, M.: Shape analysis in the absence of pointers and structure. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 263–278. Springer, Heidelberg (2010)
Might, M., Shivers, O.: Exploiting reachability and cardinality in higher-order flow analysis. Journal of Functional Programming 18(Special Double Issue 5-6), 821–864 (2008)
Might, M., Smaragdakis, Y., Van Horn, D.: Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In: PLDI 2010: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 305–315. ACM, New York (2010)
Navabi, A., Jagannathan, S.: Exceptionally safe futures. In: Field, J., Vasconcelos, V. (eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 47–65. Springer, Heidelberg (2009)
Palsberg, J.: Closure analysis in constraint form. ACM Transactions on Programming Languages and Systems 17(1), 47–62 (1995)
Queinnec, C.: Continuations and web servers. Higher-Order and Symbolic Computation 17(4), 277–295 (2004)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)
Shivers, O.: Control flow analysis in Scheme. In: PLDI 1988: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, pp. 164–174. ACM, New York (1988)
Shivers, O.G.: Control-Flow Analysis of Higher-Order Languages PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (1991)
Van Horn, D., Mairson, H.G.: Deciding kCFA is complete for EXPTIME. In: ICFP 2008: Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, pp. 275–282. ACM, New York (2008)
Van Horn, D., Might, M.: Abstracting abstract machines. In: ICFP 2010: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, pp. 51–62. ACM, New York (2010)
Yahav, E.: Verifying safety properties of concurrent java programs using 3-valued logic. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001, pp. 27–40. ACM Press, New York (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Might, M., Van Horn, D. (2011). A Family of Abstract Interpretations for Static Analysis of Concurrent Higher-Order Programs. In: Yahav, E. (eds) Static Analysis. SAS 2011. Lecture Notes in Computer Science, vol 6887. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23702-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-23702-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23701-0
Online ISBN: 978-3-642-23702-7
eBook Packages: Computer ScienceComputer Science (R0)