×

zbMATH — the first resource for mathematics

Dependence analysis for safe futures. (English) Zbl 1243.68144
Summary: A future is a well-known programming construct used to introduce concurrency into sequential programs. Computations annotated as futures are executed asynchronously and run concurrently with their continuations. Typically, futures are not transparent annotations: a program with futures need not produce the same result as the sequential program from which it was derived. Safe futures guarantee that a future-annotated program produces the same result as its sequential counterpart. The safety property is trivially satisfied in languages without side-effects or exceptions. In the presence of mutable references and language abstractions, such as exceptions, which permit the expression of non-local control-flow, ensuring safety requires that the future-annotated program adhere to control and data dependences imposed by the program’s sequential counterpart. In this paper, we present a formulation of safe futures for a higher-order functional language with first-class references and exceptions. Safety can be guaranteed at runtime by blocking a continuation from performing a potentially unsafe action before its futures have completed. To enable greater concurrency, we develop a static analysis and instrumentation and formalize the runtime behavior for instrumented programs that allows a continuation to proceed before its futures complete, as long as its actions are determined to be safe. A continuation’s action is safe if it is not control or data dependent on actions that may subsequently be performed by its futures.
MSC:
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] E. Allan, D. Chase, V.L. J. Hallett, J. Maessen, S. Ryu, G. Steele, S. Tobin-Hochstadt, The Fortress Language Specification Version 1.0, Tech. rep., Sun Microsystems, Inc., May 2008.
[2] Berger, E. D.; Yang, T.; Liu, T.; Novark, G.: Grace: safe multithreaded programming for c/c++, , 81-96 (2009)
[3] Jr., R. L. Bocchino; Adve, V. S.; Dig, D.; Adve, S. V.; Heumann, S.; Komuravelli, R.; Overbey, J.; Simmons, P.; Sung, H.; Vakilian, M.: A type and effect system for deterministic parallel Java, , 97-116 (2009)
[4] Charles, P.; Grothoff, C.; Saraswat, V.; Donawa, C.; Kielstra, A.; Ebcioglu, K.; Von Praun, C.; Sarkar, V.: X10: an object-oriented approach to non-uniform cluster computing, , 519-538 (2005)
[5] Danaher, J.; Lee, I.; Leiserson, C.: Programming with exceptions in jcilk, Science of computer programming 63, No. 2, 147-171 (2006) · Zbl 1114.68023 · doi:10.1016/j.scico.2006.05.008
[6] De Boer, F. S.; Clarke, D.; Johnsen, E. B.: A complete guide to the future, , 316-330 (2007)
[7] Feret, J.: Dependency analysis of mobile systems, , 314-330 (2002) · Zbl 1077.68578
[8] Flanagan, C.; Felleisen, M.: The semantics of future and an application, Journal of functional programming 9, No. 1, 1-31 (1999) · Zbl 0926.68075 · doi:10.1017/S0956796899003329
[9] Flanagan, C.; Freund, S. N.: Atomizer: a dynamic atomicity checker for multithreaded programs, , 256-267 (2004) · Zbl 1146.68350
[10] Flanagan, C.; Qadeer, S.: Types for atomicity, , 1-12 (2003) · Zbl 1271.68086
[11] Halstead, R.: Multilisp: a language for concurrent symbolic computation, ACM transactions on programming languages and systems 7, No. 4, 501-538 (1985) · Zbl 0581.68037 · doi:10.1145/4472.4478 · www.acm.org
[12] Harris, T.; Fraser, K.: Language support for lightweight transactions, , 388-402 (2003)
[13] Herlihy, M.; Luchangco, V.; Moir, M.; Iii, N. S. W.: Software transactional memory for dynamic-sized data structures, , 92-101 (2003)
[14] Jones, N. D.: Flow analysis of lambda expressions (preliminary version), , 114-128 (1981) · Zbl 0481.68027
[15] JSR166: Concurrency utilities, 2004. http://java.sun.com/j2se/1.5.0/docs/guide/concurrency.
[16] Kranz, D.; Jr., H. H. R.; Mohr, E.: Mul-T: a high-performance parallel lisp, , 81-90 (1989)
[17] Liskov, B.; Shrira, L.: Promises: linguistic support for efficient asynchronous procedure calls in distributed systems, , 260-267 (1988)
[18] M. Might, T. Prabhu, Interprocedural dependence analysis of higher-order programs via stack reachability, in: Proceedings of the 2009 Workshop on Scheme and Functional Programming, Scheme 2009, Boston, Massachussetts, USA, August 2009.
[19] Mohr, E.; Kranz, D.; Jr., H. H. R.: Lazy task creation: a technique for increasing the granularity of parallel programs, , 185-1990 (1990)
[20] A. Navabi, S. Jagannathan, Exceptionally Safe Futures, Tech. Rep. CSD TR #08-027, Purdue University Department of Computer Science, October 2008.
[21] Navabi, A.; Zhang, X.; Jagannathan, S.: Quasi-static scheduling for safe futures, , 23-32 (2008)
[22] Palsberg, J.: Closure analysis in constraint form, ACM transactions on programming languages and systems 17, No. 1, 47-62 (1995)
[23] Pratikakis, P.; Spacco, J.; Hicks, M.: Transparent proxies for Java futures, , 206-223 (2004)
[24] Rajwar, R.; Goodman, J. R.: Transactional lock-free execution of lock-based programs, , 5-17 (2002)
[25] Shavit, N.; Touitou, D.: Software transactional memory, , 204-213 (1995) · Zbl 1373.68178
[26] O. Shivers, Control-Flow Analysis of Higher-Order Languages or Taming Lambda, Ph.D. thesis, Carnegie Mellon University, May 1991.
[27] Welc, A.; Jagannathan, S.; Hosking, A.: Transactional monitors for concurrent objects, , 519-542 (2004)
[28] Welc, A.; Jagannathan, S.; Hosking, A.: Safe futures for Java, , 435-439 (2005)
[29] Zhang, L.; Krintz, C.; Nagpurkar, P.: Supporting exception handling for futures in Java, , 175-184 (2007)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.