[concurrency-interest] Why does JMM mention sequential consistency (SC)?

Valentin Kovalenko valentin.male.kovalenko at gmail.com
Wed Jun 7 13:11:34 EDT 2017


I truly can't understand this because of the following points:

- (1) It's impossible to reason about correctness of a program as a whole,
and programmers always do it by reasoning about correctness of smaller
parts (objects), and then combine objects into something bigger.
Linearizability allows us to do exactly this because of its locality, while
SC only allows to reason about the whole execution, and I can't see how it
may be practical, or even possible.
- (2) Programmers reason about correctness of objects not by using
sequential consistency, but rather by using restrictions JMM imposes on
executions (e.g. well-formed executions, causality requirements).
- (3) For most of existing programs JMM doesn't guarantee that all
executions will appear to be sequentially consistent, because most of
existing programs are incorrectly synchronized (in a benign way). Please
see the explanation why it is so after my question.

So the question is: if programmers don't (and often can't) use SC for
reasoning about correctness of Java programs, then why JMM even mentions
it? Is it for those who write JVM's (i.e. implement Java language
specification)? If so, then can someone explain why is this useful for JVM
writers?


Explanation of the statement (3)
JMM says
- (a) "When a program contains two conflicting accesses that are not
ordered by a happens-before relationship, it is said to contain a data
race."
(btw, strictly speaking, it's not a program, but execution that may have
read/write actions and contain data races; so it's a little bit strange
wording)
- (b) "A program is correctly synchronized if and only if all sequentially
consistent executions are free of data races."
- (c) "If a program is correctly synchronized, then all executions of the
program will appear to be sequentially consistent."

We all know that String.hashCode method is written in such a way that it
allows existence of executions that have data races on the String.hash
variable (benign, but still data races). And it's hard to imagine a program
that doesn't use String.hashCode implicitly (just use String keys in a
HashMap and voila). Thus we can say, that according to JMM all such
programs (i.e. almost all programs) are incorrectly synchronized, and hence
sequential consistency is not guaranteed.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20170607/1b1e0991/attachment.html>


More information about the Concurrency-interest mailing list