Happen before relationship in Java Memory Model

Question

I have a question about Java Memory Model.

In the following scenario: initial: a = 0; b = 0;

T1:
    a = 1;
    l.lock();
    b = 1;
    l.unlock();

T2:
    l.lock();
    read b;
    l.unlock();
    read a;

Can I say if the value of b read by T2 is 1, then the value of a read by T2 must be 1?

To my understanding, the unlock in T1 flushes both the value of a and b to main memory, and the lock in T2 makes sure both read a and read b can get the latest value.

Am I right?

Edit: I just specified that they are locked on the same lock.

Answer 1

Can I say if the value of b read by T2 is 1, then the value of a read by T2 must be 1?

Yes. It's guaranteed. An operation can move into a synchronized block, but not out from it. See Jeremy Mansons blog post Roach Motels and The Java Memory Model.

This means that, while read a can move up before unlock, (and up above read b due to instruction reordering) it can never move up above the lock instruction of T2.

Same reasoning applies for a = 1: It can move down into the synchronized block (and below b = 1 due to instruction reordering) but not passed the unlock instruction.

However, if we swap the instructions like that, they are both covered by the lock, which means that if T2 reads a 1 from b, then T1 will already have written a 1 to b.