[concurrency-interest] Correctness of final array access under a race​​​​​​​

Aleksey Shipilev shade at redhat.com
Thu Aug 31 09:04:13 EDT 2017

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


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20170831/2e7df510/attachment.sig>

More information about the Concurrency-interest mailing list