Is Synchronization Order A *Strict* Total Order?

classic Classic list List threaded Threaded
41 messages Options
123
Reply | Threaded
Open this post in threaded view
|

Is Synchronization Order A *Strict* Total Order?

thurstonn
In the JMM documentation, synchronization order is defined as a total order; perhaps it's just semantics, but I've always been curious whether it is intentional that it isn't defined as a *strict* total order.

Without getting into arcane mathematics, I guess what I'm asking is:

Given a program that contains only synchronization actions, but they are independent, e.g.

volatile int x, y

Thread A       Thread B
x = 1             y = 1

Is the following true?

I. *Every* execution of the program has only one and exactly one valid (accurate?) history?

[either

A(x=1)
B(y=1)

or

B(y=1)
A(x=1)
]  

II. or is it possible that it can be said that for some theoretical execution, both histories are equally valid?

My inference has always been that the JMM prescribes I (which implies strict total order) and proscribes II.

Of course, one might say, who cares? or how could you tell the difference? or the "results" of the program are the same . . .




Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Joe Bowbeer
The JMM is written to guarantee sequential consistency for data-race-free programs. As I understand it, sequential consistency (SC) requires that every execution *could* be the result of *some* sequential execution. But, in general, multiple possible sequential executions may exist.

Do you have a different understanding of SC? Or are you questioning why SC was chosen for JMM?

On Mon, May 30, 2016 at 7:40 AM, thurstonn <[hidden email]> wrote:
In the JMM documentation, synchronization order is defined as a total order;
perhaps it's just semantics, but I've always been curious whether it is
intentional that it isn't defined as a *strict* total order.

Without getting into arcane mathematics, I guess what I'm asking is:

Given a program that contains only synchronization actions, but they are
independent, e.g.

volatile int x, y

Thread A       Thread B
x = 1             y = 1

Is the following true?

I. *Every* execution of the program has only one and exactly one valid
(accurate?) history?

[either

A(x=1)
B(y=1)

or

B(y=1)
A(x=1)
]

II. or is it possible that it can be said that for some theoretical
execution, both histories are equally valid?

My inference has always been that the JMM prescribes I (which implies strict
total order) and proscribes II.

Of course, one might say, who cares? or how could you tell the difference?
or the "results" of the program are the same . . .








--
View this message in context: http://jsr166-concurrency.10961.n7.nabble.com/Is-Synchronization-Order-A-Strict-Total-Order-tp13457.html
Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

thurstonn
In reply to this post by thurstonn
Let me try another way:

Imagine we have the previously mentioned program:

volatile int x, y

Thread A       Thread B
x = 1             y = 1

And we have two "observers" Bob and Jill; both of them have the magical ability to observe all hardware state (registers, caches, memory, etc) during the execution of any program *without interfering in said execution*

They record each execution of a program by writing down a history of what they observed.

The above program is run a 1000 times; after each execution, Bob and Jill compare their two histories; they are always in agreement.

For some executions, the history is:
A(x=1)
B(y=1)

for others, it's:
B(y=1)
A(x=1)

Again, Jill's and Bob's histories are always the same.

Then the program is executed for the 1001 time.
Again they compare histories:
Bob:
A(x=1)
B(y=1)

Jill:
B(y=1)
A(x=1)

Bob:  "Hmm, our Java platform is broken; this violates the JMM guarantee of a total order among synchronization actions, i.e. it violates synchronization order"

Jill:   "I'm not so sure; a total order (which is just a binary operator) allows for A(x=1) <= B(y=1) AND B(y=1) <= A(x=1). i.e. it allows for A(x=1) = B(y=1). Our Java platform is OK"

My question is:  who is right (according to the JMM)?



Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Roland Kuhn-2
Your hypothetical observers cannot exist in this universe because the two writes can occur concurrently, with true parallelism: each core writes to its cache, there is no synchronization necessary and hence it is not done. Since the difference is not observable (due to special relativity if nothing else) the question is moot as far as I can see. The JMM only regulates observable behavior, and that is hard enough ;-)

Is there another question behind the one you are currently asking?

Regards, Roland

Sent from my iPhone

> On 31 May 2016, at 11:52, thurstonn <[hidden email]> wrote:
>
> Let me try another way:
>
> Imagine we have the previously mentioned program:
>
> volatile int x, y
>
> Thread A       Thread B
> x = 1             y = 1
>
> And we have two "observers" Bob and Jill; both of them have the magical
> ability to observe all hardware state (registers, caches, memory, etc)
> during the execution of any program *without interfering in said execution*
>
> They record each execution of a program by writing down a history of what
> they observed.
>
> The above program is run a 1000 times; after each execution, Bob and Jill
> compare their two histories; they are always in agreement.
>
> For some executions, the history is:
> A(x=1)
> B(y=1)
>
> for others, it's:
> B(y=1)
> A(x=1)
>
> Again, Jill's and Bob's histories are always the same.
>
> Then the program is executed for the 1001 time.
> Again they compare histories:
> Bob:
> A(x=1)
> B(y=1)
>
> Jill:
> B(y=1)
> A(x=1)
>
> Bob:  "Hmm, our Java platform is broken; this violates the JMM guarantee of
> a total order among synchronization actions, i.e. it violates
> synchronization order"
>
> Jill:   "I'm not so sure; a total order (which is just a binary operator)
> allows for A(x=1) <= B(y=1) AND B(y=1) <= A(x=1). i.e. it allows for A(x=1)
> = B(y=1). Our Java platform is OK"
>
> My question is:  who is right (according to the JMM)?
>
>
>
>
>
>
>
> --
> View this message in context: http://jsr166-concurrency.10961.n7.nabble.com/Is-Synchronization-Order-A-Strict-Total-Order-tp13457p13460.html
> Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
> _______________________________________________
> 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
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Aleksey Shipilev-2
In reply to this post by thurstonn
On 05/31/2016 12:52 PM, thurstonn wrote:
> And we have two "observers" Bob and Jill; both of them have the magical
> ability to observe all hardware state (registers, caches, memory, etc)
> during the execution of any program *without interfering in said execution*

Your question boils down to: are Bob and Jill -- the CPU demons --
observe events "x=1" and "y=1" in the same relative order?

Since there is communication delay involved, you cannot say they have to
observe the events in any particular order. Or, that is to say, the
physical universe where machines exist does not force us to detect both
events in the same relative order. (Aside: this is similar how
introducing the no-faster-than-a-speed-of-light axiom in special
relativity gives raise to relativity of simultaneity itself)

But the actual question that programmer care of is, are *programs*
allowed to observe the different relative order? I.e. if we introduce
the actual reads in the program, do we see the different order of x=1
and y=1? IRIW under JMM says "no". And this is a critical thing: model
is described as behavior observed by *programs*, not by CPU demons.

Now, it is a machine problem how to map the actual physical sequence of
events towards the program-observable behaviors. Barriers and other HW
synchronization primitives are the ways to communicate where that
observable order matters.


> My question is:  who is right (according to the JMM)?

I think you have to get back to Lamport's definition of sequential
consistency and its difference against the strict consistency.

Notably, SC definition states "... the result of any execution is the
same *as if* [emphasis is mine] the operations of all the processors
were executed in some sequential order, and the operations of each
individual processor appear in this sequence in the order specified by
its program."

That "as if"-ness is a crucial part here: under SC-DRF, the outcome of
the data-race-free program is *as if* there was a total order. The exact
order in which the actions were executed is not required to be
consistent with that order (_strict_ consistency requires that).

Introducing external observers that can magically observe the "blurry"
interim state of the system does not violate SC property, because the
program outcome still stays the same.


Thanks,
-Aleksey


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

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

thurstonn
Quoting from the JLS:

17.4.4. Synchronization Order

"Every execution has a synchronization order. A synchronization order is a total order over all of the synchronization actions of an execution. "

That seems like a categorical statement; no references to data-races, sequential consistency, observability, program results, nor, God forbid, special relativity (which isn't relevant since CPUs are not in relative motion with each other).

So for a program with only synchronization actions, the JMM requires some binary operator (the total order) over each pair of actions in the program (in this case, the set {A(x=1), B(y=1}).

What could that binary operator be?
In other words, what, within a program execution, does A(x=1) <= B(y=1) mean?
Could CPUcost(action-x, action-y) be it?  I don't think so.

It seems to me, no matter how hard I might try to avoid it, it means the numerical comparison of time(stamp) of each action, which presents difficulty in precise definition (since, e.g. writes and reads are not instantaneous).

The JMM authors had 2 choices (again when it comes to synchronization actions):

No execution with simultaneous (A(x=1) = B(y=1)) actions are allowed (Bob's understanding, and implied by a *strict* total order) or

Simultaneous (A(x=1) = B(y=1)) actions are allowed (Jill's understanding, and implied by a *non-strict* total order)

I'm assuming from your reply that it's the latter (Jill's) meaning, but I fail to see how any reasonable interpretation of the sentence I quoted above could be:
"Well, since no threads observe any other thread's actions (true in this case), then scratch the whole requirement about synchronization order" which you also seem to be suggesting
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Joe Bowbeer

The program you are referring to can be obtained by making every field volatile. However, unobservable synchronization actions, including volatile reads and writes, can be optimized and/or elided.

On May 31, 2016 11:06 AM, "thurstonn" <[hidden email]> wrote:
Quoting from the JLS:

17.4.4. Synchronization Order

"Every execution has a synchronization order. A synchronization order is a
total order over all of the synchronization actions of an execution. "

That seems like a categorical statement; no references to data-races,
sequential consistency, observability, program results, nor, God forbid,
special relativity (which isn't relevant since CPUs are not in relative
motion with each other).

So for a program with only synchronization actions, the JMM requires some
binary operator (the total order) over each pair of actions in the program
(in this case, the set {A(x=1), B(y=1}).

What could that binary operator be?
In other words, what, within a program execution, does A(x=1) <= B(y=1)
mean?
Could CPUcost(action-x, action-y) be it?  I don't think so.

It seems to me, no matter how hard I might try to avoid it, it means the
numerical comparison of time(stamp) of each action, which presents
difficulty in precise definition (since, e.g. writes and reads are not
instantaneous).

The JMM authors had 2 choices (again when it comes to synchronization
actions):

No execution with simultaneous (A(x=1) = B(y=1)) actions are allowed (Bob's
understanding, and implied by a *strict* total order) or

Simultaneous (A(x=1) = B(y=1)) actions are allowed (Jill's understanding,
and implied by a *non-strict* total order)

I'm assuming from your reply that it's the latter (Jill's) meaning, but I
fail to see how any reasonable interpretation of the sentence I quoted above
could be:
"Well, since no threads observe any other thread's actions (true in this
case), then scratch the whole requirement about synchronization order" which
you also seem to be suggesting




--
View this message in context: http://jsr166-concurrency.10961.n7.nabble.com/Is-Synchronization-Order-A-Strict-Total-Order-tp13457p13465.html
Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

thurstonn
joe.bowbeer wrote
The program you are referring to can be obtained by making every field
volatile. However, unobservable synchronization actions, including volatile
reads and writes, can be optimized and/or elided.
On May 31, 2016 11:06 AM, "thurstonn" <[hidden email]> wrote:
Of course, hence the program (repeated here)
volatile int x, y

Thread A       Thread B
x = 1             y = 1


Elision is an interesting case;  I interpret that with respect to synchronization order as:

"A synchronization order is a total order over all of the synchronization actions of an execution" where the synchronization actions (after elision) is {}.
No problem there.
Optimization, viz. turning a volatile read/write into a plain one, and therefore not a synchronization action, similarly reduces the execution's SA set.

Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Aleksey Shipilev-2
In reply to this post by thurstonn
On 05/31/2016 07:55 PM, thurstonn wrote:
> "Every execution has a synchronization order. A synchronization order is a
> total order over all of the synchronization actions of an execution. "
>
> That seems like a categorical statement; no references to data-races,
> sequential consistency, observability, program results, nor, God forbid,
> special relativity (which isn't relevant since CPUs are not in relative
> motion with each other).

Notice there are also no references as to whether those actions are the
actual machine actions that Bob and Jill are supposed to observe. And
this is for reason: the program actions in JMM are abstract, and have
little connection with what real systems do. As long as runtime/hardware
can keep the appearances of satisfying JMM requirements, it can do whatever.

The point of my previous note was to highlight that: you are asking the
question what could happen on physical level, using the entities
(actions) on abstract model level. These have little in common. What
happens on physical level is all smoke and mirrors.


> So for a program with only synchronization actions, the JMM requires some
> binary operator (the total order) over each pair of actions in the program
> (in this case, the set {A(x=1), B(y=1}).
>
> What could that binary operator be?
> In other words, what, within a program execution, does A(x=1) <= B(y=1)
> mean?
> Could CPUcost(action-x, action-y) be it?  I don't think so.
>
> It seems to me, no matter how hard I might try to avoid it, it means the
> numerical comparison of time(stamp) of each action, which presents
> difficulty in precise definition (since, e.g. writes and reads are not
> instantaneous).
I think you are trying to drag the abstract notion of action towards its
physical manifestation (e.g. changes in machine state, or associated
ticks in a global time) -- a very dangerous and confusing route.


> The JMM authors had 2 choices (again when it comes to synchronization
> actions):
>
> No execution with simultaneous (A(x=1) = B(y=1)) actions are allowed (Bob's
> understanding, and implied by a *strict* total order) or
>
> Simultaneous (A(x=1) = B(y=1)) actions are allowed (Jill's understanding,
> and implied by a *non-strict* total order)

That equality sign is confusing.

I am probably forgetting a significant part of my training, but these
are the definitions that are consistent with my own memory:

(Weak) total order implies that for all A, B, C in set:
 a) Reflexive:     (A op A)
 b) Antisymmetric: (A op B) and (B op A) => (A = B)
 c) Transitive:    (A op B) and (B op C) => (A op C)
 d) Totality:      (A op B) or (B op A)

Strict total order implies that for all A, B, C in set:
 a) Irreflexive:   !(A op A)
 b) Asymmetric:    (A op B) => !(B op A)
 c) Transitive:    (A op B) and (B op C) => (A op C)
 d) Trichotomy:    Exactly one of (A op B), (B op A), (A = B) is true

Notice (A = B) reads as "A and B are the *same*", not "simultaneous".

The difference is in reflexivity. Does it matter if SO is reflexive or
not? I don't think so.

What does it mean to be simultaneous in SO? Does it mean there exist two
non-equal actions that are *not* ordered by SO relation? This
contradicts totality/trichotomy in either. Does it mean two non-equal
actions have SO in different orders? This breaks anti/asymmetry in either.

Thanks,
-Aleksey



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

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Scott Blum
In reply to this post by thurstonn
I would posit that there is only a strict total order if you try to observe it within the program.  If you add sufficient code to determine which history actually happened, you will in effect force the instructions to be generated to insist on a strict total ordering.  In the absence of that extra code, it's meaningless to ask which happened first.

Imagine a hypothetical implementation where you have two threads running on two processors each with their own data caches.  Each thread might either write its x=1, y=1 to its local cache, or to main memory.  If they write to local cache, there's no rules around when that needs to get pushed through to main memory-- provided no one is doing a volatile read on those fields.  Without the volatile reads you're never forcing the system to reach an absolutely "determined" state.

But I use all these terms loosely because there truly isn't a clear 1:1 mapping between JMM and hardware. The JMM is all about reads and writes and visibility within a program; how and when things actually get written to memory or cache or whatever is an implementation detail of a particular JVM and machine.

TLDR: the JMM doesn't require a strict total ordering unless you try to observe it.

On Tue, May 31, 2016 at 1:42 PM, thurstonn <[hidden email]> wrote:
joe.bowbeer wrote
> The program you are referring to can be obtained by making every field
> volatile. However, unobservable synchronization actions, including
> volatile
> reads and writes, can be optimized and/or elided.
> On May 31, 2016 11:06 AM, "thurstonn" &lt;

> thurston@

> &gt; wrote:

Of course, hence the program (repeated here)
volatile int x, y

Thread A       Thread B
x = 1             y = 1


Elision is an interesting case;  I interpret that with respect to
synchronization order as:

"A synchronization order is a total order over all of the synchronization
actions of an execution" where the synchronization actions (after elision)
is {}.
No problem there.
Optimization, viz. turning a volatile read/write into a plain one, and
therefore not a synchronization action, similarly reduces the execution's SA
set.





--
View this message in context: http://jsr166-concurrency.10961.n7.nabble.com/Is-Synchronization-Order-A-Strict-Total-Order-tp13457p13467.html
Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

thurstonn
In reply to this post by Aleksey Shipilev-2
Aleksey Shipilev-2 wrote

I am probably forgetting a significant part of my training, but these
are the definitions that are consistent with my own memory:

(Weak) total order implies that for all A, B, C in set:
 a) Reflexive:     (A op A)
 b) Antisymmetric: (A op B) and (B op A) => (A = B)
 c) Transitive:    (A op B) and (B op C) => (A op C)
 d) Totality:      (A op B) or (B op A)

Strict total order implies that for all A, B, C in set:
 a) Irreflexive:   !(A op A)
 b) Asymmetric:    (A op B) => !(B op A)
 c) Transitive:    (A op B) and (B op C) => (A op C)
 d) Trichotomy:    Exactly one of (A op B), (B op A), (A = B) is true

Notice (A = B) reads as "A and B are the *same*", not "simultaneous".
Ah, I think that last statement might be the rub; my understanding is that A = B does not mean A and B are the *same*, the irreflexive rule deals with that
"=" is defined by the total order.
The phraseology is extremely awkward; let's replace total order with "binary operator" (subject to the rules you've enumerated), and let's dispense with (ir)reflexivity, as I agree it's completely unnecessary to speak of ordering a SA with respect to itself.

"=" is analogous to equals() vis a vis Java identity (==) (at least as I understand it)

Say I have a set of laptops {Laptop-A, Laptop-B}, 2 physically distinct laptops.
It is meaningless to speak of a total order over that set.
I have to define a binary operator, right?

Say, weight-of-laptop.
In such a case, I can say weight-of-laptop is a total order over {Laptop-A, Laptop-B}; it's not difficult to interpret "=" in that case.

Now my understanding is that weight-of-laptop is *not* a strict total order over say {Laptop-A 1.1kg, Laptop-B 1.1kg}
Because in order to be a total order, either Laptop-A :wol: Laptop-B => "<"
or Laptop-B :wol: Laptop-A => "<".

Similarly, let's define an execution as a set of actions. e.g. {A(x=1), B(y=1)}.
What's a total order over it?
Meaningless right, i.e. I have to define a binary operator.
Now, the JMM doesn't define one; it simply adds that the relations produced by it, must be consistent with (intra-thread) program order; which in the sample trivial program is no restriction at all, since each thread contains a single SA.

The only logical binary operator "implementation" I can think of is:  timestamp of action.
So, my interpretation of synchronization order has been, every possible legal execution's SAs are ordered by "timestamp of action", with the unsolved question being:
does the JMM allow an execution to have a pair of SA's with the same timestamp?

Is that thinking too close to the "physical layer"?  Maybe; it only requires that each SA have a timestamp associated with it, and those timestamps be comparable in the common-sense way





Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Roland Kuhn-2

> 31 maj 2016 kl. 21:37 skrev thurstonn <[hidden email]>:
>
> Aleksey Shipilev-2 wrote
>>
>> I am probably forgetting a significant part of my training, but these
>> are the definitions that are consistent with my own memory:
>>
>> (Weak) total order implies that for all A, B, C in set:
>> a) Reflexive:     (A op A)
>> b) Antisymmetric: (A op B) and (B op A) => (A = B)
>> c) Transitive:    (A op B) and (B op C) => (A op C)
>> d) Totality:      (A op B) or (B op A)
>>
>> Strict total order implies that for all A, B, C in set:
>> a) Irreflexive:   !(A op A)
>> b) Asymmetric:    (A op B) => !(B op A)
>> c) Transitive:    (A op B) and (B op C) => (A op C)
>> d) Trichotomy:    Exactly one of (A op B), (B op A), (A = B) is true
>>
>> Notice (A = B) reads as "A and B are the *same*", not "simultaneous".
>
> Ah, I think that last statement might be the rub; my understanding is that A
> = B does not mean A and B are the *same*, the irreflexive rule deals with
> that
> "=" is defined by the total order.

You can’t have it both ways: if you’re talking mathematics, = means “they can be used interchangeably”, they are the same. And that is exactly what antisymmetry gives you for a total order.

> The phraseology is extremely awkward; let's replace total order with "binary
> operator" (subject to the rules you've enumerated), and let's dispense with
> (ir)reflexivity, as I agree it's completely unnecessary to speak of ordering
> a SA with respect to itself.
>
> "=" is analogous to equals() vis a vis Java identity (==) (at least as I
> understand it)
>
> Say I have a set of laptops {Laptop-A, Laptop-B}, 2 physically distinct
> laptops.
> It is meaningless to speak of a total order over that set.
> I have to define a binary operator, right?
>
> Say, weight-of-laptop.
> In such a case, I can say weight-of-laptop is a total order over {Laptop-A,
> Laptop-B}; it's not difficult to interpret "=" in that case.
>
> Now my understanding is that weight-of-laptop is *not* a strict total order
> over say {Laptop-A 1.1kg, Laptop-B 1.1kg}
> Because in order to be a total order, either Laptop-A :wol: Laptop-B => "<"
> or Laptop-B :wol: Laptop-A => "<".
>
> Similarly, let's define an execution as a set of actions. e.g. {A(x=1),
> B(y=1)}.
> What's a total order over it?
> Meaningless right, i.e. I have to define a binary operator.

Nope, not meaningless: for every execution there is at least one total order that results in the observed outcome. That binary operator is defined for you—synchronization order. What is meaningless is to ask how many such orders there can be, given that they all result in the same observed outcome, i.e. they cannot be distinguished by definition.

> Now, the JMM doesn't define one; it simply adds that the relations produced
> by it, must be consistent with (intra-thread) program order; which in the
> sample trivial program is no restriction at all, since each thread contains
> a single SA.
>
> The only logical binary operator "implementation" I can think of is:
> timestamp of action.
> So, my interpretation of synchronization order has been, every possible
> legal execution's SAs are ordered by "timestamp of action", with the
> unsolved question being:
> does the JMM allow an execution to have a pair of SA's with the same
> timestamp?
>
> Is that thinking too close to the "physical layer"?  Maybe; it only requires
> that each SA have a timestamp associated with it, and those timestamps be
> comparable in the common-sense way

There is no such thing as a common-sense timestamp for these operations. And for timestamps to not be comparable due to special relativity the two devices do not actually have to be in motion relative to each other, the only thing that matters is that the observed order of events is not invariant under Lorentz transformations (i.e. different external observers could see conflicting sequences depending on their movement relative to the devices).

If you write timestamps from the CPU cores into memory, you’re adding the synchronization steps needed to collapse those multiple undistinguishable histories into distinct ones.

Coming back to your initial question: I don’t think it matters whether synchronization order is described in strict or non-strict form, as one gives rise to the other.

Regards,

Roland

>
>
>
>
>
>
>
>
>
> --
> View this message in context: http://jsr166-concurrency.10961.n7.nabble.com/Is-Synchronization-Order-A-Strict-Total-Order-tp13457p13471.html
> Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
> _______________________________________________
> Concurrency-interest mailing list
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest

--
Simplicity and elegance are unpopular because they require hard work and discipline to achieve and education to be appreciated.
  -- Dijkstra

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

Re: Is Synchronization Order A *Strict* Total Order?

thurstonn
Nope, not meaningless: for every execution there is at least one total order that results in the observed outcome. That binary operator is defined for you—synchronization order. What is meaningless is to ask how many such orders there can be, given that they all result in the same observed outcome, i.e. they cannot be distinguished by definition.


OK, what's the "observed outcome" of the program?
x=1, y=1  ?
So then what's  the total order of that execution?
Total orders can be enumerated pairwise
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

thurstonn
In reply to this post by Scott Blum
Scott Blum wrote
I would posit that there is only a strict total order if you try to observe
it within the program.  If you add sufficient code to determine which
history actually happened, you will in effect force the instructions to be
generated to insist on a strict total ordering.  In the absence of that
extra code, it's meaningless to ask which happened first.

Imagine a hypothetical implementation where you have two threads running on
two processors each with their own data caches.  Each thread might either
write its x=1, y=1 to its local cache, or to main memory.  If they write to
local cache, there's no rules around when that needs to get pushed through
to main memory-- provided no one is doing a volatile read on those fields.
Without the volatile reads you're never forcing the system to reach an
absolutely "determined" state.

But I use all these terms loosely because there truly isn't a clear 1:1
mapping between JMM and hardware. The JMM is all about reads and writes and
visibility within a program; how and when things actually get written to
memory or cache or whatever is an implementation detail of a particular JVM
and machine.

TLDR: the JMM doesn't require a strict total ordering unless you try to
observe it.

Here's the issue, let's presume you're correct.
Where does it stipulate that in  JLS$17?

I read the JMM very simply:
There's an (legal) execution.
Does the execution contain SA's?  Yes, 2 of them
Then there is a total order among those SA's. Period. Categorical

As I wrote in the OP, I agree that it's reasonable to ask:
who cares?  how can one tell the difference (i.e. one would have to "observe" the total order, which requires reads, which changes the program)?


Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Justin Sampson
Your program has no reads in it, so the Java Memory Model doesn't constrain the implementation in any way whatsoever:

"A memory model describes, given a program and an execution trace of that program, whether the execution trace is a legal execution of the program. The Java programming language memory model works by examining each read in an execution trace and checking that the write observed by that read is valid according to certain rules.

"The memory model describes possible behaviors of a program. An implementation is free to produce any code it likes, as long as all resulting executions of a program produce a result that can be predicted by the memory model.

"This provides a great deal of freedom for the implementor to perform a myriad of code transformations, including the reordering of actions and removal of unnecessary synchronization."

https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4

Cheers,
Justin


-----Original Message-----
From: Concurrency-interest [mailto:[hidden email]] On Behalf Of thurstonn
Sent: Tuesday, May 31, 2016 1:57 PM
To: [hidden email]
Subject: Re: [concurrency-interest] Is Synchronization Order A *Strict* Total Order?

Scott Blum wrote

> I would posit that there is only a strict total order if you try to
> observe
> it within the program.  If you add sufficient code to determine which
> history actually happened, you will in effect force the instructions to be
> generated to insist on a strict total ordering.  In the absence of that
> extra code, it's meaningless to ask which happened first.
>
> Imagine a hypothetical implementation where you have two threads running
> on
> two processors each with their own data caches.  Each thread might either
> write its x=1, y=1 to its local cache, or to main memory.  If they write
> to
> local cache, there's no rules around when that needs to get pushed through
> to main memory-- provided no one is doing a volatile read on those fields.
> Without the volatile reads you're never forcing the system to reach an
> absolutely "determined" state.
>
> But I use all these terms loosely because there truly isn't a clear 1:1
> mapping between JMM and hardware. The JMM is all about reads and writes
> and
> visibility within a program; how and when things actually get written to
> memory or cache or whatever is an implementation detail of a particular
> JVM
> and machine.
>
> TLDR: the JMM doesn't require a strict total ordering unless you try to
> observe it.


Here's the issue, let's presume you're correct.
Where does it stipulate that in  JLS$17?

I read the JMM very simply:
There's an (legal) execution.
Does the execution contain SA's?  Yes, 2 of them
Then there is a total order among those SA's. Period. Categorical

As I wrote in the OP, I agree that it's reasonable to ask:
who cares?  how can one tell the difference (i.e. one would have to
"observe" the total order, which requires reads, which changes the program)?






--
View this message in context: http://jsr166-concurrency.10961.n7.nabble.com/Is-Synchronization-Order-A-Strict-Total-Order-tp13457p13474.html
Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Scott Blum
In reply to this post by thurstonn
I think you're reading too much into it.  JLS 17 doesn't say there's one particular execution or even one particular total order.  In fact it implies the opposite: there may be a lot of executions and a lot of possible total orderings, but:

"If a program has no data races, then all executions of the program will appear to be sequentially consistent."

In a loosely defined program such as your example, there is more than one sequentially consistent total ordering of events.



On Tue, May 31, 2016 at 4:57 PM, thurstonn <[hidden email]> wrote:
Scott Blum wrote
> I would posit that there is only a strict total order if you try to
> observe
> it within the program.  If you add sufficient code to determine which
> history actually happened, you will in effect force the instructions to be
> generated to insist on a strict total ordering.  In the absence of that
> extra code, it's meaningless to ask which happened first.
>
> Imagine a hypothetical implementation where you have two threads running
> on
> two processors each with their own data caches.  Each thread might either
> write its x=1, y=1 to its local cache, or to main memory.  If they write
> to
> local cache, there's no rules around when that needs to get pushed through
> to main memory-- provided no one is doing a volatile read on those fields.
> Without the volatile reads you're never forcing the system to reach an
> absolutely "determined" state.
>
> But I use all these terms loosely because there truly isn't a clear 1:1
> mapping between JMM and hardware. The JMM is all about reads and writes
> and
> visibility within a program; how and when things actually get written to
> memory or cache or whatever is an implementation detail of a particular
> JVM
> and machine.
>
> TLDR: the JMM doesn't require a strict total ordering unless you try to
> observe it.


Here's the issue, let's presume you're correct.
Where does it stipulate that in  JLS$17?

I read the JMM very simply:
There's an (legal) execution.
Does the execution contain SA's?  Yes, 2 of them
Then there is a total order among those SA's. Period. Categorical

As I wrote in the OP, I agree that it's reasonable to ask:
who cares?  how can one tell the difference (i.e. one would have to
"observe" the total order, which requires reads, which changes the program)?






--
View this message in context: http://jsr166-concurrency.10961.n7.nabble.com/Is-Synchronization-Order-A-Strict-Total-Order-tp13457p13474.html
Sent from the JSR166 Concurrency mailing list archive at Nabble.com.
_______________________________________________
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
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Aleksey Shipilev-2
In reply to this post by thurstonn
On 05/31/2016 11:35 PM, thurstonn wrote:

> Nope, not meaningless: for every execution there is at least one total order
> that results in the observed outcome. That binary operator is defined for
> you—synchronization order. What is meaningless is to ask how many such
> orders there can be, given that they all result in the same observed
> outcome, i.e. they cannot be distinguished by definition.
>
>
> OK, what's the "observed outcome" of the program?
> x=1, y=1  ?
> So then what's  the total order of that execution?
Follow-up question: "If a tree falls in a forest and no one is around to
hear it, does it make a sound?"

But really, you can observe the finished state is (x = 1, y = 1). Is it
relevant which order had produced it? You can justify this outcome with
either juxtaposition, and so cannot distinguish which one "really
happened". The model does not concern itself with what "really happens",
it only cares that outcomes are governed by some abstract rules (that
is, "as if" there was a total order indeed).

Thanks,
-Aleksey


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

signature.asc (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

thurstonn
In reply to this post by Justin Sampson

"17.4.4. Synchronization Order

Every execution has a synchronization order. A synchronization order is a total order over all of the synchronization actions of an execution. For each thread t, the synchronization order of the synchronization actions (§17.4.2) in t is consistent with the program order (§17.4.3) of t. "

Every execution (a program without reads falls within "every")
Free to do whatever it wants? yes, as long as there is a total order over the set of synchronization actions.
My English is pretty good
Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

thurstonn
In reply to this post by Aleksey Shipilev-2
Aleksey Shipilev-2 wrote
On 05/31/2016 11:35 PM, thurstonn wrote:
> Nope, not meaningless: for every execution there is at least one total order
> that results in the observed outcome. That binary operator is defined for
> you—synchronization order. What is meaningless is to ask how many such
> orders there can be, given that they all result in the same observed
> outcome, i.e. they cannot be distinguished by definition.
>
>
> OK, what's the "observed outcome" of the program?
> x=1, y=1  ?
> So then what's  the total order of that execution?

Follow-up question: "If a tree falls in a forest and no one is around to
hear it, does it make a sound?"

But really, you can observe the finished state is (x = 1, y = 1). Is it
relevant which order had produced it? You can justify this outcome with
either juxtaposition, and so cannot distinguish which one "really
happened". The model does not concern itself with what "really happens",
it only cares that outcomes are governed by some abstract rules (that
is, "as if" there was a total order indeed).

Thanks,
-Aleksey


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


signature.asc (853 bytes) <http://jsr166-concurrency.10961.n7.nabble.com/attachment/13477/0/signature.asc>
Those are perfectly fair questions and I essentially raised them in the OP if you look back.
For such a trivial program, I agree it's not an issue; it just seems very difficult to "prove" to myself at least that it doesn't present some issue in some hypothetical "concurrency puzzler" program that I inadvertently write.




Reply | Threaded
Open this post in threaded view
|

Re: Is Synchronization Order A *Strict* Total Order?

Aleksey Shipilev-2
In reply to this post by thurstonn
On 05/31/2016 10:37 PM, thurstonn wrote:

> Aleksey Shipilev-2 wrote
>>
>> I am probably forgetting a significant part of my training, but these
>> are the definitions that are consistent with my own memory:
>>
>> (Weak) total order implies that for all A, B, C in set:
>>  a) Reflexive:     (A op A)
>>  b) Antisymmetric: (A op B) and (B op A) => (A = B)
>>  c) Transitive:    (A op B) and (B op C) => (A op C)
>>  d) Totality:      (A op B) or (B op A)
>>
>> Strict total order implies that for all A, B, C in set:
>>  a) Irreflexive:   !(A op A)
>>  b) Asymmetric:    (A op B) => !(B op A)
>>  c) Transitive:    (A op B) and (B op C) => (A op C)
>>  d) Trichotomy:    Exactly one of (A op B), (B op A), (A = B) is true
>>
>> Notice (A = B) reads as "A and B are the *same*", not "simultaneous".
>
> Ah, I think that last statement might be the rub; my understanding is that A
> = B does not mean A and B are the *same*, the irreflexive rule deals with
> that
> "=" is defined by the total order.
Set X is totally ordered under "op" binary relation if conditions above
are met. Equality is not defined by that binary relation (no less
because equality requires symmetry, which is at odds with a/antisymmetry
you already have), it should be defined separately.


> let's replace total order with "binary operator" (subject to the
> rules you've enumerated), and let's dispense with (ir)reflexivity, as
> I agree it's completely unnecessary to speak of ordering a SA with
> respect to itself.
> "=" is analogous to equals() vis a vis Java identity (==) (at least
> as I understand it)

I see that you are inventing the definitions that were not used to
define JMM. On these grounds alone the rest of the derivation that tries
to analyze if "SO is (strict) total order" is rather suspicious.


> Say I have a set of laptops {Laptop-A, Laptop-B}, 2 physically
> distinct laptops. It is meaningless to speak of a total order over
> that set. I have to define a binary operator, right?
>
> Say, weight-of-laptop. In such a case, I can say weight-of-laptop is
>  a total order over {Laptop-A, Laptop-B}; it's not difficult to
> interpret "=" in that case.

It is actually difficult to interpret, because it allows for at least
two interpretations:
  a) "equal by name";
  b) "equal by weight";

Once you have chosen one, you have to run with it.

> Now my understanding is that weight-of-laptop is *not* a strict total
> order over say {Laptop-A 1.1kg, Laptop-B 1.1kg} Because in order to
> be a total order, either Laptop-A :wol: Laptop-B => "<" or Laptop-B
> :wol: Laptop-A => "<".

I don't understand the semantics of "weight-of-laptop" relation. What
does it mean Laptop-A weight-of-laptop Laptop-B?! Let's instead define
"is-heavier-than" relation, which has meaning in Laptop-A
is-heavier-than Laptop-B, comparing weights.

With "equal by weight" definition of equality, "is-heavier-than" defines
a *strict* total order over the set of laptops: it is irreflexive,
asymmetric, transitive, and trichotomous.

Note that it is not a *weak* total order: it lacks totality,
demonstrated by (Laptop-A is-heavier-than Laptop-B) and (Laptop-B
is-heavier-than Laptop-A) = false. The saving grace for this binary
relation is that equality by weight allows the escape hatch in third
case (A = B) in trichotomy.

With "equal by name" definition of equality, "is-heavier-than" is not
even a _strict_ total order anymore, because it could not satisfy the
trichotomy property. So it loses all opportunities to be total.

Doing the same for "is-heavier-than-or-equal-weight" relation is left as
an exercise for the reader :) Hint: you will run into problems with
reflexivity and antisymmetry under "equal by name" there.

So, choose: either you want a consistent equality and total order, or
auxiliary equality and the deconstructed total order.


> Similarly, let's define an execution as a set of actions. e.g.
> {A(x=1), B(y=1)}. What's a total order over it? Meaningless right,
> i.e. I have to define a binary operator. Now, the JMM doesn't define
> one; it simply adds that the relations produced by it, must be
> consistent with (intra-thread) program order; which in the sample
> trivial program is no restriction at all, since each thread contains
> a single SA.

The definition of total order means there exists a binary relation that
satisfy the requirements...


> The only logical binary operator "implementation" I can think of is:
> timestamp of action. So, my interpretation of synchronization order
> has been, every possible legal execution's SAs are ordered by
> "timestamp of action", with the unsolved question being: does the JMM
> allow an execution to have a pair of SA's with the same timestamp?

...and the fact that JMM does not advertise the exact relation used to
produce the total order does not allow you to pull a cozy one out of
thin air. You have to prove that whatever candidate relation you
invented satisfies the original "SO is total order" definition. Can you
do that for timestamps?

I don't think you can, pretty much by the reasons explained in the
laptop example above. The SA equality has a trivial property: distinct
actions are not equal -- this is roughly similar to "equals by name" in
the laptop example. If you allow two SAs to have equal timestamps, then
it derails the SO totality under whatever binary relation over timestamps.


> Is that thinking too close to the "physical layer"?  Maybe; it only requires
> that each SA have a timestamp associated with it, and those timestamps be
> comparable in the common-sense way

This is why we have formal logic, so that we can keep "common sense"
"physical" intuitions from running afoul, producing garbage interpretations.

Cheers,
-Aleksey


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

signature.asc (853 bytes) Download Attachment
123