Elvira Albert
Damiano Zanardini
ABSTRACT
The task level of a program is the maximum number of tasks that can be available (i.e., not finished nor suspended) simultaneously during its execution for any input data. Static knowledge of the task level is of utmost importance for understanding and debugging parallel programs as well as for guiding task schedulers. We present, to the best of our knowledge, the first static analysis which infers safe and precise approximations on the task level for a language with async-finish parallelism. In parallel languages, async and finish are basic constructs for, respectively, spawning tasks and waiting until they terminate. They are the core of modern, parallel, distributed languages like X10. Given a (parallel) program, our analysis returns a task-level upper bound, i.e., a function on the program's input arguments that guarantees that the task level of the program will never exceed its value along any execution. Our analysis provides a series of useful (over)-approximations, going from the total number of tasks spawned in the execution up to an accurate estimation of the task level.
- M. Abadi and G. D. Plotkin. A model of cooperative threads. In Proc. of POPL'09, pages 29--40. ACM, 2009. Google Scholar
Digital Library
- E. Albert, P. Arenas, S. Genaim, and G. Puebla. Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning, 46(2):161--203, 2011. Google ScholarDigital Library
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In Proc. of ESOP'07, volume 4421 of LNCS, pages 157--172. Springer, 2007. Google ScholarDigital Library
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. COSTA: Design and Implementation of a Cost and Termination Analyzer for Java Bytecode. In Proc. of FMCO'07, volume 5382 of LNCS, pages 113--133. Springer, 2008. Google ScholarDigital Library
- E. Albert, S. Genaim, and M. Gómez-Zamalloa. Parametric Inference of Memory Requirements for Garbage Collected Languages. In Proc. of ISMM'10, pages 121--130. ACM Press, 2010. Google ScholarDigital Library
- A. W. Appel. Ssa is Functional Programming. SIGPLAN Notices, 33(4):17--20, 1998. Google ScholarDigital Library
- V. Braberman, F. Fernández, D. Garbervetsky, and S. Yovine. Parametric Prediction of Heap Memory Requirements. In Proc. of ISMM'08, pages 141--150. ACM Press, 2008. Google ScholarDigital Library
- P. Charles, C. Grothoff, V. A. Saraswat, C. Donawa, A. Kielstra, K. Ebcioglu, C. von Praun, and V. Sarkar. X10: An Object-Oriented Approach to Non-Uniform Cluster computing. In Proc. of OOPSLA'05, pages 519--538. ACM, 2005. Google ScholarDigital Library
- W-N. Chin, H.H. Nguyen, C. Popeea, and S. Qin. Analysing Memory Resource Bounds for Low-Level Programs. In Proc. of ISMM'08, pages 151--160. ACM Press, 2008. Google ScholarDigital Library
- R. DeLine and K.R.M. Leino. BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005--70, Microsoft Research, 2005.Google Scholar
- M. F\"ahndrich. Static Verification for Code Contracts. In Proc. of SAS'10, volume 6337 of LNCS, pages 2--5. Springer, 2010. Google ScholarDigital Library
- S. Gulwani, K. K. Mehra, and T. M. Chilimbi. Speed: precise and efficient static estimation of program computational complexity. In Proc. of POPL'09, pages 127--139. ACM, 2009. Google ScholarDigital Library
- J. Hoffmann and M. Hofmann. Amortized Resource Analysis with Polynomial Potential. In Proc. of ESOP'10, volume 6012 of LNCS, pages 287--306. Springer, 2010. Google ScholarDigital Library
- M. Hofmann and S. Jost. Type-Based Amortised Heap-Space Analysis. In Proc. of ESOP'06, volume 3924 of LNCS, pages 22--37. Springer, 2006. Google ScholarDigital Library
- N.D. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall, New York, 1993. Google ScholarDigital Library
- J. K. Lee and J. Palsberg. Featherweight X10: A Core Calculus for Async-Finish Parallelism. In Proc. of PPoPP'10, pages 25--36. ACM, 2010. Google ScholarDigital Library
- Antoine Miné. Field-sensitive value analysis of embedded c programs with union types and pointer arithmetics. In Proc. of LCTES'06, pages 54--63. ACM, 2006. Google ScholarDigital Library
- C. Otto, M. Brockschmidt, C. von Essen, and J. Giesl. Automated Termination Analysis of Java Bytecode by Term Rewriting. In Proc. of RTA'10, volume 6 of LIPIcs, pages 259--276, 2010.Google Scholar
- R. Raman, J. Zhao, V. Sarkar, M. T. Vechev, and E. Yahav. Efficient data race detection for async-finish parallelism. In Proc. of RV'10, volume 6418 of LNCS, pages 368--383. Springer, 2010. Google ScholarDigital Library
- V. A. Saraswat and R. Jagadeesan. Concurrent Clustered Programming. In Proc. of CONCUR'05, volume 3653 of LNCS, pages 353--367. Springer, 2005. Google ScholarDigital Library
- F. Spoto, F. Mesnard, and É. Payet. A Termination Analyser for Java Bytecode based on Path-Length. Transactions on Programming Languages and Systems, 32(3), 2010. Google ScholarDigital Library
- W. Zou T. Wei, J. Mao and Y. Chen. A new algorithm for identifying loops in decompilation. In Proc. of SAS'07, volume 4634 of LNCS, pages 170--183, 2007. Google ScholarDigital Library
- L. Unnikrishnan and S. Stoller. Parametric heap usage analysis for functional programs. In Proc. of ISMM'09, pages 139--148. ACM Press, 2009. Google ScholarDigital Library
- L. Unnikrishnan, S. D. Stoller, and Y. A. Liu. Optimized Live Heap Bound Analysis. In Proc. of VMCAI'03, volume 2575 of LNCS, pages 70--85. Springer, 2003. Google ScholarDigital Library
- R. Vallee-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot - a Java Optimization Framework. In Proc. of CASCON'99, pages 125--135. IBM, 1999. Google ScholarDigital Library
- M. T. Vechev, E. Yahav, R. Raman, and V. Sarkar. Automatic Verification of Determinism for Structured Parallel Programs. In Proc. of SAS'10, volume 6337 of LNCS, pages 455--471. Springer, 2010. Google ScholarDigital Library
- B. Wegbreit. Mechanical Program Analysis. Communications of the ACM, 18(9), 1975. Google ScholarDigital Library
Index Terms
- Task-level analysis for a language with async/finish parallelism
Recommendations
Task-level analysis for a language with async/finish parallelism
LCTES '10The task level of a program is the maximum number of tasks that can be available (i.e., not finished nor suspended) simultaneously during its execution for any input data. Static knowledge of the task level is of utmost importance for understanding and ...
Work-first and help-first scheduling policies for async-finish task parallelism
IPDPS '09: Proceedings of the 2009 IEEE International Symposium on Parallel&Distributed ProcessingMultiple programming models are emerging to address an increased need for dynamic task parallelism in applications for multicore processors and shared-address-space parallel computing. Examples include OpenMP 3.0, Java Concurrency Utilities, Microsoft ...
A work-stealing scheduler for X10's task parallelism with suspension
PPoPP '12: Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel ProgrammingThe X10 programming language is intended to ease the programming of scalable concurrent and distributed applications. X10 augments a familiar imperative object-oriented programming model with constructs to support light-weight asynchronous tasks as well ...
Reviews
Rafael Corchuelo
Multicore hardware platforms are sprouting up at an increasing pace, which makes it more important than ever before to schedule parallel programs efficiently. Having an a priori estimation of the maximum number of tasks a program can spawn at runtime (also referred to as a task level) would help schedulers to be more effective; unfortunately, having such estimations has not been possible so far. Albert, Arenas, Genaim, and Zanardini have devised a technique to calculate a precise upper bound to the task level, which seems to be the first such result in the literature. Their focus is on an X10-like language that supports async-finish parallelism. (This kind of parallelism is appealing because the results in the literature prove that it may not lead to deadlocking situations.) The technique is based on generating symbolic recurrence equations that accurately represent the resources a program consumes along theoretical parallel executions; the solution to these equations provides a precise upper bound to the task level. Furthermore, the authors argue that if this upper bound exists, then the program is guaranteed to terminate for all input data. The experimental results seem to suggest that this technique is promising. A lot of work must be done, however, with regard to extending it to the full X10 language and considering specific scheduling characteristics. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments