Non-preemptive Semantics for Data-Race-Free Programs

  • Siyang XiaoEmail author
  • Hanru Jiang
  • Hongjin Liang
  • Xinyu Feng
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)


It is challenging to reason about the behaviors of concurrent programs because of the non-deterministic interleaving execution of threads. To simplify the reasoning, we propose a non-preemptive semantics for data-race-free (DRF) concurrent programs, where a thread yields the control of the CPU only at certain carefully-chosen program points. We formally prove that DRF concurrent programs behave the same in the standard interleaving semantics and in our non-preemptive semantics. We also propose a novel formulation of data-race-freedom in our non-preemptive semantics, called NPDRF, which is proved equivalent to the standard DRF notion in the interleaving semantics.


Data-race-freedom Interleaving semantics Non-preemptive semantics 


  1. 1.
    Abadi, M., Plotkin, G.: A model of cooperative threads. In: Proceedings of 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, January 2009, pp. 29–40. ACM Press, New York (2009).
  2. 2.
    Adve, S.V., Hill, M.D.: Weak ordering: a new definition. In: Proceedings of 17th Annual International Symposium on Computer Architecture, ISCA 1990, Seattle, WA, June 1990, pp. 2–14. ACM Press, New York (1990).
  3. 3.
    Adve, S.V., Hill, M.D.: A unified formalization of four shared-memory models. IEEE Trans. Parallel Distrib. Syst. 4(6), 613–624 (1993). Scholar
  4. 4.
    von Behren, R., Condit, J., Zhou, F., Necula, G.C., Brewer, E.: Capriccio: scalable threads for internet services. In: Proceedings of 19th ACM Symposium on Operating Systems Principles, SOSP 2003, Bolton Landing, NY, October 2003, pp. 268–281. ACM Press, New York (2003).
  5. 5.
    Beringer, L., Stewart, G., Dockins, R., Appel, A.W.: Verified compilation for shared-memory C. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 107–127. Springer, Heidelberg (2014). Scholar
  6. 6.
    Boudol, G.: Fair cooperative multithreading. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 272–286. Springer, Heidelberg (2007). Scholar
  7. 7.
    Collingbourne, P., Donaldson, A.F., Ketema, J., Qadeer, S.: Interleaving and lock-step semantics for analysis and verification of GPU kernels. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 270–289. Springer, Heidelberg (2013). Scholar
  8. 8.
    Ferreira, R., Feng, X., Shao, Z.: Parameterized memory models and concurrent separation logic. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 267–286. Springer, Heidelberg (2010). Scholar
  9. 9.
    Hower, D.R., et al.: Heterogeneous-race-free memory models. In: Architectural Support for Programming Languages and Operating Systems, ASPLOS 2014, Salt Lake City, UT, March 2014, pp. 427–440. ACM Press (2014).
  10. 10.
    Kojima, K., Igarashi, A.: A Hoare logic for GPU kernels. ACM Trans. Comput. Log. 18(1), Article No. 3 (2017). Scholar
  11. 11.
    Li, P., Zdancewic, S.: Combining events and threads for scalable network services implementation and evaluation of monadic, application-level concurrency primitives. In: Proceedings of 28th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2007, San Diego, CA, June 2007, pp. 189–199. ACM Press, New York (2007).
  12. 12.
    Loring, M.C., Marron, M., Leijen, D.: Semantics of asynchronous JavaScript. In: Proceedings of 13th ACM SIGPLAN Int. Symposium on Dynamic Languages, DLS 2017, Vancouver, BC, October 2017, pp. 51–62. ACM Press, New York (2017).
  13. 13.
    Marino, D., Singh, A., Millstein, T., Musuvathi, M., Narayanasamy, S.: DRFx: a simple and efficient memory model for concurrent programming languages. In: Proceedings of 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, ON, June 2010, pp. 351–362. ACM Press, New York (2010).
  14. 14.
    Vouillon, J.: Lwt: a cooperative thread library. In: Proceedings of the of 2008 ACM SIGPLAN Workshop on ML, ML 2008, Victoria, BC, September 2008, pp. 3–12. ACM Press, New York (2008).
  15. 15.
    Yi, J., Disney, T., Freund, S.N., Flanagan, C.: Cooperative types for controlling thread interference in Java. In: Proceedings of 2012 International Symposium on Software Testing and Analysis, ISSTA 2012, Minneapolis, MN, July 2012, pp. 232–242. ACM Press (2012).
  16. 16.
    Yi, J., Sadowski, C., Flanagan, C.: Cooperative reasoning for preemptive execution. In: Proceedings of 16th ACM Symposium on Principles and Practice of Parallel Programming, PPoPP 2011, San Antonio, TX, February 2011, pp. 147–156. ACM Press, New York (2011).

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Siyang Xiao
    • 1
    Email author
  • Hanru Jiang
    • 1
  • Hongjin Liang
    • 2
  • Xinyu Feng
    • 2
  1. 1.University of Science and Technology of ChinaHefeiChina
  2. 2.State Key Laboratory for Novel Software TechnologyNanjing UniversityNanjingChina

Personalised recommendations