Flip van Spaendonck: Understanding std::memory_order in C++11 using MCA semantics


Event Details


C++11 introduced many tools to write safe multi threaded code. One of those tools are the std::memory_orders, which specify how memory accesses, including regular, non-atomic memory accesses, are to be ordered around atomic operations. Understanding these memory orders can be quite a complex situation, specifically when different memory orders are combined. We will try to make sense of these by using mCRL2 to analyze all traces possible under MCA semantics. A set of semantics in which all threads perceive memory accesses in the same order.