Why sequential consistency model is widely used if it is unsound From this talk and these lecture notes here and here I learned that sequential consistency does not actually model what really happens in practice. However, it is also pointed out that most of the work in formal methods assumes the sequential consistency model even though there exists other models which correctly characterize what really happens in practice. I'm unable to understand why the sequential consistency model is widely used if it is unsound with respect to what happens in practice. Is there a good reason for doing this? What confused me even further was that in the textbooks on concurrency theory that I could access (e.g. [1]. [2], [3]), I could not find any references to this topic.

Roscoe, B. (1998). The theory and practice of concurrency.
Bowman, H., &amp; Gomez, R. (2006). Concurrency theory: calculi an automata for modelling untimed and timed concurrent systems. Springer Science &amp; Business Media.
Gorrieri, R., &amp; Versari, C. (2015). Introduction to concurrency theory: transition systems and CCS. Springer.
The underlying hardware often has more relaxed memory ordering compared to SC. For example, the X86 will allow for older stores to be reordered with newer loads for a different address due to store buffers. So instead of having a total order over all loads and stores (SC), you only get a total order over all store (TSO). ARM is even more relaxed. And apart from the hardware, the compiler can also reorder instructions if this isn't prohibited.
There are also weak memory models. Weak memory models are a relaxation of strong memory models like SC/TSO because a distinction is made between plain loads and stores and synchronizing loads/stores.
For most engineer it is way too difficult to reason about any other model than SC. SC is often the most intuitive model and that is why many API's are SC (e.g. a C++ atomic by default is SC or Java volatile) and why language level memory models like the Java Memory Model are rooted in SC. Only the experts understand how to relax consistency in favor of improved scalability/performance.