Abel Garcia
ABSTRACT
We propose a static analysis technique that computes upper bounds of virtual machine usages in a concurrent language with explicit acquire and release operations of virtual machines. In our language it is possible to delegate other (ad-hoc or third party) concurrent code to release virtual machines (by passing them as arguments of invocations). Our technique is modular and consists of (i) a type system associating programs with behavioural types that records relevant information for resource usage (creations, releases, and concurrent operations), (ii) a translation function that takes behavioural types and return cost equations, and (iii) an automatic off-the-shelf solver for the cost equations. A soundness proof of the type system establishes the correctness of our technique with respect to the cost equations. We have experimentally evaluated our technique using a cost analysis solver and we report some results. The experiments show that our analysis allows us to derive bounds for programs that are better than other techniques, such as those based on amortized analysis.
- E. Albert, P. Arenas, S. Genaim, and G. Puebla. Automatic inference of upper bounds for recurrence relations in cost analysis. In Proceedings SAS 2008, volume 5079 of Lecture Notes in Computer Science, pages 221--237. Springer, 2008. Google Scholar
Digital Library
- E. Albert, S. Genaim, and M. Gómez-Zamalloa. Parametric inference of memory requirements for garbage collected languages. SIGPLAN Not., 45(8):121--130, 2010. Google ScholarDigital Library
- E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, and G. Puebla. Cost analysis of concurrent OO programs. In Proceedings of APLAS 2011, volume 7078 of Lecture Notes in Computer Science, pages 238--254. Springer, 2011. Google ScholarDigital Library
- E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost analysis of object-oriented bytecode programs. Theoretical Computer Science, 413(1):142--159, 2012. Google ScholarDigital Library
- E. Albert, J. Correas, and G. Romn-Dez. Peak cost analysis of distributed systems. In Proceedings of SAS 2014, volume 8723 of Lecture Notes in Computer Science, pages 18--33. Springer, 2014.Google ScholarCross Ref
- E. Albert, J. Correas, and G. Román-Díez. Non-Cumulative Resource Analysis. In Proceedings of TACAS 2015, Lecture Notes in Computer Science. Springer, 2015. To appear.Google ScholarDigital Library
- D. E. Alonso-Blas and S. Genaim. On the limits of the classical approach to cost analysis. In Proceedings of SAS 2012, volume 7460 of Lecture Notes in Computer Science, pages 405--421. Springer, 2012. Google ScholarDigital Library
- R. Barik. Efficient computation of may-happen-in-parallel information for concurrent java programs. In Proceedings of LCPC 2005, volume 4339 of Lecture Notes in Computer Science, pages 152--169. Springer, 2006. Google ScholarDigital Library
- M. Brockschmidt, F. Emmes, S. Falke, C. Fuhs, and J. Giesl. Alternating runtime and size complexity analysis of integer programs. In Proceedings of TACAS 2014, volume 8413 of Lecture Notes in Computer Science, pages 140--155. Springer, 2014.Google ScholarCross Ref
- W. Chin, H. H. Nguyen, S. Qin, and M. Rinard. Memory usage verification for oo programs. In Proceedings of SAS 2005, volume 3672 of Lecture Notes in Computer Science, pages 70--86. Springer, 2005. Google ScholarDigital Library
- A. Flores Montoya and R. Hähnle. Resource analysis of complex programs with cost equations. In Proceedings of 12th Asian Symposium on Programming Languages and Systems, volume 8858 of Lecture Notes in Computer Science, pages 275--295. Springer, 2014.Google ScholarCross Ref
- E. Giachino, C. Laneve, and M. Lienhardt. A framework for deadlock detection in ABS. Software and Systems Modeling, 2015. ISSN 1619-1366. . URL http://dx.doi.org/10.1007/s10270-014-0444-y. To appear.Google Scholar
- S. Gulwani, K. K. Mehra, and T. Chilimbi. Speed: precise and efficient static estimation of program computational complexity. In ACM SIGPLAN Notices, volume 44, pages 127--139. ACM, 2009. Google ScholarDigital Library
- J. Hoffmann and Z. Shao. Automatic static cost analysis for parallel programs, 2015. URL http://cs.yale.edu/homes/hoffmann/papers/parallelcost2014.pdfm. {Online; accessed 11-February-2015}.Google ScholarDigital Library
- J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst., 34(3):14, 2012. . URL http://doi.acm.org/10.1145/2362389.2362393. Google ScholarDigital Library
- M. Hofmann and S. Jost. Static prediction of heap space usage for first-order functional programs. In Proceedings of POPL 2003, pages 185--197. ACM, 2003. Google ScholarDigital Library
- M. Hofmann and S. Jost. Type-based amortised heap-space analysis. In Proceedings of ESOP 2006, volume 3924 of Lecture Notes in Computer Science, pages 22--37. Springer, 2006. Google ScholarDigital Library
- M. Hofmann and D. Rodriguez. Efficient type-checking for amortised heap-space analysis. In Proceedings of CSL 2009, volume 5771 of Lecture Notes in Computer Science, pages 317--331. Springer, 2009. Google ScholarDigital Library
- E. B. Johnsen, R. Hähnle, J. Schäfer, R. Schlatte, and M. Steffen. ABS: A core language for abstract behavioral specification. In Proceedings of FMCO 2010, volume 6957 of Lecture Notes in Computer Science, pages 142--164. Springer, 2011. Google ScholarDigital Library
- R. E. Tarjan. Amortized computational complexity. SIAM Journal on Algebraic Discrete Methods, 6(2):306--318, 1985.Google ScholarCross Ref
- B. Wegbreit. Mechanical program analysis. Communications of the ACM, 18(9):528--539, 1975. Google ScholarDigital Library
Index Terms
- Static analysis of cloud elasticity
Recommendations
Automatic Static Cost Analysis for Parallel Programs
Proceedings of the 24th European Symposium on Programming on Programming Languages and Systems - Volume 9032Static 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 ...
Multivariate amortized resource analysis
POPL '11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesWe study the problem of automatically analyzing the worst-case resource usage of procedures with several arguments. Existing automatic analyses based on amortization, or sized types bound the resource usage or result size of such a procedure by a sum of ...
Comments