Advertisement

On Verifying TSO Robustness for Event-Driven Asynchronous Programs

  • Ahmed Bouajjani
  • Constantin EneaEmail author
  • Madhavan Mukund
  • Rajarshi Roy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11028)

Abstract

We present a method for checking whether an event-driven asynchronous program running under the Total Store Ordering (TSO) memory model is robust, i.e., all its TSO computations are equivalent to computations under the Sequential Consistency (SC) semantics. We show that this verification problem can be reduced in polynomial time to a reachability problem in a program with two threads, provided that the original program satisfies a criterion called robustness against concurrency, introduced recently in the literature. This result allows to avoid explicit handling of all concurrent executions in the analysis, which leads to an important gain in complexity.

References

  1. 1.
    Abdulla, P.A., Atig, M.F., Chen, Y.-F., Leonardsson, C., Rezine, A.: Counter-example guided fence insertion under TSO. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 204–219. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_15CrossRefGoogle Scholar
  2. 2.
    Abdulla, P.A., Atig, M.F., Ngo, T.-P.: The best of both worlds: trading efficiency and optimality in fence insertion for TSO. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 308–332. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46669-8_13CrossRefGoogle Scholar
  3. 3.
    Alglave, J., Maranget, L.: Stability in weak memory models. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 50–66. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_6CrossRefGoogle Scholar
  4. 4.
    Atig, M.F., Bouajjani, A., Burckhardt, S., Musuvathi, M.: On the verification problem for weak memory models. ACM Sigplan Not. 45(1), 7–18 (2010)CrossRefGoogle Scholar
  5. 5.
    Bouajjani, A., Derevenetc, E., Meyer, R.: Checking and enforcing robustness against TSO. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 533–553. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-37036-6_29CrossRefzbMATHGoogle Scholar
  6. 6.
    Bouajjani, A., Emmi, M., Enea, C., Ozkan, B.K., Tasiran, S.: Verifying robustness of event-driven asynchronous programs against concurrency. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 170–200. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54434-1_7CrossRefGoogle Scholar
  7. 7.
    Bouajjani, A., Meyer, R., Möhlmann, E.: Deciding robustness against total store ordering. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011. LNCS, vol. 6756, pp. 428–440. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22012-8_34CrossRefGoogle Scholar
  8. 8.
    Burckhardt, S., Musuvathi, M.: Effective program verification for relaxed memory models. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 107–120. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70545-1_12CrossRefzbMATHGoogle Scholar
  9. 9.
    Burnim, J., Sen, K., Stergiou, C.: Sound and complete monitoring of sequential consistency for relaxed memory models. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 11–25. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19835-9_3CrossRefzbMATHGoogle Scholar
  10. 10.
    Emmi, M., Lal, A., Qadeer, S.: Asynchronous programs with prioritized task-buffers. In: Proceedings of the International Symposium on Foundations of Software Engineering, FSE 2012, pp. 48:1–48:11. ACM (2012)Google Scholar
  11. 11.
    Emmi, M., Ozkan, B.K., Tasiran, S.: Exploiting synchronization in the analysis of shared-memory asynchronous programs. In: Proceedings of the International SPIN Symposium on Model Checking of Software, pp. 20–29. ACM (2014)Google Scholar
  12. 12.
    Emmi, M., Qadeer, S., Rakamarić, Z.: Delay-bounded scheduling. SIGPLAN Not. 46(1), 411–422 (2011)CrossRefGoogle Scholar
  13. 13.
    Kuperstein, M., Vechev, M., Yahav, E.: Partial-coherence abstractions for relaxed memory models. In: ACM SIGPLAN Notices, vol. 46, pp. 187–198. ACM (2011)Google Scholar
  14. 14.
    Kuperstein, M., Vechev, M., Yahav, E.: Automatic inference of memory fences. ACM SIGACT News 43(2), 108–123 (2012)CrossRefGoogle Scholar
  15. 15.
    Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 100(9), 690–691 (1979)CrossRefGoogle Scholar
  16. 16.
    Owens, S.: Reasoning about the implementation of concurrency abstractions on x86-TSO. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 478–503. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14107-2_23CrossRefGoogle Scholar
  17. 17.
    Ozkan, B.K., Emmi, M., Tasiran, S.: Systematic asynchrony bug exploration for android apps. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 455–461. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21690-4_28CrossRefGoogle Scholar
  18. 18.
    Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.O.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM 53(7), 89–97 (2010)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Ahmed Bouajjani
    • 1
  • Constantin Enea
    • 1
    Email author
  • Madhavan Mukund
    • 2
  • Rajarshi Roy
    • 2
  1. 1.IRIF, University Paris DiderotParisFrance
  2. 2.Chennai Mathematical InstituteChennaiIndia

Personalised recommendations