The FLINT Project








Automatic Static Cost Analysis for Parallel Programs

Last modified: Mon Apr 6 20:41:01 2015 GMT.


Jan Hoffmann
Zhong Shao


Static analysis of the evaluation cost of programs is an extensively studied problem that has many important applications. However, most automatic methods for static cost analysis are limited to sequential evaluation while programs are increasingly evaluated on modern multicore and multiprocessor hardware.

This article introduces the first automatic analysis for deriving bounds on the worst-case evaluation cost of parallel first-order functional programs. The analysis is performed by a novel type system for amortized resource analysis. The main innovation is a technique that separates the reasoning about sizes of data structures and evaluation cost within the same framework. The cost semantics of parallel programs is based on call-by-value evaluation and the standard cost measures work and depth. A soundness proof of the type system establishes the correctness of the derived cost bounds with respect to the cost semantics. The derived bounds are multivariate resource polynomials which depend on the sizes of the arguments of a function.

Type inference can be reduced to linear programming and is fully automatic. A prototype implementation of the analysis system has been developed to experimentally evaluate the effectiveness of the approach. The experiments show that the analysis infers bounds for realistic example programs such as quick sort for lists of lists, matrix multiplication, and an implementation of sets with lists. The derived bounds are often asymptotically tight and the constant factors are close to the optimal ones.


In Proc. 24th European Symposium on Programming (ESOP'15), London, UK, April 2015. Lecture Notes in Computer Science, Vol. 9032, pages 132-157.
  • Conference Paper PDF

  • Copyright © 1996-2023 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page