Asynchronous programming, analysis and testing with state machines

Abstract

Programming efficient asynchronous systems is challenging because it can often be hard to express the design declaratively, or to defend against data races and interleaving-dependent assertion violations. Previous work has only addressed these challenges in isolation, by either designing a new declarative language, a new data race detection tool or a new testing technique. We present P#, a language for high-reliability asynchronous programming co-designed with a static data race analysis and systematic concurrency testing infrastructure. We describe our experience using P# to write several distributed protocols and port an industrial-scale system internal to Microsoft, showing that the combined techniques, by leveraging the design of P#, are effective in finding bugs.

References

1. T. Andrews, S. Qadeer, S. K. Rajamani, J. Rehof, and Y. Xie. Zing: A model checker for concurrent software. In Proceedings of the 16th International Conference on Computer Aided Verification, volume 3114 of Lecture Notes in Computer Science, pages 484–487. Springer, 2004.
2. Apple Inc. Grand Central Dispatch (GCD) reference, accessed November 2014. URL https://developer.apple.com/library/mac/ documentation/Performance/Reference/GCD_libdispatch_ Ref/index.html.
3. S. Blackshear, B. E. Chang, and M. Sridharan. Thresher: Precise refutations for heap reachability. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 275–286. ACM, 2013.
4. S. Burckhardt, P. Kothari, M. Musuvathi, and S. Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In Proceedings of the 15th Edition of ASPLOS on Architectural Support for Programming Languages and Operating Systems, pages 167–178. ACM, 2010.
5. T. D. Chandra, R. Griesemer, and J. Redstone. Paxos made live: An engineering perspective. In Proceedings of the 26th Annual ACM Symposium on Principles of Distributed Computing, pages 398–407. ACM, 2007.
6. A. Desai, V. Gupta, E. K. Jackson, S. Qadeer, S. K. Rajamani, and D. Zufferey. P: Safe asynchronous event-driven programming. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 321–332. ACM, 2013.
7. A. Desai, P. Garg, and P. Madhusudan. Natural proofs for asynchronous programs using almost-synchronous reductions. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications, pages 709––725. ACM, 2014.
8. A. Desai, S. Qadeer, and S. Seshia. Systematic testing of asynchronous reactive systems. Technical Report MSR-TR-2015-25, Microsoft Research, 2015.
9. M. Emmi, S. Qadeer, and Z. Rakamari´c. Delay-bounded scheduling. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 411–422. ACM, 2011.
10. S. German. Tutorial on verification of distributed cache memory protocols. In Formal Methods in Computer Aided Design, 2004.
11. P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer, 1996.
12. P. Godefroid. Model checking for programming languages using VeriSoft. In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, pages 174–186. ACM, 1997.
13. J. N. Gray. Notes on Data Base Operating Systems. Springer, 1978.
14. O. Gruber and F. Boyer. Ownership-based isolation for concurrent actors on multi-core machines. In Proceedings of the 27th European Conference on Object-Oriented Programming, volume 7920 of Lecture Notes in Computer Science, pages 281–301. Springer, 2013.
15. P. Haller and M. Odersky. Capabilities for uniqueness and borrowing. In Proceedings of the 24th European Conference on Object-Oriented Programming, volume 6183 of Lecture Notes in Computer Science, pages 354–378. Springer, 2010.
16. L. Lamport. The part-time parliament. ACM Transactions on Computer Systems, 16(2):133–169, 1998.
17. S. Lauterburg, R. K. Karmani, D. Marinov, and G. Agha. Evaluating ordering heuristics for dynamic partial-order reduction techniques. In Proceedings of the 13th International Conference on Fundamental Approaches to Software Engineering, volume 6013 of Lecture Notes in Computer Science, pages 308–322. Springer, 2010.
18. D. Leijen, W. Schulte, and S. Burckhardt. The design of a task parallel library. In Proceedings of the 24th ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, pages 227–242. ACM, 2009.
19. 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 8th USENIX Conference on Operating Systems Design and Implementation, pages 267–280. USENIX Association, 2008.
20. S. Negara, R. K. Karmani, and G. Agha. Inferring ownership transfer for efficient message passing. In Proceedings of the 16th ACM Symposium on Principles and Practice of Parallel Programming, pages 81–90. ACM, 2011.
21. M. Odersky, L. Spoon, and B. Venners. Programming in Scala. Artima Inc, 2008.
22. D. Ongaro and J. Ousterhout. In search of an understandable consensus algorithm. In Proceedings of the 2014 USENIX Annual Technical Conference, pages 305–319. USENIX Association, 2014.
23. K. Sen and G. Agha. Automated systematic testing of open distributed programs. In Proceedings of the 9th International Conference on Fundamental Approaches to Software Engineering, volume 3922 of Lecture Notes in Computer Science, pages 339–356. Springer, 2006.
24. I. Stoica, R. Morris, D. Karger, M. F. Kaashoek, and H. Balakrishnan. Chord: A scalable peer-to-peer lookup service for internet applications. In Proceedings of the 2001 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, pages 149–160. ACM, 2001.
25. 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, pages 15–28. ACM, 2014.
26. R. van Renesse and F. B. Schneider. Chain replication for supporting high throughput and availability. In Proceedings of the 6th Symposium on Operating Systems Design and Implementation, pages 91–104. USENIX Association, 2004.
27. C. Varela and G. Agha. Programming dynamically reconfigurable open systems with SALSA. ACM SIGPLAN Notices, 36(12):20–34, 2001.
28. R. Virding, C. Wikström, and M. Williams. Concurrent Programming in Erlang. Prentice Hall International, 2nd edition, 1996.

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 defect analysis

        • Software testing and debugging

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification