Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
Termination and Cost Analysis of Loops with Concurrent Interleavings
verfasst von : Elvira Albert, Antonio Flores-Montoya, Samir Genaim, Enrique Martin-Martin
Erschienen in: Automated Technology for Verification and Analysis
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.