Verifying liveness for asynchronous programs

ABSTRACT

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 are finite-state. Even though variables are finite-state, asynchronous programs can have an unbounded stack from recursive calls made by tasks, as well as an unbounded task buffer of pending tasks. We show a reduction from the fair termination problem for asynchronous programs to fair termination problems on Petri Nets, and our main technical result is a reduction of the latter problem to Presburger satisfiability. Our decidability result is in contrast to multithreaded recursive programs, for which liveness properties are undecidable. While we focus on fair termination, we show our reduction to Petri Nets can be used to prove related properties such as fair nonstarvation (every posted task is eventually executed) and safety properties such as boundedness (find a bound on the maximum number of posted tasks that can be in the task buffer at any point).

REFERENCES

• 1: Olaf Burkart , Bernhard Steffen, Pushdown Processes: Parallel Composition and Model Checking, Proceedings of the Concurrency Theory, p.98-113, August 22-25, 1994
• 2: R. Chadha and M. Viswanathan. Decidability results for well-structured transition systems with auxiliary storage. In CONCUR '07, volume 4703 of LNCS, pages 136--150. Springer, 2007.
• 3: Prakash Chandrasekaran , Christopher L. Conway , Joseph M. Joy , Sriram K. Rajamani, Programming asynchronous layers with CLARITY, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287636]
• 4: Ryan Cunningham , Eddie Kohler, Making events less slippery with eel, Proceedings of the 10th conference on Hot Topics in Operating Systems, p.3-3, June 12-15, 2005, Santa Fe, NM
• 5: J. Esparza and M. Nielsen. Decidability issues for Petri nets -- a survey. Journal of Informatik Processing and Cybernetics, 30(3):143--160, 1994.
• 6: Jeffrey Fischer , Rupak Majumdar , Todd Millstein, Tasks: language support for event-driven programming, Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 15-16, 2007, Nice, France [doi>10.1145/1244381.1244403]
• 7: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 8: Jason Hill , Robert Szewczyk , Alec Woo , Seth Hollar , David Culler , Kristofer Pister, System architecture directions for networked sensors, Proceedings of the ninth international conference on Architectural support for programming languages and operating systems, p.93-104, November 2000, Cambridge, Massachusetts, United States
• 9: John E. Hopcroft , Rajeev Motwani , Rotwani , Jeffrey D. Ullman, Introduction to Automata Theory, Languages and Computability, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2000
• 10: Petr Jančar, Decidability of a temporal logic problem for petri nets, Theoretical Computer Science, v.74 n.1, p.71-93, July 30, 1990
• 11: Ranjit Jhala , Rupak Majumdar, Interprocedural analysis of asynchronous programs, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 12: R.M. Karp and R.E. Miller. Parallel program schemata. Journal of Comput. Syst. Sci., 3(2):147--195, 1969.
• 13: Eddie Kohler , Robert Morris , Benjie Chen , John Jannotti , M. Frans Kaashoek, The click modular router, ACM Transactions on Computer Systems (TOCS), v.18 n.3, p.263-297, Aug. 2000 [doi>10.1145/354871.354874]
• 14: Maxwell Krohn , Eddie Kohler , M. Frans Kaashoek, Events can make sense, 2007 USENIX Annual Technical Conference on Proceedings of the USENIX Annual Technical Conference, p.1-14, June 17-22, 2007, Santa Clara, CA
• 15: Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
• 16: Peng Li , Steve Zdancewic, Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 17: Libasync. http://pdos.csail.mit.edu/6.824--2004/async/.
• 18: Libevent. http://www.monkey.org/provos/libevent/.
• 19: R. Lipton. The reachability problem is exponential-space hard. Technical Report 62, Department of Computer Science, Yale University, 1976.
• 20: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 21: P. Manolios and D. Vroon. Termination analysis with calling context graphs. In CAV '06, volume 4144 of LNCS, pages 401--414. Springer, 2006.
• 22: Marvin L. Minsky, Computation: finite and infinite machines, Prentice-Hall, Inc., Upper Saddle River, NJ, 1967
• 23: Vivek S. Pai , Peter Druschel , Willy Zwaenepoel, Flash: an efficient and portable web server, Proceedings of the annual conference on USENIX Annual Technical Conference, p.15-15, June 06-11, 1999, Monterey, California
• 24: Rohit J. Parikh, On Context-Free Languages, Journal of the ACM (JACM), v.13 n.4, p.570-581, Oct. 1966 [doi>10.1145/321356.321364]
• 25: M. Presburger. Über die vollständigkeit einer gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In Comptes Rendus du I congrès de Mathématiciens des Pays Slaves, pages 92--101. 1929.
• 26: C. Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223--231, 1978.
• 27: G. Ramalingam, Context-sensitive synchronization-sensitive analysis is undecidable, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.2, p.416-430, March 2000 [doi>10.1145/349214.349241]
• 28: Wolfgang Reisig, Petri nets: an introduction, Springer-Verlag New York, Inc., New York, NY, 1985
• 29: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 30: A. Rybalchenko. Temporal Verification with Transition Invariants. PhD thesis, Universität des Saarlandes, 2004.
• 31: H. Seidl, A. Muscholl, T. Schwentick, and P. Habermehl. Counting in trees for free. In ICALP'04, volume 3142 of LNCS, pages 1136--1149. Springer, 2004.
• 32: K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In CAV '06, volume 4144 of LNCS, pages 300--314. Springer, 2006.
• 33: R. Valk and M. Jantzen. The residue of vector sets with applications to decidability problems in Petri nets. Acta Informatica, 21:643--674, 1985.
• 34: R. Valk and G. Vidal-Naquet. Petri nets and regular languages. Journal of Computer and System Sciences, 23(3):299--325, 1981.
• 35: M.Y. Vardi. Verification of concurrent programs -- the automata-theoretic approach. Annals of Pure and Applied Logic, 51:79--98, 1991.
• 36: Igor Walukiewicz, Pushdown processes: games and model-checking, Information and Computation, v.164 n.2, p.234-263, Jan. 29, 2001 [doi>10.1006/inco.2000.2894]
• 37: Hsu-Chun Yen, A unified approach for deciding the existence of certain Petri net paths, Information and Computation, v.96 n.1, p.119-137, Jan. 1992 [doi>10.1016/0890-5401(92)90059-O]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Languages, Reliability, Verification

Keywords:
asynchronous (event-driven) programming, fair termination, liveness, petri nets