Finding Non-terminating Executions in Distributed Asynchronous Programs

Programming distributed and reactive asynchronous systems is complex due to the lack of synchronization between concurrently executing tasks, and arbitrary delay of message-based communication. As even simple programming mistakes have the capability to introduce divergent behavior, a key liveness property is eventual quiescence: for any finite number of external stimuli (e.g., client-generated events), only a finite number of internal messages are ever created. In this work we propose a practical three-step reduction-based approach for detecting divergent executions in asynchronous programs. As a first step, we give a code-to-code translation reducing divergence of an asynchronous program P to completed state-reachability—i.e., reachability to a given state with no pending asynchronous tasks—of a polynomially-sized asynchronous program P . In the second step, we give a code-to-code translation under-approximating completed state-reachability of P by statereachability of a polyno...

• Type: Journal
• Year: 2012
• Where: SAS
• Authors: Michael Emmi, Akash Lal
• Keywords: Code Translation, Divergent Behavior, External Stimuli, Formal Methods, SAS 2012