Advertisement

Automatic Synthesis of Deterministic Concurrency

  • Veselin Raychev
  • Martin Vechev
  • Eran Yahav
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7935)

Abstract

Many parallel programs are meant to be deterministic: for the same input, the program must produce the same output, regardless of scheduling choices. Unfortunately, due to complex parallel interaction, programmers make subtle mistakes that lead to violations of determinism.

In this paper, we present a framework for static synthesis of deterministic concurrency control: given a non-deterministic parallel program, our synthesis algorithm introduces synchronization that transforms the program into a deterministic one. The main idea is to statically compute inter-thread ordering constraints that guarantee determinism and preserve program termination. Then, given the constraints and a set of synchronization primitives, the synthesizer produces a program that enforces the constraints using the provided synchronization primitives.

To handle realistic programs, our synthesis algorithm uses two abstractions: a thread-modular abstraction, and an abstraction for memory locations that can track array accesses. We have implemented our algorithm and successfully applied it to synthesize deterministic control for a number of programs inspired by those used in the high-performance computing community. For most programs, the synthesizer produced synchronization that is as good or better than the handcrafted synchronization inserted by the programmer.

Keywords

Transition System Memory Location Parallel Program Satisfying Assignment Abstract Domain 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Agarwal, S., Barik, R., Sarkar, V., Shyamasundar, R.K.: May-happen-in-parallel analysis of x10 programs. In: PPoPP 2007: Proceedings of the 12th Symposium on Principles and Practice of Parallel Programming, pp. 183–193. ACM (2007)Google Scholar
  2. 2.
    Aviram, A., Weng, S.-C., Hu, S., Ford, B.: Efficient system-enforced deterministic parallelism. In: OSDI (2010)Google Scholar
  3. 3.
    Berger, E.D., Yang, T., Liu, T., Novark, G.: Grace: safe multithreaded programming for c/c++. In: OOPSLA 2009 (2009)Google Scholar
  4. 4.
    Blumofe, R.D., Joerg, C.F., Kuszmaul, B.C., Leiserson, C.E., Randall, K.H., Zhou, Y.: Cilk: an efficient multithreaded runtime system. In: PPoPP 1995 (1995)Google Scholar
  5. 5.
    Bocchino Jr., R.L., Adve, V.S., Dig, D., Adve, S.V., Heumann, S., Komuravelli, R., Overbey, J., Simmons, P., Sung, H., Vakilian, M.: A type and effect system for deterministic parallel java. In: OOPSLA 2009 (2009)Google Scholar
  6. 6.
    Botincan, M., Dodds, M., Jagannathan, S.: Resource-sensitive synchronization inference by abduction. In: POPL 2012 (2012)Google Scholar
  7. 7.
    Burckhardt, S., Baldassin, A., Leijen, D.: Concurrent programming with revisions and isolation types. In: OOPSLA 2010 (2010)Google Scholar
  8. 8.
    Cherem, S., Chilimbi, T., Gulwani, S.: Inferring locks for atomic sections. In: PLDI 2008 (2008)Google Scholar
  9. 9.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL 1997 (1977)Google Scholar
  10. 10.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978 (1978)Google Scholar
  11. 11.
    Devietti, J., Lucia, B., Ceze, L., Oskin, M.: Dmp: deterministic shared memory multiprocessing. In: ASPLOS 2009 (2009)Google Scholar
  12. 12.
    Gulwani, S.: Dimensions in program synthesis. In: PPDP 2010 (2010)Google Scholar
  13. 13.
    Jeannet, B., Miné, A.: APRON: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  14. 14.
    Jin, G., Zhang, W., Deng, D., Liblit, B., Lu, S.: Automated concurrency-bug fixing. In: OSDI 2012 (2012)Google Scholar
  15. 15.
    Kawaguchi, M., Rondon, P., Bakst, A., Jhala, R.: Deterministic parallelism via liquid effects. In: PLDI 2012 (2012)Google Scholar
  16. 16.
    Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. In: FMCAD 2010 (2010)Google Scholar
  17. 17.
    Lhoták, O., Hendren, L.: Scaling Java points-to analysis using SPARK. In: Hedin, G. (ed.) CC 2003. LNCS, vol. 2622, pp. 153–169. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  18. 18.
    Lu, S., Park, S., Seo, E., Zhou, Y.: Learning from mistakes: a comprehensive study on real world concurrency bug characteristics. In: SIGOPS Oper. Syst. Rev. (2008)Google Scholar
  19. 19.
    Manevich, R., Lev-Ami, T., Sagiv, M., Ramalingam, G., Berdine, J.: Heap decomposition for concurrent shape analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 363–377. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  20. 20.
    McCloskey, B., Zhou, F., Gay, D., Brewer, E.: Autolocker: synchronization inference for atomic sections. In: POPL 2006 (2006)Google Scholar
  21. 21.
    Miné, A.: Static analysis of run-time errors in embedded critical parallel c programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 398–418. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  22. 22.
    Miné, A.: The octagon abstract domain. Higher Order Symbol. Comput. 19, 31–100 (2006)zbMATHCrossRefGoogle Scholar
  23. 23.
    Navabi, A., Zhang, X., Jagannathan, S.: Quasi-static scheduling for safe futures. In: PPoPP 2008 (2008)Google Scholar
  24. 24.
    Olszewski, M., Ansel, J., Amarasinghe, S.: Kendo: efficient deterministic multithreading in software. ASPLOS 2009 (2009)Google Scholar
  25. 25.
    Habanero Multicore Software Research project, http://habanero.rice.edu/hj
  26. 26.
    The SAT4J SAT solver, http://www.sat4j.org/.
  27. 27.
    Vallée-Rai, R., et al.: Soot - a Java Optimization Framework. In: Proceedings of CASCON 1999, pp. 125–135 (1999)Google Scholar
  28. 28.
    Vasudevan, N., Edwards, S.A.: A determinizing compiler. In: PLDI, FIT Session (2009)Google Scholar
  29. 29.
    Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic verification of determinism for structured parallel programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 455–471. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  30. 30.
    Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL 2010 (2010)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Veselin Raychev
    • 1
  • Martin Vechev
    • 1
  • Eran Yahav
    • 2
  1. 1.ETH ZurichSwitzerland
  2. 2.TechnionIsrael

Personalised recommendations