Towards a formal model of shared memory consistency for Intel ItaniumTM

Provides a simple formal model for Itanium^TM shared memory consistency covering a core set of instructions, that is reverse-engineered from <http://developer.intel.com/design/ia-64/downloads/24531802.htm> and <http://www.cs.utah.edu/mpv/papers/neiger/fmcad2001.pdf>. Our model sheds light on tricky concepts such as causality. It deals with cacheable memory instructions consisting of acquire loads, ordinary loads, release stores and ordinary stores, as well as memory fences. It does not currently handle atomic read-modify-writes, non-cacheable memory or special rules pertaining to data dependencies involving registers. Despite its simplicity, our model captures all published ordering properties of the instructions we consider. While operational models have been proposed for commercial shared memory systems (notably for Sparc V9), a notable feature of our operational model is its use of a few explicit devices such as vector timestamps to clearly describe the tricky notion of causality