Advertisement

On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency

  • Alex HornEmail author
  • Daniel Kroening
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9039)

Abstract

Concurrent systems are notoriously difficult to analyze, and technological advances such as weak memory architectures greatly compound this problem. This has renewed interest in partial order semantics as a theoretical foundation for formal verification techniques. Among these, symbolic techniques have been shown to be particularly effective at finding concurrency-related bugs because they can leverage highly optimized decision procedures such as SAT/SMT solvers. This paper gives new fundamental results on partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. In particular, we give the theoretical basis for a decision procedure that can handle a fragment of concurrent programs endowed with least fixed point operators. In addition, we show that a certain partial order semantics of relaxed sequential consistency is equivalent to the conjunction of three extensively studied weak memory axioms by Alglave et al. An important consequence of this equivalence is an asymptotically smaller symbolic encoding for bounded model checking which has only a quadratic number of partial order constraints compared to the state-of-the-art cubic-size encoding.

Keywords

Partial Order Memory Location Concurrent System Data Race Quadratic Number 
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.

References

  1. 1.
    Hoare, C.A., Möller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra and its foundations. J. Log. Algebr. Program. 80(6), 266–296 (2011)CrossRefzbMATHMathSciNetGoogle Scholar
  2. 2.
    Hoare, T., van Staden, S.: The laws of programming unify process calculi. Sci. Comput. Program. 85, 102–114 (2014)CrossRefGoogle Scholar
  3. 3.
    Hoare, T., van Staden, S.: In praise of algebra. Formal Aspects of Computing 24(4-6), 423–431 (2012)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Hoare, T., van Staden, S., Möller, B., Struth, G., Villard, J., Zhu, H., O’Hearn, P.: Developments in Concurrent Kleene Algebra. In: Höfner, P., Jipsen, P., Kahl, W., Müller, M.E. (eds.) RAMiCS 2014. LNCS, vol. 8428, pp. 1–18. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  5. 5.
    Pratt, V.: Modeling concurrency with partial orders. Int. J. Parallel Program. 15(1), 33–71 (1986)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Gischer, J.L.: The equational theory of pomsets. Theor. Comput. Sci. 61(2-3), 199–224 (1988)CrossRefzbMATHMathSciNetGoogle Scholar
  7. 7.
    Petri, C.A.: Communication with automata. PhD thesis, Universität Hamburg (1966)Google Scholar
  8. 8.
    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefzbMATHGoogle Scholar
  9. 9.
    Grabowski, J.: On partial languages. Fundam. Inform. 4(2), 427–498 (1981)zbMATHMathSciNetGoogle Scholar
  10. 10.
    Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part I. Theor. Comput. Sci. 13(1), 85–108 (1981)CrossRefzbMATHMathSciNetGoogle Scholar
  11. 11.
    Bloom, B., Kwiatkowska, M.: Trade-offs in true concurrency: Pomsets and Mazurkiewicz traces. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1991. LNCS, vol. 598, pp. 350–375. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  12. 12.
    Feigenbaum, J., Kahn, J., Lund, C.: Complexity results for POMSET languages. SIAM J. Discret. Math. 6(3), 432–442 (1993)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Laurence, M.R., Struth, G.: Completeness theorems for Bi-Kleene algebras and series-parallel rational pomset languages. In: Höfner, P., Jipsen, P., Kahl, W., Müller, M.E. (eds.) RAMiCS 2014. LNCS, vol. 8428, pp. 65–82. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  14. 14.
    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
  15. 15.
    Ševčík, J., Vafeiadis, V., Zappa Nardelli, F., Jagannathan, S., Sewell, P.: Relaxed-memory concurrency and verified compilation. SIGPLAN Not. 46(1), 43–54 (2011)CrossRefGoogle Scholar
  16. 16.
    Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. SIGPLAN Not. 46(1), 55–66 (2011)CrossRefGoogle Scholar
  17. 17.
    Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Fences in weak memory models (extended version). FMSD 40(2), 170–205 (2012)zbMATHGoogle Scholar
  18. 18.
    Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  19. 19.
    Ésik, Z.: Axiomatizing the subsumption and subword preorders on finite and infinite partial words. Theor. Comput. Sci. 273(1-2), 225–248 (2002)CrossRefzbMATHGoogle Scholar
  20. 20.
    Alglave, J., Maranget, L., Sarkar, S., Sewell, P.: Litmus: Running tests against hardware. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 41–44. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  21. 21.
    Horn, A., Alglave, J.: Concurrent Kleene algebra of partial strings. ArXiv e-prints abs/1407.0385 (July 2014)Google Scholar
  22. 22.
    de Bakker, J.W., Warmerdam, J.H.A.: Metric pomset semantics for a concurrent language with recursion. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 21–49. Springer, Heidelberg (1990)CrossRefGoogle Scholar
  23. 23.
    Lamport, L.: How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput. 28(9), 690–691 (1979)CrossRefzbMATHGoogle Scholar
  24. 24.
    Gharachorloo, K., Lenoski, D., Laudon, J., Gibbons, P., Gupta, A., Hennessy, J.: Memory consistency and event ordering in scalable shared-memory multiprocessors. SIGARCH Comput. Archit. News 18(2SI), 15–26 (1990)CrossRefGoogle Scholar
  25. 25.
    ISO: International Standard ISO/IEC 14882:2014(E) Programming Language C++. International Organization for Standardization (2014) (Ratified, to appear soon)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2015

Authors and Affiliations

  1. 1.University of OxfordOxfordUK

Personalised recommendations