Correctness of final array access under a race​​​​​​​

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

Correctness of final array access under a race​​​​​​​

Nikita Koval
 
Hi,

I am thinking about reading String under a race. String class has the array of chars field, which is final and is initialized during the construction. However, elements of this array "are not final" in terms of the memory model (but they effectively are). Therefore, I do not understand why reading the array of non-final chars cannot read the array of default char elements. I think I do not clearly understand the final's semantics. 

According to JLS 17.5.1, a new happens-before (which does not transitively close with other happens-before orderings) is introduced in the semantics of final fields. Could you please explain what "does not transitively close with other happens-before orderings" mean? On the other side, it looks like "freeze" action at the end of an object construction has a global effect and makes a happens-before order between writing the object to the memory after the construction and reading the object then. However, I am not sure I am right.

In addition, maybe there is any full axiomatic semantics of JMM. Could you please say if it exists.


Thank you for your help,
Nikita.

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

Re: Correctness of final array access under a race​​​​​​​

Aleksey Shipilev-3
On 08/30/2017 08:32 PM, Nikita Koval wrote:
> I am thinking about reading String under a race. String class has the array of chars field, which is
> final and is initialized during the construction. However, elements of this array "are not final" in
> terms of the memory model (but they effectively are). Therefore, I do not understand why reading the
> array of non-final chars cannot read the array of default char elements. I think I do not clearly
> understand the final's semantics.

I think it follows directly from the spec definition:

"Given a write $w, a freeze $f, an action $a (that is not a read of a final field), a read
$r1 of the final field frozen by $f, and a read $r2 such that hb($w, $f), hb($f, $a), mc($a, $r1),
and dereferences($r1, $r2), then when determining which values can be seen by $r2,
we consider hb($w, $r2)."

For example:

Thread 1:

  class C {
    final int[] arr;
    C() {
       arr = new int[1];
       arr[0] = 42; // $w
       {freeze}     // $f
    }
  }

  GLOBAL = new C;


Thread 2:

  C c = GLOBAL;    // $a
  int[] a = c.arr; // $r1
  int t = a[0];    // $r2


Now I remember this is the example from "Final Fields Semantics" by Sitnikov and Kovalenko:
  https://www.slideshare.net/VladimirSitnikv/final-field-semantics, see around slide #68

Thanks,
-Aleksey


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

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

Re: Correctness of final array access under a race​​​​​​​

Jonas Konrad
JCIP also talks about this behaviour in section 16.3: all variables that
can be *reached* through a final field are visible to other threads
after (proper) construction. It also explicitly mentions array contents
as an example of this.

- Jonas

On 08/31/2017 03:04 PM, Aleksey Shipilev wrote:

> On 08/30/2017 08:32 PM, Nikita Koval wrote:
>> I am thinking about reading String under a race. String class has the array of chars field, which is
>> final and is initialized during the construction. However, elements of this array "are not final" in
>> terms of the memory model (but they effectively are). Therefore, I do not understand why reading the
>> array of non-final chars cannot read the array of default char elements. I think I do not clearly
>> understand the final's semantics.
>
> I think it follows directly from the spec definition:
>
> "Given a write $w, a freeze $f, an action $a (that is not a read of a final field), a read
> $r1 of the final field frozen by $f, and a read $r2 such that hb($w, $f), hb($f, $a), mc($a, $r1),
> and dereferences($r1, $r2), then when determining which values can be seen by $r2,
> we consider hb($w, $r2)."
>
> For example:
>
> Thread 1:
>
>    class C {
>      final int[] arr;
>      C() {
>         arr = new int[1];
>         arr[0] = 42; // $w
>         {freeze}     // $f
>      }
>    }
>
>    GLOBAL = new C;
>
>
> Thread 2:
>
>    C c = GLOBAL;    // $a
>    int[] a = c.arr; // $r1
>    int t = a[0];    // $r2
>
>
> Now I remember this is the example from "Final Fields Semantics" by Sitnikov and Kovalenko:
>    https://www.slideshare.net/VladimirSitnikv/final-field-semantics, see around slide #68
>
> Thanks,
> -Aleksey
>
>
>
> _______________________________________________
> 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