Why does JMM mention sequential consistency (SC)?

classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Why does JMM mention sequential consistency (SC)?

Valentin Kovalenko
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.

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Why does JMM mention sequential consistency (SC)?

Alex Otenko
All of these definitions are there so you can talk about the correctness of the program in a hardware-agnostic manner. It is the JVM’s job then to establish the bridge between the abstract notion of correctness and the actual code executed by, and effects observed on the hardware platform.

Sequential Consistency is the weakest (or is it strongest?) correctness guarantee you want to be achievable in JMM. (“Can you at least construct sequentially consistent Java programs?”)


“data race” is a useful term when talking about the program. In order to be able to tell what is wrong with the program, you might need new terms.


Establishing whether some executions are possible such that the program will not be sequentially consistent, is a difficult business. Enumerating all possible executions is not practical, and does not establish universal properties of the algorithm. And yet, this only makes the enumeration of possible executions a useless enterprise, not sequential consistency as a property.


Alex

> On 7 Jun 2017, at 18:11, Valentin Kovalenko <[hidden email]> wrote:
>
> 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.
> _______________________________________________
> Concurrency-interest mailing list
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest

_______________________________________________
Concurrency-interest mailing list
[hidden email]
http://cs.oswego.edu/mailman/listinfo/concurrency-interest
Loading...