%0 Conference Proceedings
%T On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency
%+ University of Oxford
%A Horn, Alex
%A Kroening, Daniel
%Z Part 1: Ensuring Properties of Distributed Systems
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 35th International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE)
%C Grenoble, France
%Y Susanne Graf
%Y Mahesh Viswanathan
%I Springer International Publishing
%3 Formal Techniques for Distributed Objects, Components, and Systems
%V LNCS-9039
%P 19-34
%8 2015-06-02
%D 2015
%R 10.1007/978-3-319-19195-9_2
%K Partial Order
%K Memory Location
%K Concurrent System
%K Data Race
%K Quadratic Number
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-01767325/document
%2 https://inria.hal.science/hal-01767325/file/978-3-319-19195-9_2_Chapter.pdf
%L hal-01767325
%U https://inria.hal.science/hal-01767325
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-LNCS-9039