"Formal models for concurrency within programming languages address conflicting requirements from programmers, compilers, and architectures. Despite the large body of literature that exists examining weak memory consistency models for hardware architectures and programming languages, there exists a critical gap in developing automated reasoning frameworks for determining the correctness of the programs that execute over them. In this paper, we propose a framework for the automated verification of operational models of weakly consistent memory within a decidable logic. We shall focus on OCaml’s memory consistency model, which is understood to be an exemplary weakly consistent memory model for safe programming languages. In contrast to the original published semantics of OMM, we shall develop alternative semantics inspired by the geometry of interactions within a version control system to guarantee causal consistency, while being compliant with the original axiomatic semantics.

More precisely, we shall develop an alternative ““combined”” operational semantics for OCaml’s memory consistency model. In our model, we adopt a branch-and-merge semantics to simultaneously describe the behaviors specified by both the original axiomatic semantics and the newly proposed causally consistent operational semantics. The behaviors specified by our alternative semantics can be suitably constituted into a first-order transition system. This facilitates the use of effectively propositional logic, a decidable fragment of first-order logic, as the logical basis to reason about the correctness of program execution over this class of weakly consistent memory. We finally derive an executable specification for OMM in EPR, via an automated theorem prover, IVy that discharges proofs with the help of an SMT-solver like Z3. We thus verify the soundness of OCaml’s axiomatic semantics with respect to its causally consistent operational semantics and propose to explore the verification of liveness properties, like fairness and termination, within weakly consistent memory models.