Bounded Phase Analysis of Message-Passing ProgramsReport as inadecuate

Bounded Phase Analysis of Message-Passing Programs - Download this document for free, or read online. Document in PDF available to download.

* Corresponding author 1 Modélisation et Vérification LIAFA - Laboratoire d-informatique Algorithmique : Fondements et Applications

Abstract : We describe a novel technique for bounded analysis of asynchronous message-passing programs with ordered message queues. Our bounding parameter does not limit the number of pending messages, nor the number of -contexts-switches- between processes. Instead, we limit the number of process communication cycles, in which an unbounded number of messages are sent to an unbounded number of processes across an unbounded number of contexts. We show that remarkably, despite the potential for such vast exploration, our bounding scheme gives rise to a simple and efficient program analysis by reduction to sequential programs. As our reduction avoids explicitly representing message queues, our analysis scales irrespectively of queue content and variation.

Keywords : Concurrency Message-Passing Verification

Author: Ahmed Bouajjani - Michael Emmi -



Related documents