Quantified Abstract Configurations of Distributed Systems
Loading...
Full text at PDC
Publication date
2014
Advisors (or tutors)
Editors
Journal Title
Journal ISSN
Volume Title
Publisher
Springer
Citation
[AAG07] E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In Rocco De Nicola, editor, 16th European Symposium on Programming, ESOP’07, volume 4421 of Lecture Notes in Computer Science, pages 157–172. Springer, March 2007.
[AAG10] E. Albert, P. Arenas, S. Genaim, I. Herraiz, and G. Puebla. Comparing cost functions in resource analysis. In 1st International Workshop on Foundational and Practical Aspects of Resource Analysis (FOPARA’09), volume 6234 of Lecture Notes in Computer Science, pages 1–17. Springer, 2010.
[AAG11a] E. Albert, P. Arenas, S. Genaim, M. G´omez-Zamalloa, and G. Puebla. Cost Analysis of Concurrent OO programs. In Proc. of APLAS’11, volume 7078 of LNCS, pages 238–254. Springer, December 2011.
[AAG12a] E. Albert, P. Arenas, S. Genaim, M. G´omez-Zamalloa, and G. Puebla. COSTABS: A Cost and Termination Analyzer for ABS. In Procs. of PEPM’12, pages 151–154. ACM Press, 2012.
[AAG12b] E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Object-Oriented Bytecode Programs. Theoretical Computer Science (Special Issue on Quantitative Aspects of Programming Languages), 413(1):142–159, 2012.
[AAG08] E. Albert, P. Arenas, S. Genaim, and G. Puebla. Automatic inference of upper bounds for recurrence relations in cost analysis. In Proc. of SAS 2008, volume 5079 of Lecture Notes in Computer Science, pages 221–237. Springer, 2008.
[AAG11b] 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.
[ACP13] E. Albert, J. Correas, G. Puebla, and G. Rom´an-D´ıez. Quantified Abstractions of Distributed Systems. In Proc. of iFM’13, volume 7940 of LNCS, pages 285–300. Springer, 2013.
[AFG13] E. Albert, A. Flores-Montoya, S. Genaim, and E. Martin-Martin. Termination and Cost Analysis of Loops with Concurrent Interleavings. In ATVA 2013, LNCS 8172, pages 349–364. Springer, October 2013.
[Ame89] P. America. Issues in the design of a parallel object-oriented language. Formal Aspects of Computing, 1:366–411, 1989.
[APC12] E. Albert, P.Arenas, J. Correas, M. G´omez-Zamalloa, S. Genaim, G. Puebla, and G. Rom´an-D´ıez. Object-sensitive cost analysis for concurrent objects. http://costa.ls.fi.upm.es/papers/costa/AlbertACGGPRtr.pdf, 2012.
[ASY09] M. F. Al-Saleh and A. E. Yousif. Properties of the standard deviation that are rarely mentioned in classrooms. Austrian Journal of Statistics, 38(3):193–202, 2009.
[AVW96] J. Armstrong, R. Virding, C. Wistrom, and M. Williams. Concurrent Programming in Erlang. Prentice Hall, 1996.
[BCG07] M. Bruynooghe, M. Codish, J. Gallagher, S. Genaim, and W. Vanhoof. Termination Analysis of Logic Programs through Combination of Type-Based norms. TOPLAS, 29(2):Art. 10, 2007.
[BBS13] J. Bjørk, F. S. de Boer, E. Broch Johnsen, R. Schlatte, and S. L. Tapia Tarifa. User-defined schedulers for real-time concurrent objects. ISSE, 9(1):29–43, 2013.
[BYV09] R. Buyya, C. S. Yeo, S. Venugopal, J. Broberg, and I. Brandic. Cloud computing and emerging IT platforms: Vision, hype, and reality for delivering computing as the 5th utility. Future Generation Computer Systems, 25(6):599–616, 2009.
[Car93] D. Caromel. Towards a method of object-oriented concurrent programming. Communications of the ACM, 36(9):90–102, 1993.
[BGS12] F. S. de Boer, I. Grabe, and M. Steffen. Termination detection for active objects. J. Log. Algebr. Program., 81(4):541–557, 2012.
[Fer01] J. Feret. Occurrence Counting Analysis for the Pi-Calculus. Electronic Notes in Theoretical Computer Science, 39(2):1–18, 2001.
[FMA13] A. Flores-Montoya, E. Albert, and S. Genaim. May-Happen-in-Parallel based Deadlock Analysis for Concurrent Objects. In FORTE’13, LNCS, pages 273–288. Springer, 2013.
[HO09] P. Haller and M. Odersky. Scala actors: Unifying thread-based and event-based programming. Theor. Comput. Sci., 410(2-3):202–220, 2009.
[JHS12] E. B. Johnsen, R. H¨ahnle, J. Sch¨afer, R. Schlatte, and M. Steffen. ABS: A Core Language for Abstract Behavioral Specification. In Proc. of FMCO’10 (Revised Papers), volume 6957 of LNCS, pages 142–164. Springer, 2012.
[MRR05] A. Milanova, A. Rountev, and B. G. Ryder. Parameterized Object Sensitivity for Points-to Analysis for Java. ACM Trans. Softw. Eng. Methodol., 14:1–41, 2005.
[PHW05] A. Di Pierro, C. Hankin, and H. Wiklicky. Quantitative static analysis of distributed systems. Journal of Functional Programming, 1:37–81, 2005.
[RL05] R.Gori and F. Levi. A new occurrence counting analysis for bioambients. In APLAS, volume 3780 of LNCS, pages 381–400. Springer, 2005.
[SBL11] Y. Smaragdakis, M. Bravenboer, and O. Lhot´ak. Pick your Contexts Well: Understanding Object-Sensitivity. In In Proc. of POPL’11, pages 17–30. ACM, 2011.
[SPH10] J. Sch¨afer and A. Poetzsch-Heffter. JCobox: Generalizing Active Objects to Concurrent Components. In Proc. Of ECOOP’10, LNCS, pages 275–299. Springer, 2010.
[YBS86] A. Yonezawa, J.P. Briot, and E. Shibayama. Object-oriented concurrent programming ABCL/1. In Procs. Of OOPLSA’86, pages 258–268, New York, USA, 1986. ACM
Abstract
When reasoning about distributed systems, it is essential to have information about the different kinds of nodes that compose the system, how many instances of each kind exist, and how nodes communicate with other nodes. In this paper we present a static-analysis-based approach which is able to provide information about the questions above. In order to cope with an unbounded number of nodes and an unbounded number of calls among them, the analysis performs an abstraction of the system producing a graph whose nodes may represent (infinitely) many concrete nodes and arcs represent any number of (infinitely) many calls among nodes. The crux of our approach is that the abstraction is enriched with upper bounds inferred by resource analysis that limit the number of concrete instances that the nodes and arcs represent and their resource consumption. The information available in our quantified abstract configurations allows us to define performance indicators which measure the quality of the system. In particular, we present several indicators that assess the level of distribution in the system, the amount of communication among distributed nodes that it requires, and how balanced the load of the distributed nodes that compose the system is. Our performance indicators are given as functions on the input data sizes, and they can be used to automate the comparison of different distributed settings and guide towards finding the optimal configuration.