EventBreak: analyzing the responsiveness of user interfaces through performance-guided test generation

ABSTRACT

Event-driven user interface applications typically have a single thread of execution that processes event handlers in response to input events triggered by the user, the network, or other applications. Programmers must ensure that event handlers terminate after a short amount of time because otherwise, the application may become unresponsive. This paper presents EventBreak, a performance-guided test generation technique to identify and analyze event handlers whose execution time may gradually increase while using the application. The key idea is to systematically search for pairs of events where triggering one event increases the execution time of the other event. For example, this situation may happen because one event accumulates data that is processed by the other event. We implement the approach for JavaScript-based web applications and apply it to three real-world applications. EventBreak discovers events with an execution time that gradually increases in an unbounded way, which makes the application unresponsive, and events that, if triggered repeatedly, reveal a severe scalability problem, which makes the application unusable. The approach reveals two known bugs and four previously unknown responsiveness problems. Furthermore, we show that EventBreak helps in testing that event handlers avoid such problems by bounding a handler's execution time.

References

1. P. Abdulla, S. Aronis, B. Jonsson, and K. Sagonas. Optimal dynamic partial order reduction. POPL '14, pages 373--384, New York, NY, USA, 2014. ACM.
2. P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. In LICS, pages 160--170, 1993.
3. R. Alur and M. Yannakakis. Model checking of message sequence charts. CONCUR '99, pages 114--129, London, UK, 1999. Springer-Verlag.
4. T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In CAV, pages 484--487, 2004.
5. S. Basu and T. Bultan. Choreography conformance via synchronizability. WWW '11, pages 795--804, New York, NY, USA, 2011. ACM.
6. S. Basu, T. Bultan, and M. Ouederni. Synchronizability for verification of asynchronously communicating systems. In VMCAI, pages 56--71, 2012.
7. A. Bouajjani and M. Emmi. Bounded phase analysis of message-passing programs. TACAS'12, pages 451--465, Berlin, Heidelberg, 2012. Springer-Verlag.
8. D. Brand and P. Zafiropulo. On communicating finite-state machines. J. ACM, 30(2):323--342, Apr. 1983. ISSN 0004--5411.
9. A. Desai, V. Gupta, E. K. Jackson, S. Qadeer, S. K. Rajamani, and D. Zufferey. P: safe asynchronous event-driven programming. In PLDI, pages 321--332, 2013.
10. M. Emmi, S. Qadeer, and Z. Rakamarić. Delay-bounded scheduling. POPL '11, pages 411--422, New York, NY, USA, 2011. ACM.
11. J. Fisher, T. A. Henzinger, M. Mateescu, and N. Piterman. Bounded asynchrony: Concurrency for modeling cell-cell interactions. In FMSB, pages 17--32, 2008.
12. C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. POPL '05, pages 110--121, New York, NY, USA, 2005. ACM.
13. P. Godefroid. Model checking for programming languages using verisoft. POPL '97, pages 174--186, New York, NY, USA, 1997. ACM.
14. P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. PhD thesis, University of Liege, 1995.
15. P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods (extended abstract). CAV'93, pages 438--449, London, UK, UK, 1993. Springer-Verlag.
16. P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2):149--164, 1993.
17. M. G. Gouda, E. M. Gurari, T. H. Lai, and L. E. Rosier. On deadlock detection in systems of communicating finite state machines. Comput. Artif. Intell., 6(3):209--228, July 1987. ISSN 0232-0274.
18. G. C. Hunt and J. R. Larus. Singularity: Rethinking the software stack. SIGOPS Oper. Syst. Rev., 41(2):37--49, Apr. 2007. ISSN 0163--5980.
19. R. Jhala and R. Majumdar. Interprocedural analysis of asynchronous programs. POPL '07, pages 339--350, New York, NY, USA, 2007. ACM.
20. C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4): 596--619, 1983.
21. S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In LICS, pages 161--170, 2007.
22. S. La Torre, P. Madhusudan, and G. Parlato. Context-bounded analysis of concurrent queue systems. In TACAS, pages 299--314, 2008.
23. S. Lauterburg, M. Dotta, D. Marinov, and G. Agha. A framework for state-space exploration of java-based actor programs. ASE '09, pages 468--479,Washington, DC, USA, 2009. IEEE Computer Society. ISBN 978-0--7695--3891--4.
24. S. Lauterburg, R. K. Karmani, D. Marinov, and G. Agha. Evaluating ordering heuristics for dynamic partial-order reduction techniques. FASE'10, pages 308--322, Berlin, Heidelberg, 2010. Springer-Verlag.
25. P. Madhusudan. Reasoning about sequential and branching behaviours of message sequence graphs. ICALP '01, pages 809--820, London, UK, UK, 2001. Springer-Verlag.
26. P. Madhusudan and B. Meenakshi. Beyond message sequence graphs. In FSTTCS, pages 256--267, 2001.
27. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL, pages 283--294, 2011.
28. P. Madhusudan, X. Qiu, and A. Stefanescu. Recursive proofs for inductive tree data-structures. In POPL, pages 123--136, 2012.
29. A.W. Mazurkiewicz. Trace theory. In Advances in Petri Nets, pages 279--324, 1986.
30. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '07, pages 446--455, New York, NY, USA, 2007. ACM.
31. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. PLDI '07, pages 446--455, New York, NY, USA, 2007. ACM.
32. R. Palmer, G. Gopalakrishnan, and R. M. Kirby. Semantics driven dynamic partial-order reduction of mpi-based parallel programs. PADTAD '07, pages 43--53, New York, NY, USA, 2007. ACM.
33. E. Pek, X. Qiu, and P. Madhusudan. Natural proofs for data structure manipulation in c using separation logic. In PLDI, page 46, 2014.
34. W. Peng and S. Puroshothaman. Data flow analysis of communicating finite state machines. ACM Trans. Program. Lang. Syst., 13(3):399--442, July 1991. ISSN 0164-0925.
35. W. Peng and S. Purushothaman. Analysis of a class of communicating finite state machines. Acta Inf., 29(6/7): 499--522, 1992.
36. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. TACAS'05, pages 93--107, Berlin, Heidelberg, 2005. Springer-Verlag.
37. S. Qadeer and D. Wu. Kiss: keep it simple and sequential. In PLDI, pages 14--24, 2004.
38. X. Qiu, P. Garg, A. Stefanescu, and P. Madhusudan. Natural proofs for structure, data, and separation. In PLDI, pages 231--242, 2013.
39. K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. CAV'06, pages 300--314, Berlin, Heidelberg, 2006. Springer-Verlag.
40. S. F. Siegel. Efficient verification of halting properties for mpi programs with wildcard receives. VMCAI'05, pages 413--429, Berlin, Heidelberg, 2005. Springer-Verlag.
41. S. F. Siegel and G. S. Avrunin. Modeling wildcard-free mpi programs for verification. In PPOPP, pages 95--106, 2005.
42. S. Tasharofi, R. K. Karmani, S. Lauterburg, A. Legay, D. Marinov, and G. Agha. Transdpor: A novel dynamic partial-order reduction technique for testing actor programs. FMOODS'12/FORTE'12, pages 219--234, Berlin, Heidelberg, 2012. Springer-Verlag.
43. P. Thomson, A. F. Donaldson, and A. Betts. Concurrency testing using schedule bounding: An empirical study. In Proceedings of the 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP '14, pages 15--28, New York, NY, USA, 2014. ACM.
44. A. Udupa, A. Desai, and S. K. Rajamani. Depth bounded explicit-state model checking. In SPIN, pages 57--74, 2011.
45. A. Valmari. Stubborn sets for reduced state space generation. In Proceedings of the 10th International Conference on Applications and Theory of Petri Nets: Advances in Petri Nets 1990, pages 491--515, London, UK, UK, 1991. Springer-Verlag.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Metrics

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging