When verifying a concurrent program, it is usual to assume that memory is
sequentially consistent. However, most modern multiprocessors depend on store
buffering for efficiency, and provide native sequential consistency only at a
substantial performance penalty. To regain sequential consistency, a programmer
has to follow an appropriate programming discipline. However, na\"ive
disciplines, such as protecting all shared accesses with locks, are not
flexible enough for building high-performance multiprocessor software.