Parrot: a practical runtime for deterministic, stable, and reliable threads

ABSTRACT

Multithreaded programs are hard to get right. A key reason is that the contract between developers and runtimes grants exponentially many schedules to the runtimes. We present Parrot, a simple, practical runtime with a new contract to developers. By default, it orders thread synchronizations in the well-defined round-robin order, vastly reducing schedules to provide determinism (more precisely, deterministic synchronizations) and stability (i.e., robustness against input or code perturbations, a more useful property than determinism). When default schedules are slow, it allows developers to write intuitive performance hints in their code to switch or add schedules for speed. We believe this "meet in the middle" contract eases writing correct, efficient programs.

We further present an ecosystem formed by integrating Parrot with a model checker called dbug. This ecosystem is more effective than either system alone: dbug checks the schedules that matter to Parrot, and Parrot greatly increases the coverage of dbug.

Results on a diverse set of 108 programs, roughly 10× more than any prior evaluation, show that Parrot is easy to use (averaging 1.2 lines of hints per program); achieves low overhead (6.9% for 55 real-world programs and 12.7% for all 108 programs), 10× better than two prior systems; scales well to the maximum allowed cores on a 24-core server and to different scales/types of workloads; and increases Dbug's coverage by 10⁶--10¹⁹⁷³⁴ for 56 programs. Parrot's source code, entire benchmark suite, and raw results are available at github.com/columbia/smt-mc.

References

1. Complete source code, benchmark suite, and raw results of the PARROT thread runtime. https://github.com/columbia/smt-mc.
2. The Princeton application repository for shared-memory computers (PARSEC). http://parsec.cs.princeton.edu/.
3. Parallel BZIP2 (PBZIP2). http://compression.ca/pbzip2/.
4. Aget. http://www.enderunix.org/aget/.
5. J. Albrecht, C. Tuttle, A. C. Snoeren, and A. Vahdat. Loose synchronization for large-scale networked systems. In Proceedings of the USENIX Annual Technical Conference (USENIX '06), pages 28--28, 2006.
6. A. Aviram, S.-C. Weng, S. Hu, and B. Ford. Efficient system-enforced deterministic parallelism. In Proceedings of the Ninth Symposium on Operating Systems Design and Implementation (OSDI '10), Oct. 2010.
7. A. F. Aviram. Deterministic OpenMP. PhD thesis, Yale University, 2012.
8. Bench3n. http://libdb.wordpress.com/3n1/.
9. T. Bergan, O. Anderson, J. Devietti, L. Ceze, and D. Grossman. CoreDet: a compiler and runtime system for deterministic multithreaded execution. In Fifteenth International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '10), pages 53--64, Mar. 2010.
10. T. Bergan, N. Hunt, L. Ceze, and S. D. Gribble. Deterministic process groups in dOS. In Proceedings of the Ninth Symposium on Operating Systems Design and Implementation (OSDI '10), Oct. 2010.
11. T. Bergan, L. Ceze, and D. Grossman. Input-covering schedules for multithreaded programs. In Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '13), Oct. 2013.
12. E. Berger, T. Yang, T. Liu, D. Krishnan, and A. Novark. Grace: safe and efficient concurrent programming. In Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '09), pages 81--96, Oct. 2009.
13. Berkeley DB. http://www.sleepycat.com.
14. O. A. R. Board. OpenMP application program interface version 3.0, May 2008.
15. R. L. Bocchino, Jr., V. S. Adve, D. Dig, S. V. Adve, S. Heumann, R. Komuravelli, J. Overbey, P. Simmons, H. Sung, and M. Vakilian. A type and effect system for deterministic parallel java. In Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA '09), pages 97--116, Oct. 2009.
16. H. Cui, J. Wu, C.-C. Tsai, and J. Yang. Stable deterministic multithreading through schedule memoization. In Proceedings of the Ninth Symposium on Operating Systems Design and Implementation (OSDI '10), Oct. 2010.
17. H. Cui, J. Wu, J. Gallagher, H. Guo, and J. Yang. Efficient deterministic multithreading through schedule relaxation. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP '11), pages 337--351, Oct. 2011.
18. J. Devietti, B. Lucia, L. Ceze, and M. Oskin. DMP: deterministic shared memory multiprocessing. In Fourteenth International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '09), pages 85--96, Mar. 2009.
19. A. C. Dusseau, R. H. Arpaci, and D. E. Culler. Effective distributed scheduling of parallel workloads. In Proceedings of the 1996 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems (SIGMETRICS '96), pages 25--36, May 1996.
20. D. Engler and K. Ashcraft. RacerX: effective, static detection of race conditions and deadlocks. In Proceedings of the 19th ACM Symposium on Operating Systems Principles (SOSP '03), pages 237--252, Oct. 2003.
21. C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd Annual Symposium on Principles of Programming Languages (POPL '05), pages 110--121, Jan. 2005.
22. P. Godefroid. Model checking for programming languages using verisoft. In Proceedings of the 24th Annual Symposium on Principles of Programming Languages (POPL '97), pages 174--186, Jan. 1997.
23. H. Guo, M. Wu, L. Zhou, G. Hu, J. Yang, and L. Zhang. Practical software model checking via dynamic interface reduction. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP '11), pages 265--278, Oct. 2011.
24. M. D. Hill and M. Xu. Racey: A stress test for deterministic execution. http://www.cs.wisc.edu/~markhill/racey.html.
25. N. Hunt, T. Bergan, L. Ceze, and S. Gribble. DDOS: Taming nondeterminism in distributed systems. In Eighteenth International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '13), pages 499--508, 2013.
26. ImageMagick. http://www.imagemagick.org/script/index.php.
27. M. Isard and A. Birrell. Automatic mutual exclusion. In Proceedings of the 11th USENIX workshop on Hot topics in operating systems (HOTOS '07), pages 3:1--3:6, 2007.
28. G. Jin, W. Zhang, D. Deng, B. Liblit, and S. Lu. Automated concurrency-bug fixing. In Proceedings of the Tenth Symposium on Operating Systems Design and Implementation (OSDI '12), pages 221--236, 2012.
29. H. Jula, D. Tralamazza, Z. Cristian, and C. George. Deadlock immunity: Enabling systems to defend against deadlocks. In Proceedings of the Eighth Symposium on Operating Systems Design and Implementation (OSDI '08), pages 295--308, Dec. 2008.
30. P. Kilby, J. K. Slaney, S. Thiébaux, and T. Walsh. Estimating search tree size. In Proceedings of the 21st national conference on Artificial intelligence (AAAI '06), pages 1014--1019, 2006.
31. C. Killian, J. W. Anderson, R. Jhala, and A. Vahdat. Life, death, and the critical transition: Finding liveness bugs in systems code. In Proceedings of the Fourth Symposium on Networked Systems Design and Implementation (NSDI '07), pages 243--256, Apr. 2007.
32. D. E. Knuth. Estimating the Efficiency of Back-track Programs. Mathematics of Computation, 29 (129):121--136, 1975.
33. N. G. Leveson and C. S. Turner. An investigation of the Therac-25 accidents. Computer, 26(7):18--41, 1993.
34. T. Liu, C. Curtsinger, and E. D. Berger. DTHREADS: efficient deterministic multithreading. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles (SOSP '11), pages 327--336, Oct. 2011.
35. S. Lu, J. Tucek, F. Qin, and Y. Zhou. AVIO: detecting atomicity violations via access interleaving invariants. In Twelfth International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '06), pages 37--48, Oct. 2006.
36. S. Lu, S. Park, C. Hu, X. Ma, W. Jiang, Z. Li, R. A. Popa, and Y. Zhou. Muvi: automatically inferring multi-variable access correlations and detecting related semantic and concurrency bugs. In Proceedings of the 21st ACM Symposium on Operating Systems Principles (SOSP '07), pages 103--116, 2007.
37. S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In Thirteenth International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '08), pages 329--339, Mar. 2008.
38. Mongoose. https://code.google.com/p/mongoose/.
39. MPlayer. http://www.mplayerhq.hu/design7/news.html.
40. M. Musuvathi, D. Y. Park, A. Chou, D. R. Engler, and D. L. Dill. CMC: A pragmatic approach to model checking real code. In Proceedings of the Fifth Symposium on Operating Systems Design and Implementation (OSDI '02), pages 75--88, Dec. 2002.
41. M. Musuvathi, S. Qadeer, T. Ball, G. Basler, P. A. Nainar, and I. Neamtiu. Finding and reproducing heisenbugs in concurrent programs. In Proceedings of the Eighth Symposium on Operating Systems Design and Implementation (OSDI '08), pages 267--280, Dec. 2008.
42. NASA Parallel Benchmarks. http://www.nas.nasa.gov/publications/npb.html.
43. M. Olszewski, J. Ansel, and S. Amarasinghe. Kendo: efficient deterministic multithreading in software. In Fourteenth International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '09), pages 97--108, Mar. 2009.
44. M. Olszewski, J. Ansel, and S. Amarasinghe. Scaling deterministic multithreading. In The 2nd Workshop on Determinism and Correctness in Parallel Programming (WODET '11), Mar. 2011.
45. OpenLDAP. http://www.openldap.org/.
46. J. K. Ousterhout. Scheduling Techniques for Concurrent Systems. In Proceedings of Third International Conference on Distributed Computing Systems (ICDCS '82), pages 22--30, 1982.
47. C.-S. Park and K. Sen. Randomized active atomicity violation detection in concurrent programs. In Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering (SIGSOFT '08/FSE-16), pages 135--145, Nov. 2008.
48. S. Park, S. Lu, and Y. Zhou. CTrigger: exposing atomicity violation bugs from their hiding places. In Fourteenth International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '09), pages 25--36, Mar. 2009.
49. S. Park, Y. Zhou, W. Xiong, Z. Yin, R. Kaushik, K. H. Lee, and S. Lu. PRES: probabilistic replay with execution sketching on multiprocessors. In Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP '09), pages 177--192, Oct. 2009.
50. Perf. https://perf.wiki.kernel.org/index.php/Main_Page/.
51. pfscan. http://ostatic.com/pfscan.
52. K. Poulsen. Software bug contributed to blackout. http://www.securityfocus.com/news/8016, Feb. 2004.
53. C. Ranger, R. Raghuraman, A. Penmetsa, G. Bradski, and C. Kozyrakis. Evaluating mapreduce for multi-core and multiprocessor systems. In Proceedings of the 2007 IEEE 13th International Symposium on High Performance Computer Architecture (HPCA '07), pages 13--24, 2007.
54. Redis. http://redis.io/.
55. S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T. E. Anderson. Eraser: A dynamic data race detector for multithreaded programming. ACM Transactions on Computer Systems, pages 391--411, Nov. 1997.
56. K. Sen. Race directed random testing of concurrent programs. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation (PLDI '08), pages 11--21, June 2008.
57. J. Simsa, G. Gibson, and R. Bryant. dBug: Systematic Testing of Unmodified Distributed and Multi-Threaded Systems. In The 18th International SPIN Workshop on Model Checking of Software (SPIN'11), pages 188--193, 2011.
58. SPLASH-2x. http://parsec.cs.princeton.edu/parsec3-doc.htm.
59. STL Parallel Mode. http://gcc.gnu.org/onlinedocs/libstdc++/manual/parallel_mode.html.
60. VTune. http://software.intel.com/en-us/intel-vtune-amplifier-xe/.
61. Y. Wang, T. Kelly, M. Kudlur, S. Lafortune, and S. Mahlke. Gadara: Dynamic deadlock avoidance for multithreaded programs. In Proceedings of the Eighth Symposium on Operating Systems Design and Implementation (OSDI '08), pages 281--294, Dec. 2008.
62. J. Wu, H. Cui, and J. Yang. Bypassing races in live applications with execution filters. In Proceedings of the Ninth Symposium on Operating Systems Design and Implementation (OSDI '10), Oct. 2010.
63. J. Wu, Y. Tang, G. Hu, H. Cui, and J. Yang. Sound and precise analysis of parallel programs through schedule specialization. In Proceedings of the ACM SIGPLAN 2012 Conference on Programming Language Design and Implementation (PLDI '12), pages 205--216, June 2012.
64. W. Xiong, S. Park, J. Zhang, Y. Zhou, and Z. Ma. Ad hoc synchronization considered harmful. In Proceedings of the Ninth Symposium on Operating Systems Design and Implementation (OSDI '10), Oct. 2010.
65. J. Yang, P. Twohey, D. Engler, and M. Musuvathi. Using model checking to find serious file system errors. In Proceedings of the Sixth Symposium on Operating Systems Design and Implementation (OSDI '04), pages 273--288, Dec. 2004.
66. J. Yang, C. Sar, and D. Engler. Explode: a lightweight, general system for finding serious storage system errors. In Proceedings of the Seventh Symposium on Operating Systems Design and Implementation (OSDI '06), pages 131--146, Nov. 2006.
67. J. Yang, T. Chen, M. Wu, Z. Xu, X. Liu, H. Lin, M. Yang, F. Long, L. Zhang, and L. Zhou. MODIST: Transparent model checking of unmodified distributed systems. In Proceedings of the Sixth Symposium on Networked Systems Design and Implementation (NSDI '09), pages 213--228, Apr. 2009.
68. J. Yang, A. Cui, S. Stolfo, and S. Sethumadhavan. Concurrency attacks. In the Fourth USENIX Workshop on Hot Topics in Parallelism (HOTPAR '12), June 2012.
69. J. Yang, H. Cui, and J. Wu. Determinism is over-rated: What really makes multithreaded programs hard to get right and what can be done about it? In the Fifth USENIX Workshop on Hot Topics in Parallelism (HOTPAR '13), June 2013.
70. J. Yang, H. Cui, J. Wu, Y. Tang, and G. Hu. Determinism is not enough: Making parallel programs reliable with stable multithreading. Communications of the ACM, 2014.
71. Y. Yu, T. Rodeheffer, and W. Chen. RaceTrack: efficient detection of data race conditions via adaptive tracking. In Proceedings of the 20th ACM Symposium on Operating Systems Principles (SOSP '05), pages 221--234, Oct. 2005.
72. W. Zhang, C. Sun, and S. Lu. ConMem: detecting severe concurrency bugs through an effect-oriented approach. In Fifteenth International Conference on Architecture Support for Programming Languages and Operating Systems (ASPLOS '10), pages 179--192, Mar. 2010.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Reliability

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Extra-functional properties

      • Software reliability

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification