Bounded Phase Analysis of Message-Passing Programs

Date: Thursday, October 18, 2012
Speaker: Michael Emmi
Venue: TU Wien

We describe a novel technique for bounded analysis of asynchronousmessage-passing programs with ordered message queues. Our boundingparameter does not limit the number of pending messages, nor thenumber of “context-switches” between processes. Instead, we limit thenumber of process communication cycles, in which an unbounded numberof messages are sent to an unbounded number of processes across anunbounded number of contexts. We show that remarkably, despite thepotential for such vast exploration, our bounding scheme gives rise toa simple and efficient program analysis by reduction to sequentialprograms. As our reduction avoids explicitly representing messagequeues, our analysis scales irrespectively of queue content andvariation.

Posted in RiSE Seminar