Linearizability of synchronization actions

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

Linearizability of synchronization actions

JSR166 Concurrency mailing list
The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
1) T1 q.enq(x)
2) T2 q.enq(y)
3) T3 q.deq(y)

This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.

Any ideas on that?

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

Re: Linearizability of synchronization actions

JSR166 Concurrency mailing list
Time is an illusion.

Alex

> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>
> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
> 1) T1 q.enq(x)
> 2) T2 q.enq(y)
> 3) T3 q.deq(y)
>
> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>
> Any ideas on that?
>
> Andrey
> _______________________________________________
> 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: Linearizability of synchronization actions

JSR166 Concurrency mailing list
On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.

There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)

Alex

> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>
> Time is an illusion.
>
> Alex
>
>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>
>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>> 1) T1 q.enq(x)
>> 2) T2 q.enq(y)
>> 3) T3 q.deq(y)
>>
>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>
>> Any ideas on that?
>>
>> Andrey
>> _______________________________________________
>> 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: Linearizability of synchronization actions

JSR166 Concurrency mailing list
If there is no global time, does it make sense to talk about linearizability?
For humans time is mostly about causality.
What if we enrich my previous example with external actions (socket read/write) like this:
T1
q.enq(x)
writeToSocket1()

T2
readFromSocket2()
q.enq(y)
q.deq(y)

And there is an external actor, that receives message from socket1 as soon as enqueuing in the first thread is done and immediately writes to socket2 to unblock thread T2.
What in JMM prohibits such execution?

> On 28 Sep 2018, at 17:53, Alex Otenko <[hidden email]> wrote:
>
> On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.
>
> There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)
>
> Alex
>
>> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>>
>> Time is an illusion.
>>
>> Alex
>>
>>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>>
>>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>>> 1) T1 q.enq(x)
>>> 2) T2 q.enq(y)
>>> 3) T3 q.deq(y)
>>>
>>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>>
>>> Any ideas on that?
>>>
>>> Andrey
>>> _______________________________________________
>>> 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: Linearizability of synchronization actions

JSR166 Concurrency mailing list

> On 28 Sep 2018, at 17:41, Andrew Ershov <[hidden email]> wrote:
>
> If there is no global time, does it make sense to talk about linearizability?

Yes. By defining a total order of synchronization events which all the threads agree on.

Global time is more than that. Global time is about agreeing on the time elapsed between any two events in such an order. But this is not a necessary condition for linearizability.

> For humans time is mostly about causality.

Happens-before captures that.

> What if we enrich my previous example with external actions (socket read/write) like this:
> T1
> q.enq(x)
> writeToSocket1()
>
> T2
> readFromSocket2()
> q.enq(y)
> q.deq(y)
>
> And there is an external actor, that receives message from socket1 as soon as enqueuing in the first thread is done and immediately writes to socket2 to unblock thread T2.
> What in JMM prohibits such execution?

For JMM to prohibit such execution, you need a synchronizes-with edge that from which absurd follows.


Alex


>> On 28 Sep 2018, at 17:53, Alex Otenko <[hidden email]> wrote:
>>
>> On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.
>>
>> There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)
>>
>> Alex
>>
>>> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>>>
>>> Time is an illusion.
>>>
>>> Alex
>>>
>>>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>>>
>>>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>>>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>>>> 1) T1 q.enq(x)
>>>> 2) T2 q.enq(y)
>>>> 3) T3 q.deq(y)
>>>>
>>>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>>>
>>>> Any ideas on that?
>>>>
>>>> Andrey
>>>> _______________________________________________
>>>> 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: Linearizability of synchronization actions

JSR166 Concurrency mailing list

Thanks for your reply.
Regarding your third answer: do you mean synchronizes-with edge between writeToSocket and readFromSocket? I don’t see in the spec, that external actions could form synchronizes-with edge.

> On 28 Sep 2018, at 19:17, Alex Otenko <[hidden email]> wrote:
>
>
>> On 28 Sep 2018, at 17:41, Andrew Ershov <[hidden email]> wrote:
>>
>> If there is no global time, does it make sense to talk about linearizability?
>
> Yes. By defining a total order of synchronization events which all the threads agree on.
>
> Global time is more than that. Global time is about agreeing on the time elapsed between any two events in such an order. But this is not a necessary condition for linearizability.
>
>> For humans time is mostly about causality.
>
> Happens-before captures that.
>
>> What if we enrich my previous example with external actions (socket read/write) like this:
>> T1
>> q.enq(x)
>> writeToSocket1()
>>
>> T2
>> readFromSocket2()
>> q.enq(y)
>> q.deq(y)
>>
>> And there is an external actor, that receives message from socket1 as soon as enqueuing in the first thread is done and immediately writes to socket2 to unblock thread T2.
>> What in JMM prohibits such execution?
>
> For JMM to prohibit such execution, you need a synchronizes-with edge that from which absurd follows.
>
>
> Alex
>
>
>>> On 28 Sep 2018, at 17:53, Alex Otenko <[hidden email]> wrote:
>>>
>>> On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.
>>>
>>> There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)
>>>
>>> Alex
>>>
>>>> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>>>>
>>>> Time is an illusion.
>>>>
>>>> Alex
>>>>
>>>>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>>>>
>>>>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>>>>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>>>>> 1) T1 q.enq(x)
>>>>> 2) T2 q.enq(y)
>>>>> 3) T3 q.deq(y)
>>>>>
>>>>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>>>>
>>>>> Any ideas on that?
>>>>>
>>>>> Andrey
>>>>> _______________________________________________
>>>>> 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: Linearizability of synchronization actions

JSR166 Concurrency mailing list
In reply to this post by JSR166 Concurrency mailing list
Andrey,

>JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.

As Alex mentioned, there is no concept of physical global time and what is considered as "time" in the definition of linearizability (see https://www.ics.forth.gr/tech-reports/2013/2013.TR439_Survey_on_Consistency_Conditions.pdf or the original https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf) is just a partial order of actions (I hate this terrible choice to use word "time"). Our "time"-order is the happens-before order.

Regards,
Valentin
LinkedIn   GitHub   YouTube


On Fri, 28 Sep 2018 at 10:25, <[hidden email]> wrote:
Send Concurrency-interest mailing list submissions to
        [hidden email]

To subscribe or unsubscribe via the World Wide Web, visit
        http://cs.oswego.edu/mailman/listinfo/concurrency-interest
or, via email, send a message with subject or body 'help' to
        [hidden email]

You can reach the person managing the list at
        [hidden email]

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Concurrency-interest digest..."


Today's Topics:

   1. Re: Linearizability of synchronization    actions (Alex Otenko)
   2. Re: Linearizability of synchronization    actions (Alex Otenko)


----------------------------------------------------------------------

Message: 1
Date: Fri, 28 Sep 2018 16:47:12 +0100
From: Alex Otenko <[hidden email]>
To: Andrew Ershov <[hidden email]>
Cc: [hidden email]
Subject: Re: [concurrency-interest] Linearizability of synchronization
        actions
Message-ID: <[hidden email]>
Content-Type: text/plain;       charset=utf-8

Time is an illusion.

Alex

> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>
> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
> 1) T1 q.enq(x)
> 2) T2 q.enq(y)
> 3) T3 q.deq(y)
>
> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>
> Any ideas on that?
>
> Andrey
> _______________________________________________
> Concurrency-interest mailing list
> [hidden email]
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest



------------------------------

Message: 2
Date: Fri, 28 Sep 2018 16:53:10 +0100
From: Alex Otenko <[hidden email]>
To: Andrew Ershov <[hidden email]>
Cc: [hidden email]
Subject: Re: [concurrency-interest] Linearizability of synchronization
        actions
Message-ID: <[hidden email]>
Content-Type: text/plain;       charset=utf-8

On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.

There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)

Alex

> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>
> Time is an illusion.
>
> Alex
>
>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>
>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>> 1) T1 q.enq(x)
>> 2) T2 q.enq(y)
>> 3) T3 q.deq(y)
>>
>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>
>> Any ideas on that?
>>
>> Andrey
>> _______________________________________________
>> Concurrency-interest mailing list
>> [hidden email]
>> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>



------------------------------

Subject: Digest Footer

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


------------------------------

End of Concurrency-interest Digest, Vol 163, Issue 25
*****************************************************

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

Re: Linearizability of synchronization actions

JSR166 Concurrency mailing list
In reply to this post by JSR166 Concurrency mailing list
I am not sure what you are getting at. You asked about JMM. JMM needs a synchronizes-with edge that makes the sequence you are enquiring about absurd. If there is no such edge, then JMM doesn’t forbid it.

It doesn’t mean it’s possible. It only means it is not JMM that can make it impossible.

Alex

> On 28 Sep 2018, at 18:26, Andrew Ershov <[hidden email]> wrote:
>
>
> Thanks for your reply.
> Regarding your third answer: do you mean synchronizes-with edge between writeToSocket and readFromSocket? I don’t see in the spec, that external actions could form synchronizes-with edge.
>
>> On 28 Sep 2018, at 19:17, Alex Otenko <[hidden email]> wrote:
>>
>>
>>> On 28 Sep 2018, at 17:41, Andrew Ershov <[hidden email]> wrote:
>>>
>>> If there is no global time, does it make sense to talk about linearizability?
>>
>> Yes. By defining a total order of synchronization events which all the threads agree on.
>>
>> Global time is more than that. Global time is about agreeing on the time elapsed between any two events in such an order. But this is not a necessary condition for linearizability.
>>
>>> For humans time is mostly about causality.
>>
>> Happens-before captures that.
>>
>>> What if we enrich my previous example with external actions (socket read/write) like this:
>>> T1
>>> q.enq(x)
>>> writeToSocket1()
>>>
>>> T2
>>> readFromSocket2()
>>> q.enq(y)
>>> q.deq(y)
>>>
>>> And there is an external actor, that receives message from socket1 as soon as enqueuing in the first thread is done and immediately writes to socket2 to unblock thread T2.
>>> What in JMM prohibits such execution?
>>
>> For JMM to prohibit such execution, you need a synchronizes-with edge that from which absurd follows.
>>
>>
>> Alex
>>
>>
>>>> On 28 Sep 2018, at 17:53, Alex Otenko <[hidden email]> wrote:
>>>>
>>>> On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.
>>>>
>>>> There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)
>>>>
>>>> Alex
>>>>
>>>>> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>>>>>
>>>>> Time is an illusion.
>>>>>
>>>>> Alex
>>>>>
>>>>>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>>>>>
>>>>>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>>>>>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>>>>>> 1) T1 q.enq(x)
>>>>>> 2) T2 q.enq(y)
>>>>>> 3) T3 q.deq(y)
>>>>>>
>>>>>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>>>>>
>>>>>> Any ideas on that?
>>>>>>
>>>>>> Andrey
>>>>>> _______________________________________________
>>>>>> 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: Linearizability of synchronization actions

JSR166 Concurrency mailing list
In reply to this post by JSR166 Concurrency mailing list
To elaborate some more, JMM is not about the behaviour of processes separated by space (running on different CPU cores communicating using physical connections limited by the speed of light), or time (running on a single CPU with preemptive multitasking). JMM is about the behaviour of processes subject to optimizations. Java program then is only a model of computation.

Measuring time delta then becomes an impossible task. If you place any sort of beacon taking the wall clock reading at two points in the Java program, what is the optimizer meant to do? Keep all the computations appearing between them in program order strictly between them at run time? What makes the time measurement so special?

But then what’s the meaning of “socket write appears after q.enq(x)”? Appears to whom? Java language spec only requires that it should appear so to T1. It doesn’t mean T1 measures time to observe that is so. It only means that the side effects of q.enq and socket write are observable by T1 as if appearing in that order. That’s the meaning of program order: things appearing in the program before the socket write cannot see side effects of the socket write.

T2 reading from socket is not bound by that constraint. So even an existence of an obvious constraint (but out-of-bounds as far as JMM is concerned) that the read of the socket cannot see the write “before” the write to the socket happens, it is not sufficient to agree that q.enq also happened before that read. If you were to demonstrate that within JMM, you would need a synchronizes-with edge joining the program orders of the two threads.



Also, linearizability is not meant to be in opposition to sequential consistency. Linearizable FIFO queue is (I think! I am not too strong on theory here) sequentially consistent, too - that is, any execution corresponds to some possible sequential ordering of enq and deq.

Linearizability is meant to describe a property of composable computations, unlike sequential consistency. If you look at the coarse grained events, you may agree the queue is sequentially consistent; but when you look into the finer grained events, you may not see sequential consistency there - CAS failing does not correspond to any possible sequential execution of enq and deq. Converse is also true: if you see the building blocks behave sequentially consistently (ok, CAS failing does correspond to a possible sequential execution of the lock acquire attempts), you will not necessarily see the whole behave sequentially consistently.

But linearizability is composable: if the building blocks are linearizable, then the whole is linearizable, too. It is not a substitute of sequential consistency. It is just a different correctness guarantee.


Alex

> On 28 Sep 2018, at 18:26, Andrew Ershov <[hidden email]> wrote:
>
>
> Thanks for your reply.
> Regarding your third answer: do you mean synchronizes-with edge between writeToSocket and readFromSocket? I don’t see in the spec, that external actions could form synchronizes-with edge.
>
>> On 28 Sep 2018, at 19:17, Alex Otenko <[hidden email]> wrote:
>>
>>
>>> On 28 Sep 2018, at 17:41, Andrew Ershov <[hidden email]> wrote:
>>>
>>> If there is no global time, does it make sense to talk about linearizability?
>>
>> Yes. By defining a total order of synchronization events which all the threads agree on.
>>
>> Global time is more than that. Global time is about agreeing on the time elapsed between any two events in such an order. But this is not a necessary condition for linearizability.
>>
>>> For humans time is mostly about causality.
>>
>> Happens-before captures that.
>>
>>> What if we enrich my previous example with external actions (socket read/write) like this:
>>> T1
>>> q.enq(x)
>>> writeToSocket1()
>>>
>>> T2
>>> readFromSocket2()
>>> q.enq(y)
>>> q.deq(y)
>>>
>>> And there is an external actor, that receives message from socket1 as soon as enqueuing in the first thread is done and immediately writes to socket2 to unblock thread T2.
>>> What in JMM prohibits such execution?
>>
>> For JMM to prohibit such execution, you need a synchronizes-with edge that from which absurd follows.
>>
>>
>> Alex
>>
>>
>>>> On 28 Sep 2018, at 17:53, Alex Otenko <[hidden email]> wrote:
>>>>
>>>> On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.
>>>>
>>>> There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)
>>>>
>>>> Alex
>>>>
>>>>> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>>>>>
>>>>> Time is an illusion.
>>>>>
>>>>> Alex
>>>>>
>>>>>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>>>>>
>>>>>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>>>>>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>>>>>> 1) T1 q.enq(x)
>>>>>> 2) T2 q.enq(y)
>>>>>> 3) T3 q.deq(y)
>>>>>>
>>>>>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>>>>>
>>>>>> Any ideas on that?
>>>>>>
>>>>>> Andrey
>>>>>> _______________________________________________
>>>>>> 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: Linearizability of synchronization actions

JSR166 Concurrency mailing list
In reply to this post by JSR166 Concurrency mailing list
What you hint at here, is data flow program order.  That is, only the computations that a data item flow though are actually ordered relative to others.  Data flow is not really the way that many programmers consider anything they write in Java, since the programming language/environment is very much about linear statements (ordered by lines) and strictly sequential programming (loops, ifs, function calls) paradigms.  We’ve had this discussion before and I still think it’s not a good idea to really let the language and the JMM be so disconnected that you can have discussions about the JMM which discard language constructs as a form of execution order/control.

The reason why the lack of consistency is interesting is because it makes the hardware more effective when you hand it (or infer) details to allow better/parallel use of hardware resources.  However, the largest issue is that different hardware has very different requirements to be most effectively used.  And you are continuing to weaken the guarantees that the implementation used to “provide” by making “happens before” be the only guaranteed ordering that the “language” can provide, even though it’s the JMM that is implemented this way.  

In effect, the JMM is so weak in controllability by any language compiled to it, that allowing a language to have more strict linear/ordering execution guarantees than the JMM has, is extremely difficult.   So in the end, we only have the JMM.  It’s really no longer about a language compiling to the JMM being able to guarantee any observable execution beyond happens-before.

Thus the Java language is really not the consideration any more.  All we should discuss is the JMM and just stop confusion.  

Gregg

> On Oct 1, 2018, at 3:12 AM, Alex Otenko via Concurrency-interest <[hidden email]> wrote:
>
> To elaborate some more, JMM is not about the behaviour of processes separated by space (running on different CPU cores communicating using physical connections limited by the speed of light), or time (running on a single CPU with preemptive multitasking). JMM is about the behaviour of processes subject to optimizations. Java program then is only a model of computation.
>
> Measuring time delta then becomes an impossible task. If you place any sort of beacon taking the wall clock reading at two points in the Java program, what is the optimizer meant to do? Keep all the computations appearing between them in program order strictly between them at run time? What makes the time measurement so special?
>
> But then what’s the meaning of “socket write appears after q.enq(x)”? Appears to whom? Java language spec only requires that it should appear so to T1. It doesn’t mean T1 measures time to observe that is so. It only means that the side effects of q.enq and socket write are observable by T1 as if appearing in that order. That’s the meaning of program order: things appearing in the program before the socket write cannot see side effects of the socket write.
>
> T2 reading from socket is not bound by that constraint. So even an existence of an obvious constraint (but out-of-bounds as far as JMM is concerned) that the read of the socket cannot see the write “before” the write to the socket happens, it is not sufficient to agree that q.enq also happened before that read. If you were to demonstrate that within JMM, you would need a synchronizes-with edge joining the program orders of the two threads.
>
>
>
> Also, linearizability is not meant to be in opposition to sequential consistency. Linearizable FIFO queue is (I think! I am not too strong on theory here) sequentially consistent, too - that is, any execution corresponds to some possible sequential ordering of enq and deq.
>
> Linearizability is meant to describe a property of composable computations, unlike sequential consistency. If you look at the coarse grained events, you may agree the queue is sequentially consistent; but when you look into the finer grained events, you may not see sequential consistency there - CAS failing does not correspond to any possible sequential execution of enq and deq. Converse is also true: if you see the building blocks behave sequentially consistently (ok, CAS failing does correspond to a possible sequential execution of the lock acquire attempts), you will not necessarily see the whole behave sequentially consistently.
>
> But linearizability is composable: if the building blocks are linearizable, then the whole is linearizable, too. It is not a substitute of sequential consistency. It is just a different correctness guarantee.
>
>
> Alex
>
>> On 28 Sep 2018, at 18:26, Andrew Ershov <[hidden email]> wrote:
>>
>>
>> Thanks for your reply.
>> Regarding your third answer: do you mean synchronizes-with edge between writeToSocket and readFromSocket? I don’t see in the spec, that external actions could form synchronizes-with edge.
>>
>>> On 28 Sep 2018, at 19:17, Alex Otenko <[hidden email]> wrote:
>>>
>>>
>>>> On 28 Sep 2018, at 17:41, Andrew Ershov <[hidden email]> wrote:
>>>>
>>>> If there is no global time, does it make sense to talk about linearizability?
>>>
>>> Yes. By defining a total order of synchronization events which all the threads agree on.
>>>
>>> Global time is more than that. Global time is about agreeing on the time elapsed between any two events in such an order. But this is not a necessary condition for linearizability.
>>>
>>>> For humans time is mostly about causality.
>>>
>>> Happens-before captures that.
>>>
>>>> What if we enrich my previous example with external actions (socket read/write) like this:
>>>> T1
>>>> q.enq(x)
>>>> writeToSocket1()
>>>>
>>>> T2
>>>> readFromSocket2()
>>>> q.enq(y)
>>>> q.deq(y)
>>>>
>>>> And there is an external actor, that receives message from socket1 as soon as enqueuing in the first thread is done and immediately writes to socket2 to unblock thread T2.
>>>> What in JMM prohibits such execution?
>>>
>>> For JMM to prohibit such execution, you need a synchronizes-with edge that from which absurd follows.
>>>
>>>
>>> Alex
>>>
>>>
>>>>> On 28 Sep 2018, at 17:53, Alex Otenko <[hidden email]> wrote:
>>>>>
>>>>> On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.
>>>>>
>>>>> There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)
>>>>>
>>>>> Alex
>>>>>
>>>>>> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>>>>>>
>>>>>> Time is an illusion.
>>>>>>
>>>>>> Alex
>>>>>>
>>>>>>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>>>>>>
>>>>>>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>>>>>>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>>>>>>> 1) T1 q.enq(x)
>>>>>>> 2) T2 q.enq(y)
>>>>>>> 3) T3 q.deq(y)
>>>>>>>
>>>>>>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>>>>>>
>>>>>>> Any ideas on that?
>>>>>>>
>>>>>>> Andrey
>>>>>>> _______________________________________________
>>>>>>> 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

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

Re: Linearizability of synchronization actions

JSR166 Concurrency mailing list
I am not sure I see what the problem is.

Single-threaded executions are unable to observe what the “real” execution order is through the means of the language. Multi-threaded executions don’t become more correct or substantially easier to reason about, if you make all accesses totally ordered. Race conditions are possible in Javascript just as well. Javascript can have concurrency unimaginable in Java, although its memory accesses are totally ordered, and its concurrency is cooperative.


Alex

> On 1 Oct 2018, at 18:54, Gregg Wonderly <[hidden email]> wrote:
>
> What you hint at here, is data flow program order.  That is, only the computations that a data item flow though are actually ordered relative to others.  Data flow is not really the way that many programmers consider anything they write in Java, since the programming language/environment is very much about linear statements (ordered by lines) and strictly sequential programming (loops, ifs, function calls) paradigms.  We’ve had this discussion before and I still think it’s not a good idea to really let the language and the JMM be so disconnected that you can have discussions about the JMM which discard language constructs as a form of execution order/control.
>
> The reason why the lack of consistency is interesting is because it makes the hardware more effective when you hand it (or infer) details to allow better/parallel use of hardware resources.  However, the largest issue is that different hardware has very different requirements to be most effectively used.  And you are continuing to weaken the guarantees that the implementation used to “provide” by making “happens before” be the only guaranteed ordering that the “language” can provide, even though it’s the JMM that is implemented this way.  
>
> In effect, the JMM is so weak in controllability by any language compiled to it, that allowing a language to have more strict linear/ordering execution guarantees than the JMM has, is extremely difficult.   So in the end, we only have the JMM.  It’s really no longer about a language compiling to the JMM being able to guarantee any observable execution beyond happens-before.
>
> Thus the Java language is really not the consideration any more.  All we should discuss is the JMM and just stop confusion.  
>
> Gregg
>
>> On Oct 1, 2018, at 3:12 AM, Alex Otenko via Concurrency-interest <[hidden email]> wrote:
>>
>> To elaborate some more, JMM is not about the behaviour of processes separated by space (running on different CPU cores communicating using physical connections limited by the speed of light), or time (running on a single CPU with preemptive multitasking). JMM is about the behaviour of processes subject to optimizations. Java program then is only a model of computation.
>>
>> Measuring time delta then becomes an impossible task. If you place any sort of beacon taking the wall clock reading at two points in the Java program, what is the optimizer meant to do? Keep all the computations appearing between them in program order strictly between them at run time? What makes the time measurement so special?
>>
>> But then what’s the meaning of “socket write appears after q.enq(x)”? Appears to whom? Java language spec only requires that it should appear so to T1. It doesn’t mean T1 measures time to observe that is so. It only means that the side effects of q.enq and socket write are observable by T1 as if appearing in that order. That’s the meaning of program order: things appearing in the program before the socket write cannot see side effects of the socket write.
>>
>> T2 reading from socket is not bound by that constraint. So even an existence of an obvious constraint (but out-of-bounds as far as JMM is concerned) that the read of the socket cannot see the write “before” the write to the socket happens, it is not sufficient to agree that q.enq also happened before that read. If you were to demonstrate that within JMM, you would need a synchronizes-with edge joining the program orders of the two threads.
>>
>>
>>
>> Also, linearizability is not meant to be in opposition to sequential consistency. Linearizable FIFO queue is (I think! I am not too strong on theory here) sequentially consistent, too - that is, any execution corresponds to some possible sequential ordering of enq and deq.
>>
>> Linearizability is meant to describe a property of composable computations, unlike sequential consistency. If you look at the coarse grained events, you may agree the queue is sequentially consistent; but when you look into the finer grained events, you may not see sequential consistency there - CAS failing does not correspond to any possible sequential execution of enq and deq. Converse is also true: if you see the building blocks behave sequentially consistently (ok, CAS failing does correspond to a possible sequential execution of the lock acquire attempts), you will not necessarily see the whole behave sequentially consistently.
>>
>> But linearizability is composable: if the building blocks are linearizable, then the whole is linearizable, too. It is not a substitute of sequential consistency. It is just a different correctness guarantee.
>>
>>
>> Alex
>>
>>> On 28 Sep 2018, at 18:26, Andrew Ershov <[hidden email]> wrote:
>>>
>>>
>>> Thanks for your reply.
>>> Regarding your third answer: do you mean synchronizes-with edge between writeToSocket and readFromSocket? I don’t see in the spec, that external actions could form synchronizes-with edge.
>>>
>>>> On 28 Sep 2018, at 19:17, Alex Otenko <[hidden email]> wrote:
>>>>
>>>>
>>>>> On 28 Sep 2018, at 17:41, Andrew Ershov <[hidden email]> wrote:
>>>>>
>>>>> If there is no global time, does it make sense to talk about linearizability?
>>>>
>>>> Yes. By defining a total order of synchronization events which all the threads agree on.
>>>>
>>>> Global time is more than that. Global time is about agreeing on the time elapsed between any two events in such an order. But this is not a necessary condition for linearizability.
>>>>
>>>>> For humans time is mostly about causality.
>>>>
>>>> Happens-before captures that.
>>>>
>>>>> What if we enrich my previous example with external actions (socket read/write) like this:
>>>>> T1
>>>>> q.enq(x)
>>>>> writeToSocket1()
>>>>>
>>>>> T2
>>>>> readFromSocket2()
>>>>> q.enq(y)
>>>>> q.deq(y)
>>>>>
>>>>> And there is an external actor, that receives message from socket1 as soon as enqueuing in the first thread is done and immediately writes to socket2 to unblock thread T2.
>>>>> What in JMM prohibits such execution?
>>>>
>>>> For JMM to prohibit such execution, you need a synchronizes-with edge that from which absurd follows.
>>>>
>>>>
>>>> Alex
>>>>
>>>>
>>>>>> On 28 Sep 2018, at 17:53, Alex Otenko <[hidden email]> wrote:
>>>>>>
>>>>>> On a serious note, there needs to be some clarity what time is meant in the definition of linearizability you are looking at.
>>>>>>
>>>>>> There is no physical global time line in the real world. The models may assume an even weaker notion of time. (Hence a reference to happens-before and total orders - that’s a way to get out of the “what is time?” conundrum and at the same time specify what it means that they are atomic, and that everyone agrees on the order. Such a definition also allows for weaker-than-real-world time.)
>>>>>>
>>>>>> Alex
>>>>>>
>>>>>>> On 28 Sep 2018, at 16:47, Alex Otenko <[hidden email]> wrote:
>>>>>>>
>>>>>>> Time is an illusion.
>>>>>>>
>>>>>>> Alex
>>>>>>>
>>>>>>>> On 28 Sep 2018, at 16:30, Andrew Ershov via Concurrency-interest <[hidden email]> wrote:
>>>>>>>>
>>>>>>>> The “Art of Multiprocessor programming” claims that “synchronization events are linearizable: they are totally ordered, and all threads agree on the ordering”. JMM also agrees that there is a total order of synchronization actions, but linearizability assumes also time ordering, JMM says nothing that synchronization actions order is consistent with time.
>>>>>>>> In other words, if there is a queue q (protected by lock) and two threads T1 and T1. In the time order (assuming no method invocations overlap):
>>>>>>>> 1) T1 q.enq(x)
>>>>>>>> 2) T2 q.enq(y)
>>>>>>>> 3) T3 q.deq(y)
>>>>>>>>
>>>>>>>> This execution is sequentially consistent, but it’s not linearizable. The total order of synchronization actions that allows this execution is 2 lock - 2 unlock - 3 lock - 3 unlock - 1 lock - 1 unlock. But it’s not consistent with time.
>>>>>>>>
>>>>>>>> Any ideas on that?
>>>>>>>>
>>>>>>>> Andrey
>>>>>>>> _______________________________________________
>>>>>>>> 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
>

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