Programming with weak consistency guarantees is both a necessity and a pain. It is a necessity, because more and more platforms opt for weak consistency guarantees or even give the developer means of influencing the consistency guarantees. It is a pain, because well-known idioms for synchronization and communication break if the consistency guarantees are chosen too weak.

Since its proposal in 2010, the programming language CAT has become the de-facto standard for formulating consistency guarantees. The Linux kernel, the languages C, C++, Java, and OCaml, the architectures of ARM, Intel, and IBM, as well as NVIDIA and Vulkan all have their consistency guarantees formulated in CAT.

We introduce Dartagnan, a formal verification tool that helps the programmer reason about the behavior of a given (C or SPIR-V) program relative to given consistency guarantees (formulated in CAT). Dartagnan checks whether all consistent executions meet all assertions in the code, reports bugs otherwise, or terminates without a conclusion. Dartagnan is a bounded model checker that unrolls the program into an acyclic form and translates it into logical constraints that are solved with an SMT solver, like Microsoft's Z3 or Yices.

Dartagnan has been instrumental in finding a bug in qspinlock, one of the major lock implementations of the Linux kernel, a development that ultimately lead to new consistency guarantees for the Linux kernel.