Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings
| Autor: | Antonio Flores-Montoya, Elvira Albert, Enrique Martin-Martin, Samir Genaim |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
LOOP (programming language)
Computer science Concurrency 020207 software engineering 0102 computer and information sciences 02 engineering and technology Static analysis 01 natural sciences Set (abstract data type) Core (game theory) Computational Theory and Mathematics 010201 computation theory & mathematics Artificial Intelligence restrict Termination analysis 0202 electrical engineering electronic engineering information engineering Actor model Algorithm Software |
| Zdroj: | Journal of Automated Reasoning. 59:47-85 |
| ISSN: | 1573-0670 0168-7433 |
| DOI: | 10.1007/s10817-016-9400-6 |
| Popis: | By following a rely-guarantee style of reasoning, we present novel termination and cost analyses for concurrent programs that, in order to prove termination or infer the cost of a considered loop: (1) infer the termination/cost of each loop as if it were a sequential one, imposing assertions on how shared-data is modified concurrently; and then (2) prove that these assertions cannot be violated infinitely many times and, for cost analysis, infer how many times they are violated. 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. Interestingly, the same kind of reasoning can be applied to prove termination and 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. We have implemented our analysis for an actor-based language, and showed its accuracy and efficiency by applying it on several typical applications for concurrent programs and on an industrial case study. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink