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. O. Burkart and B. Steffen. Pushdown processes: Parallel composition and model checking. In CONCUR '94, volume 836 of LNCS, pages 98--113. Springer, 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. P. Chandrasekaran, C.L. Conway, J.M. Joy, and S.K. Rajamani. Programming asynchronous layers with CLARITY. In ESEC/SIGSOFT FSE, pages 65--74. ACM, 2007.
4. R. Cunningham and E. Kohler. Making events less slippery with Eel. In HotOS-X, 2005.
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. J. Fischer, R. Majumdar, and T. Millstein. Tasks: Language support for event-driven programming. In PEPM '07. ACM, 2007.
7. D. Gay, P. Levis, R. von Behren, M. Welsh, E. Brewer, and D. Culler. The nesC language: A holistic approach to networked embedded systems. In PLDI '03, pages 1--11. ACM, 2003.
8. J. Hill, R. Szewczyk, A. Woo, S. Hollar, D. Culler, and K. Pister. System architecture directions for networked sensors. In ASPLOS '00, pages 93--104. ACM, 2000.
9. John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation (2nd Edition). Addison Wesley, 2000.
10. P. Jancar. Decidability of a temporal logic problem for petri nets. Theoretical Computer Science, 74(1):71--93, 1990.
11. R. Jhala and R. Majumdar. Interprocedural analysis of asynchronous programs. In POPL '07, pages 339--350. ACM, 2007.
12. R.M. Karp and R.E. Miller. Parallel program schemata. Journal of Comput. Syst. Sci., 3(2):147--195, 1969.
13. E. Kohler, R. Morris, B. Chen, J. Jannotti, and M.F. Kaashoek. The Click modular router. ACM TOCS, 18(3):263--297, 2000.
14. M. Krohn, E. Kohler, and M.F. Kaashoek. Events can make sense. In USENIX Annual Technical Conference, 2007.
15. D.J. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In ICALP '81, volume 115 of LNCS, pages 264--277. Springer, 1981.
16. P. Li and S. Zdancewic. Combining events and threads for scalable network services. In PLDI '07: Programming Languages Design and Implementation, pages 189--199. ACM, 2007.
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. Z. Manna and A. Pnueli. Temporal verification of reactive systems: Progress. Draft, 1996.
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. M. Minsky. Finite and Infinite Machines. Prentice-Hall, 1967.
23. V.S. Pai, P. Druschel, and W. Zwaenepoel. Flash: An efficient and portable web server. In Proc. USENIX Tech. Conf., pages 199--212. Usenix, 1999.
24. R.J. Parikh. On context-free languages. Journal of the ACM, 13(4):570--581, 1966.
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 TOPLAS, 22(2):416--430, 2000.
28. W. Reisig. Petri nets: An introduction. Springer, 1986.
29. T. Reps, S. Horwitz, and M. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL '95, pages 49--61. ACM, 1995.
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. I. Walukiewicz. Pushdown Processes: Games and Model-Checking. Information and Computation, 164(2):234--263, 2001.
37. H.-C. Yen. A unified approach for deciding the existence of certain Petri net paths. Information and Computation, 96(1):119--137, 1992.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification