[concurrency-interest] Volatile stores in constructors, disallowed to see the default value
Oleksandr Otenko
oleksandr.otenko at oracle.com
Thu Nov 28 06:36:25 EST 2013
On 28/11/2013 06:27, Aleksey Shipilev wrote:
> On 11/28/2013 02:46 AM, David Holmes wrote:
>>> In order to answer what outcomes are possible we need to dump the
>>> usual/partial/misleading "reorderings" and "happens-before" mindset, and
>>> get to the ground of spec. That is, we need to construct the possible
>>> traces and see if those traces are committable, as per JLS 17.4.8.
>> And therein lies your mistake. The "happens-before mindset" as you put it is
>> what determines what the legal executions are. It was obvious from
>> happens-before considerations that your premise was invalid.
> Happens-before alone is not enough to mandate the semantics of Java
> Memory Model. Even though it can cover the significant part of the
> behaviors, the complete behavior of the model is governed by
> well-formedness of executions, as per JLS 17.4.{6-8}. The classic
> example (even shown in spec!) when the happens-before consistent program
> produces causality violations.
>
>> Q.E.D
> So, there was nothing "obvious" unless you have the concrete proof. The
> only reasonable way to prove this particular thing *was* to show the
> committable traces leading to particular results (like I did), *and* to
On the contrary, the minimal thing here is not to show how 0 can be
achieved, but to prove 42 is achievable *always*. If you cannot prove 42
is achievable always, it means there may be a execution order that
results in something other than 42.
This requires a proof of "observation of store(a,r2) implies store(r2.f,
42) is observable". A sufficient proof for this is a store-store
barrier. If you have other proofs that don't allow reordering of these
stores (hence make the implication true), you can use those. (eg
final-field semantics is one alternative proof) In the absence of such
proof I don't need to show */how/* 0 may be achieved.
Alex
> find flaws in the reasoning in larger JMM. "La-la-la, happens-before,
> la-la-la" is hardly a proof, even though the conclusion is the same in
> this particular case. Make no mistake about it.
>
> -Aleksey
> _______________________________________________
> Concurrency-interest mailing list
> Concurrency-interest at cs.oswego.edu
> http://cs.oswego.edu/mailman/listinfo/concurrency-interest
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://cs.oswego.edu/pipermail/concurrency-interest/attachments/20131128/eab82dde/attachment-0001.html>
More information about the Concurrency-interest
mailing list