Comparison of Two Operational Execution Models for Weak Memory
Models.


Relaxed memory systems are a crucial part of modern hardware
architectures, which allow out-of-order execution of memory
accesses and thereby a more efficient usage of caches and other
optimization techniques.  In this work, we compare two recent
approaches by Boudol et Al. and Mantel et al. to incorporate
relaxed memory models into operational semantics.  We give a
comparision of design decisions to model core characteristics
of relaxed memory models like allowed reorderings, asynchronous
communication, read-early accesses, and their effect on the
expressive power of the semantics and the respective formulation
of sequential consistency.