Document Open Access Logo

The Benefits of Duality in Verifying Concurrent Programs under TSO

Authors Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, Tuan Phong Ngo

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.5.pdf
  • Filesize: 0.64 MB
  • 15 pages

Document Identifiers

Author Details

Parosh Aziz Abdulla
Mohamed Faouzi Atig
Ahmed Bouajjani
Tuan Phong Ngo

Cite As Get BibTex

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo. The Benefits of Duality in Verifying Concurrent Programs under TSO. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.CONCUR.2016.5

Abstract

We address the problem of verifying safety properties of concurrent programs running over the TSO memory model. Known decision procedures for this model are based on complex encodings of store buffers as lossy channels. These procedures assume that the number of processes is fixed. However, it is important in general to prove correctness of a system/algorithm in a parametric way with an arbitrarily large number of processes. In this paper, we introduce an alternative (yet equivalent) semantics to the classical one for the TSO model that is more amenable for efficient algorithmic verification and for extension to parametric verification. For that, we adopt a dual view where load buffers are used instead of store buffers. The flow of information is now from the memory to load buffers. We show that this new semantics allows (1) to simplify drastically the  safety analysis  under TSO, (2) to obtain a spectacular gain in efficiency and scalability compared to existing procedures, and (3) to extend easily the decision procedure to the parametric case, which allows to obtain a new decidability result, and more importantly, a verification algorithm that is more general and more efficient in practice than the one for bounded instances.

Subject Classification

Keywords
  • Weak Memory Models
  • Reachability Problem
  • Parameterized Systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. P. Abdulla, S. Aronis, M.F. Atig, B. Jonsson, C. Leonardsson, and K. Sagonas. Stateless model checking for TSO and PSO. In TACAS, volume 9035 of LNCS, pages 353-367. Springer, 2015. Google Scholar
  2. P.A. Abdulla, M.F. Atig, Y.F. Chen, C. Leonardsson, and A. Rezine. Counter-example guided fence insertion under TSO. In TACAS 2012, pages 204-219, 2012. Google Scholar
  3. P.A. Abdulla, M.F. Atig, Y.F. Chen, C. Leonardsson, and A. Rezine. Memorax, a precise and sound tool for automatic fence insertion under TSO. In TACAS, pages 530-536, 2013. Google Scholar
  4. P.A. Abdulla, M.F. Atig, and N.T. Phong. The best of both worlds: Trading efficiency and optimality in fence insertion for TSO. In ESOP 2015, pages 308-332, 2015. Google Scholar
  5. P.A. Abdulla, K. Cerans, B. Jonsson, and Y.K. Tsay. General decidability theorems for infinite-state systems. In LICS'96, pages 313-321. IEEE Computer Society, 1996. Google Scholar
  6. Parosh Aziz Abdulla. Well (and better) quasi-ordered transition systems. Bulletin of Symbolic Logic, 16(4):457-515, 2010. Google Scholar
  7. S. Adve and K. Gharachorloo. Shared memory consistency models: a tutorial. Computer, 29(12), 1996. Google Scholar
  8. S. Adve and M. D. Hill. Weak ordering - a new definition. In ISCA, 1990. Google Scholar
  9. J. Alglave, D. Kroening, and M. Tautschnig. Partial orders for efficient bounded model checking of concurrent software. In CAV, volume 8044 of LNCS, pages 141-157, 2013. Google Scholar
  10. Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM TOPLAS, 36(2):7:1-7:74, 2014. Google Scholar
  11. M. F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. On the verification problem for weak memory models. In POPL, 2010. Google Scholar
  12. M.F. Atig, A. Bouajjani, S. Burckhardt, and M. Musuvathi. What’s decidable about weak memory models? In ESOP, volume 7211 of LNCS, pages 26-46. Springer, 2012. Google Scholar
  13. Ahmed Bouajjani, Egor Derevenetc, and Roland Meyer. Checking and enforcing robustness against TSO. In ESOP, volume 7792 of LNCS, pages 533-553. Springer, 2013. Google Scholar
  14. S. Burckhardt, R. Alur, and M. M. K. Martin. CheckFence: checking consistency of concurrent data types on relaxed memory models. In PLDI, pages 12-21. ACM, 2007. Google Scholar
  15. Sebastian Burckhardt and Madanlal Musuvathi. Effective program verification for relaxed memory models. In CAV, volume 5123 of LNCS, pages 107-120. Springer, 2008. Google Scholar
  16. Jacob Burnim, Koushik Sen, and Christos Stergiou. Testing concurrent programs on relaxed memory models. In ISSTA, pages 122-132. ACM, 2011. Google Scholar
  17. A. Marian Dan, Y. Meshman, M. T. Vechev, and E. Yahav. Predicate abstraction for relaxed memory models. In SAS, volume 7935 of LNCS, pages 84-104. Springer, 2013. Google Scholar
  18. Brian Demsky and Patrick Lam. Satcheck: Sat-directed stateless model checking for SC and TSO. In OOPSLA 2015, pages 20-36. ACM, 2015. Google Scholar
  19. Egor Derevenetc and Roland Meyer. Robustness against Power is PSpace-complete. In ICALP (2), volume 8573 of LNCS, pages 158-170. Springer, 2014. Google Scholar
  20. M. Dubois, C. Scheurich, and F. A. Briggs. Memory access buffering in multiprocessors. In ISCA, 1986. Google Scholar
  21. A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. Google Scholar
  22. Michael Kuperstein, Martin T. Vechev, and Eran Yahav. Automatic inference of memory fences. In FMCAD, pages 111-119. IEEE, 2010. Google Scholar
  23. Michael Kuperstein, Martin T. Vechev, and Eran Yahav. Partial-coherence abstractions for relaxed memory models. In PLDI, pages 187-198. ACM, 2011. Google Scholar
  24. L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comp., C-28(9), 1979. Google Scholar
  25. Feng Liu, Nayden Nedev, Nedyalko Prisadnikov, Martin T. Vechev, and Eran Yahav. Dynamic synthesis for relaxed memory models. In PLDI '12, pages 429-440, 2012. Google Scholar
  26. S. Owens, S. Sarkar, and P. Sewell. A better x86 memory model: x86-tso. In TPHOL, 2009. Google Scholar
  27. P. Sewell, S. Sarkar, S. Owens, F. Z. Nardelli, and M. O. Myreen. x86-tso: A rigorous and usable programmer’s model for x86 multiprocessors. CACM, 53, 2010. Google Scholar
  28. D. Weaver and T. Germond, editors. The SPARC Architecture Manual Version 9. PTR Prentice Hall, 1994. Google Scholar
  29. Y. Yang, G. Gopalakrishnan, G. Lindstrom, and K. Slind. Nemos: A framework for axiomatic and executable specifications of memory consistency models. In IPDPS. IEEE, 2004. Google Scholar
  30. N. Zhang, M. Kusano, and C. Wang. Dynamic partial order reduction for relaxed memory models. In PLDI, pages 250-259. ACM, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact