By following a rely-guarantee style of reasoning, we present a novel termination analysis for concurrent programs that, in order to prove termination of a considered loop, makes the assumption that the "shared-data that is involved in the termination proof of the loop is modified a finite number of times". In a subsequent step, it proves that this assumption holds in all code whose execution might interleave with such loop. At the core of the analysis, we use a may-happen-in-parallel analysis to restrict the set of program points whose execution can interleave with the considered loop. Interestingly, the same kind of reasoning can be applied to infer upper bounds on the number of iterations of loops with concurrent interleavings. To the best of our knowledge, this is the first method to automatically bound the cost of such kind of loops.

@inproceedings{AlbertFGM13,
  author = {Elvira Albert and Antonio Flores-Montoya and Samir Genaim and Enrique Martin-Martin},
  title = {Termination and Cost Analysis of Loops with Concurrent Interleavings},
  booktitle = {11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013)},
  editor = {Dang Van Hung and Mizuhito Ogawa},
  pages = {349-364},
  volume = {8172},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  month = oct,
  year = {2013},
  doi = {10.1007/978-3-319-02444-8_25}
}

We present a novel deadlock analysis for concurrent objects based on the results inferred by a points-to analysis and a may-happen-in-parallel (MHP) analysis. Similarly to other analysis, we build a dependency graph such that the absence of cycles in the graph ensures deadlock freeness. An MHP analysis provides an over-approximation of the pairs of program points that may be running in parallel. The crux of the method is that the analysis integrates the MHP information within the dependency graph in order to discard unfeasible cycles that otherwise would lead to false positives. We argue that our analysis is more precise and/or efficient than previous proposals for deadlock analysis of concurrent objects. As regards accuracy, we are able to handle cases that other analyses have pointed out as challenges. As regards efficiency, the complexity of our deadlock analysis is polynomial.

@inproceedings{FloresAG13,
  author = {Antonio Flores-Montoya and Elvira Albert and Samir Genaim},
  title = {May-Happen-in-Parallel based  Deadlock Analysis for Concurrent Objects},
  booktitle = {Formal Techniques for Distributed Systems},
  series = {Lecture Notes in Computer Science},
  month = jun,
  editor = {Dirk Beyer and Michele Boreale},
  publisher = {Springer},
  year = {2013}
}

We present the concepts, usage and prototypical implementation of MayPar, a may-happen-in-parallel (MHP) static analyzer for a distributed asynchronous language based on concurrent objects. Our tool allows analyzing an application and finding out the pairs of statements that can execute in parallel. The information can be displayed by means of a graphical representation of the MHP analysis graph or, in a textual way, as a set of pairs which identify the program points that may run in parallel. The information yield by MayPar can be relevant (1) to spot bugs in the program related to fragments of code which should not run in parallel and also (2) to improve the precision of other analyses which infer more complex properties (e.g., termination and resource consumption).

@inproceedings{AlbertFG12-FSE,
  author = {Elvira Albert and Antonio Flores-Montoya and Samir Genaim},
  title = {MayPar: a may-happen-in-parallel analyzer for concurrent objects},
  editor = {Will Tracz and Martin P. Robillard and
               Tevfik Bultan},
  booktitle = {20th ACM SIGSOFT Symposium on the Foundations of Software
               Engineering (FSE-20), SIGSOFT/FSE'12, Cary, NC, USA - November
               11 - 16, 2012},
  year = {2012},
  month = nov,
  pages = {1-4},
  publisher = {ACM},
  isbn = {978-1-4503-1614-9, 978-1-4503-0443-6}
}

This paper presents a may-happen-in-parallel (MHP) analysis for OO languages based on concurrent objects . In this concurrency model, objects are the concurrency units such that, when a method is invoked on an object o 2 from a task executing on object o 1 , statements of the current task in o 1 may run in parallel with those of the (asynchronous) call on o 2 , and with those of transitively invoked methods. The goal of the MHP analysis is to identify pairs of statements in the program that may run in parallel in any execution. Our MHP analysis is formalized as a method-level ( local ) analysis whose information can be modularly composed to obtain application-level ( global ) information.

@incollection{AlbertFG12,
  author = {Elvira Albert and Antonio Flores-Montoya and Samir Genaim},
  affiliation = {Complutense University of Madrid, Spain},
  title = {Analysis of May-Happen-in-Parallel in Concurrent Objects},
  booktitle = {Formal Techniques for Distributed Systems},
  series = {Lecture Notes in Computer Science},
  editor = {Giese, Holger and Rosu, Grigore},
  publisher = {Springer Berlin / Heidelberg},
  isbn = {978-3-642-30792-8},
  keyword = {Computer Science},
  pages = {35-51},
  volume = {7273},
  url = {http://dx.doi.org/10.1007/978-3-642-30793-5_3},
  doi = {10.1007/978-3-642-30793-5_3},
  year = {2012}
}

Cost analysis aims at automatically approximating the resource consumption (e.g., memory) of executing a program in terms of its input parameters. While cost analysis for sequential programming languages has received considerable attention, concurrency and distribution have been notably less studied. The main challenges (and our contributions) of cost analysis in a concurrent setting are: (1) Inferring precise size relations for data in the program in the presence of shared memory. This information is essential for bounding the number of iterations of loops. (2) Distribution suggests that analysis must keep the cost of the diverse distributed components separate. We handle this by means of a novel form of recurrence equations which are parametric on the notion of cost center, which represents a corresponding component. To the best of our knowledge, our work is the first one to present a general cost analysis framework and an implementation for concurrent OO programs.

@inproceedings{AlbertAGGP11,
  author = {Elvira Albert and Puri Arenas and Samir Genaim and Miguel G\'{o}mez-Zamalloa and Germ\'an Puebla},
  title = {Cost {A}nalysis of {C}oncurrent {OO} Programs},
  booktitle = {The 9th Asian Symposium on Programming Languages and Systems (APLAS'11)},
  series = {Lecture Notes in Computer Science},
  year = {2011},
  month = dec,
  publisher = {Springer},
  pages = {238-254},
  volume = {7078}
}