Verifying liveness for asynchronous programs

Asynchronous or "event-driven" programming is a popular technique to efficiently and flexibly manage concurrent interactions. In these programs, the programmer can post tasks that get stored in a task buffer and get executed atomically by a non-preemptive scheduler at a future point. We give a decision procedure for the fair termination property of asynchronous programs. The fair termination problem asks, given an asynchronous program and a fairness condition on its executions, does the program always terminate on fair executions? The fairness assumptions rule out certain undesired bad behaviors, such as where the scheduler ignores a set of posted tasks forever, or where a non-deterministic branch is always chosen in one direction. Since every liveness property reduces to a fair termination property, our decision procedure extends to liveness properties of asynchronous programs. Our decision procedure for the fair termination of asynchronous programs assumes all variables ar...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko
• Keywords: Fair Termination, Fair Termination Problem, Fair Termination Property, POPL 2009, Programming Languages