2
$\begingroup$

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.

  1. Roscoe, B. (1998). The theory and practice of concurrency.
  2. Bowman, H., & Gomez, R. (2006). Concurrency theory: calculi an automata for modelling untimed and timed concurrent systems. Springer Science & Business Media.
  3. Gorrieri, R., & Versari, C. (2015). Introduction to concurrency theory: transition systems and CCS. Springer.
$\endgroup$
2
  • $\begingroup$ I would be careful with the term unsound, I don't think it conveys your question and thoughts very well. The model doesn't match the reality of some programs in on some CPUs with some optimization settings. But that's not the models fault and it does apply to other settings. $\endgroup$
    – orlp
    Mar 7 at 18:29
  • $\begingroup$ My intention is to not blame the model but to understand the reason why people choose to use this model. As far as I could find out, the CPU architectures implemented by both AMD and Intel use some form of total store ordering memory model and sequential consistency is unsound with respect to such weak memory models. It seems there exist other architectures which use even weaker memory models. So, I'd be very interested to know about how common it is to encounter a setting in which the sequential consistency model is sound. $\endgroup$
    – Barte
    Mar 7 at 19:34
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.