Re: is HB consistent with SO for not otherwise related synchronization actions?

Hi Peter,

> The question is if wx,wy are synchronization actions.
> Your example is open for multiple interpretations.

Yes, wx and wy are synchronization actions. I did not specify what they are
exactly on purpose, to make the statement as general as possible.

Thank you,
Valentin www.kovalenko.link


On Wed, Feb 3, 2021 at 12:39 AM Peter Veentjer <[email protected]>
wrote:

>
>
> On Wed, Feb 3, 2021 at 3:40 AM Valentin Kovalenko via Concurrency-interest
> <[email protected]> wrote:
>
>> I believe, I found how to formally prove this.
>>
>> Same thread.
>> If hb(wx, wy) and the actions wx, wy are performed by the same thread,
>> then we have so(wx, wy) trivially due to both so and hb being consistent
>> with the program order (po).
>>
>
> Correct.
>
> If wx,wy are synchronization actions, then they are part of both so and po.
>
>>
>>
>> Different threads.
>> A more interesting situation is when wx and wy are performed by different
>> threads, let us label them X and Y respectively. The only way to have a
>> happens-before relation between actions performed by different threads X
>> and Y is to have a synchronizes-with relation between a pair of
>> synchronization actions in these threads.
>>
>
> Correct
>
>>
>> In other words, given hb(wx, wy), the execution must have actions
>> releaseX performed by X and acquireY performed by Y, such that
>> synchronizes-with(releaseX, acquireY) and po(wx, releaseX), po(acquireY,
>> wy).
>>
>
> Your example is open for multiple interpretations. So I'll make it
> concrete and hope it reflects what you have in mind.
>
> int a;
> volatile int b;
>
> thread1(){
>   a=1;
>   b=1;
> }
>
> thread(){
>   int rb=b;
>   int ra=a;
>   if(rb==1 && ra==0) println("violation");
> }
>
> And let's assume we see rb==1; what can we tell about a.
>
> So we have the following:
> po(a=1,b=1)
> so(b=1,rb=b)
> po(rb=b, ra=a)
>
> So we have a hb(a=1,ra=a)=po(a=1,b=1), so(b=1,rb=b),po(rb=b, ra=a)
>
> So we are good because the read of a should see the write of a and hence
> "violation" can't be printed.
>
>
>> Now we can see that hb(wx, wy) necessary leads to so(wx, releaseX),
>> sw(releaseX, acquireY), so(acquireY, wy); and sw(releaseX, acquireY)
>> necessary means so(releaseX, acquireY).
>>
>
> I'm not sure what wx,wy for actions are. If they are regular loads/stores
> then they are not part of the so because they are not synchronization
> actions.
>
>
>
>> Therefore, hb(wx, wy) necessary leads to so(wx, releaseX), so(releaseX,
>> acquireY), so(acquireY, wy), which gives so(wx, wy).
>>
>
> The question is if wx,wy are synchronization actions. If they are not,
> then they are not part of so.  So in my example the so doesn't order
> (a=1,b=1) and it doesn't order (rb=b, ra=a)
>
> If a and b would both be volatile and hence become synchronization
> actions, then the so would contain
>
> (a=1,b=1),(b=1,rb=b),(rb=b,ra=a)
>
>
>>
>> I would highly appreciate it if someone could confirm this reasoning.
>>
>
> The definition of the so is that it is a total order over all
> synchronization actions that is consistent with the po of each of the
> threads.
>
> So in case of the universes; it would filter out any universes that
> - doesn't have a total order over all synchronization actions
> - the total order of the synchronization actions isn't consistent with the
> po of each of the threads.
>
> Based on the so you can determine the sw order since it is a sub order of
> so.
>
> And based on the po and the sw, you can determine the hb order, i.e. the
> transitive closure of the union of the po and the sw.
>
>
>>
>> Regards,
>> Valentin www.kovalenko.link
>>
>>
>> On Tue, Feb 2, 2021 at 5:53 PM Valentin Kovalenko <
>> [email protected]> wrote:
>>
>>> Hi all,
>>>
>>> Imagine that we have only partial information about an execution (as is
>>> almost always true in practice):
>>> there are synchronization actions wx and wy such that happens-before(wx,
>>> wy). These actions are not otherwise explicitly related, we may think of
>>> them as being volatile writes to two different variables x and y.
>>>
>>> According to JMM, they are also ordered with the total synchronization
>>> order. The order so(wx, wy) is a possibility that clearly does not violate
>>> any JMM constraints. Interestingly, so(wy, wx) also does not seem to
>>> violate anything, and, thus, should also be allowed.
>>>
>>> However, if I try to imagine a program that produces executions with
>>> hb(wx, wy) and so(wy, wx) - I fail miserably. Whatever I imagine is needed
>>> to have hb(wx, wy) in an execution, causes this execution to have so(wx,
>>> wy).
>>>
>>> So maybe happens-before order is always consistent with the
>>> synchronization order (if this is not the case, could someone come up with
>>> a counterexample)? If this is the case, is there a way to formally deduce
>>> it from JMM without resorting to the argument "I can't imagine a program
>>> that produces executions with hb not being consistent with so"?
>>>
>>> Thank you,
>>> Valentin www.kovalenko.link
>>>
>> _______________________________________________
>> Concurrency-interest mailing list
>> [email protected]
>> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>>
>

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