[concurrency-interest] RFR: 8065804:JEP171:Clarifications/corrections for fence intrinsics

DT dt at flyingtroika.com
Mon Dec 1 21:54:02 EST 2014


Roman, thank you. As it has been mentioned before from practical 
perspective its quite difficult to incorporate. Though as I understood , 
can be wrong of course that volatile variables and immutable objects 
represent  lineariazable objects because they satisfy those concurrent 
conditions.

Dmitry

On 11/26/2014 11:00 AM, Roman Elizarov wrote:
>
> I'd suggest to start with the original paper by Herlihy who had come 
> up with the concept of Linearizability in 1990:
>
> Linearizability: A Correctness Condition for Concurrent Objects
>
> http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.142.5315
>
>
> There were lot of reasearch about linearizability since then (there 
> are almost a thouthand citations for this arcticle) expanding and 
> improving proof techniquies and applying it. There were no 
> breakthroughs of the comparable magnitude since then. All 
> "thread-safe" objects that you enconter in the modern word are 
> linearizable. It is a defacto "golden standard" correctness condition 
> for concurrent objects.
>
>
> This position is well deserved, because having lineariazable objects 
> as your building blocks makes it super-easy to formally reason about 
> correctness of your code. You will rarely encouter concurrent 
> algorithms that provide weaker guarantees (like quescient 
> consistency), because they all too hard to reason about -- they are 
> either not composable or not local. But when all your 
> concurrent objects are linearizable, then you can ditch 
> happens-before, forget that everything is actually parallel and 
> simply reason about your code in terms of interleaving of "atomic" 
> operations that happen in some global order. That is the beauty of 
> linearizability.
>
>
> But Linearizability is indeed a pretty strong requirement. 
> Linearizability of your shared memory requires that Independent Reads 
> of Independent Writes (IRIW) are consistent. Can you get away with 
> some weaker requirement and still get all the same goodies as 
> linearizability gets you? I have not seen anything promising in this 
> direction. Whoever makes this breakthrough will surely reap the 
> world's recognition and respect.
>
>
> /Roman
>
>
> ------------------------------------------------------------------------
> *От:* DT <dt at flyingtroika.com>
> *Отправлено:* 26 ноября 2014 г. 20:24
> *Кому:* Roman Elizarov; dholmes at ieee.org; Hans Boehm
> *Копия:* core-libs-dev; concurrency-interest at cs.oswego.edu
> *Тема:* Re: [concurrency-interest] RFR: 
> 8065804:JEP171:Clarifications/corrections for fence intrinsics
> Roman,
> Can you point to any specific article providing the concurrency 
> problem statement with a further proof using linearizability to reason 
> about solution.
>
> Thanks,
> DT
>
> On 11/26/2014 2:59 AM, Roman Elizarov wrote:
>>
>> Whether IRIW has any _/practical/_ uses is definitely subject to 
>> debate. However, there is no tractable way for formal reasoning about 
>> properties of large concurrent systems, but via linearizability. 
>> Linearizability is the only property that is both local and 
>> hierarchical. It lets you build more complex linearizable algorithms 
>> from simpler ones, having quite succinct and compelling proofs at 
>> each step.
>>
>> In other words, if you want to be able to construct a formal proof 
>> that your [large] concurrent system if correct, then you must have 
>> IRIW consistency. Do you need a formal proof of correctness? Maybe 
>> not. In many applications hand-waving is enough,  but there are many 
>> other applications where hand-waving does not count as a proof. It 
>> may be possible to construct formal correctness proofs for some very 
>> simple algorithms even on a system that does not provide IRIW, but 
>> this is beyond the state of the art of formal verification for 
>> anything sufficiently complex.
>>
>> /Roman
>>
>> *From:*David Holmes [mailto:davidcholmes at aapt.net.au]
>> *Sent:* Wednesday, November 26, 2014 11:54 AM
>> *To:* Roman Elizarov; Hans Boehm
>> *Cc:* concurrency-interest at cs.oswego.edu; core-libs-dev
>> *Subject:* RE: [concurrency-interest] RFR: 
>> 8065804:JEP171:Clarifications/corrections for fence intrinsics
>>
>> Can you expand on that please. All previous discussion of IRIW I have 
>> seen indicated that the property, while a consequence of existing JMM 
>> rules, had no practical use.
>>
>> Thanks,
>>
>> David
>>
>>     -----Original Message-----
>>     *From:* Roman Elizarov [mailto:elizarov at devexperts.com]
>>     *Sent:* Wednesday, 26 November 2014 6:49 PM
>>     *To:* dholmes at ieee.org <mailto:dholmes at ieee.org>; Hans Boehm
>>     *Cc:* concurrency-interest at cs.oswego.edu
>>     <mailto:concurrency-interest at cs.oswego.edu>; core-libs-dev
>>     *Subject:* RE: [concurrency-interest] RFR:
>>     8065804:JEP171:Clarifications/corrections for fence intrinsics
>>
>>     There is no conceivable way to kill IRIW consistency requirement
>>     while retaining ability to prove correctness of large software
>>     systems. If IRIW of volatile variables are not consistent, then
>>     volatile reads and writes are not linearizable, which breaks
>>     linearizabiliy of all higher-level primitives build on top of
>>     them and makes formal reasoning about behavior of concurrent
>>     systems practically impossible. There are many fields where this
>>     is not acceptable.
>>
>>     /Roman
>>
>>     *From:*concurrency-interest-bounces at cs.oswego.edu
>>     <mailto:concurrency-interest-bounces at cs.oswego.edu>
>>     [mailto:concurrency-interest-bounces at cs.oswego.edu] *On Behalf Of
>>     *David Holmes
>>     *Sent:* Wednesday, November 26, 2014 5:11 AM
>>     *To:* Hans Boehm
>>     *Cc:* concurrency-interest at cs.oswego.edu
>>     <mailto:concurrency-interest at cs.oswego.edu>; core-libs-dev
>>     *Subject:* Re: [concurrency-interest] RFR: 8065804:
>>     JEP171:Clarifications/corrections for fence intrinsics
>>
>>     Hi Hans,
>>
>>     Given IRIW is a thorn in everyone's side and has no known useful
>>     benefit, and can hopefully be killed off in the future, lets not
>>     get bogged down in IRIW. But none of what you say below relates
>>     to multi-copy-atomicity.
>>
>>     Cheers,
>>
>>     David
>>
>>         -----Original Message-----
>>         *From:* hjkhboehm at gmail.com
>>         <mailto:hjkhboehm at gmail.com>[mailto:hjkhboehm at gmail.com]*On
>>         Behalf Of *Hans Boehm
>>         *Sent:* Wednesday, 26 November 2014 12:04 PM
>>         *To:* dholmes at ieee.org <mailto:dholmes at ieee.org>
>>         *Cc:* Stephan Diestelhorst;
>>         concurrency-interest at cs.oswego.edu
>>         <mailto:concurrency-interest at cs.oswego.edu>; core-libs-dev
>>         *Subject:* Re: [concurrency-interest] RFR: 8065804:
>>         JEP171:Clarifications/corrections for fence intrinsics
>>
>>         To be concrete here, on Power, loads can normally be ordered
>>         by an address dependency or light-weight fence (lwsync).
>>         However, neither is enough to prevent the questionable
>>         outcome for IRIW, since it doesn't ensure that the stores in
>>         T1 and T2 will be made visible to other threads in a
>>         consistent order. That outcome can be prevented by using
>>         heavyweight fences (sync) instructions between the loads
>>         instead.  Peter Sewell's group concluded that to enforce
>>         correct volatile behavior on Power, you essentially need a a
>>         heavyweight fence between every pair of volatile operations
>>         on Power.  That cannot be understood based on simple ordering
>>         constraints.
>>
>>         As Stephan pointed out, there are similar issues on ARM, but
>>         they're less commonly encountered in a Java implementation.
>>         If you're lucky, you can get to the right implementation
>>         recipe by looking at only reordering, I think.
>>
>>         On Tue, Nov 25, 2014 at 4:36 PM, David Holmes
>>         <davidcholmes at aapt.net.au <mailto:davidcholmes at aapt.net.au>>
>>         wrote:
>>
>>             Stephan Diestelhorst writes:
>>             >
>>             > David Holmes wrote:
>>             > > Stephan Diestelhorst writes:
>>             > > > Am Dienstag, 25. November 2014, 11:15:36 schrieb
>>             Hans Boehm:
>>             > > > > I'm no hardware architect, but fundamentally it
>>             seems to me that
>>             > > > >
>>             > > > > load x
>>             > > > > acquire_fence
>>             > > > >
>>             > > > > imposes a much more stringent constraint than
>>             > > > >
>>             > > > > load_acquire x
>>             > > > >
>>             > > > > Consider the case in which the load from x is an
>>             L1 hit, but a
>>             > > > > preceding load (from say y) is a long-latency
>>             miss.  If we enforce
>>             > > > > ordering by just waiting for completion of prior
>>             operation, the
>>             > > > > former has to wait for the load from y to
>>             complete; while the
>>             > > > > latter doesn't.  I find it hard to believe that
>>             this doesn't leave
>>             > > > > an appreciable amount of performance on the
>>             table, at least for
>>             > > > > some interesting microarchitectures.
>>             > > >
>>             > > > I agree, Hans, that this is a reasonable
>>             assumption.  Load_acquire x
>>             > > > does allow roach motel, whereas the acquire fence
>>             does not.
>>             > > >
>>             > > > >  In addition, for better or worse, fencing
>>             requirements on at least
>>             > > > >  Power are actually driven as much by store
>>             atomicity issues, as by
>>             > > > >  the ordering issues discussed in the cookbook. 
>>             This was not
>>             > > > >  understood in 2005, and unfortunately doesn't
>>             seem to be
>>             > amenable to
>>             > > > >  the kind of straightforward explanation as in
>>             Doug's cookbook.
>>             > > >
>>             > > > Coming from a strongly ordered architecture to a
>>             weakly ordered one
>>             > > > myself, I also needed some mental adjustment about
>>             store (multi-copy)
>>             > > > atomicity.  I can imagine others will be unaware of
>>             this difference,
>>             > > > too, even in 2014.
>>             > >
>>             > > Sorry I'm missing the connection between fences and
>>             multi-copy
>>             > atomicity.
>>             >
>>             > One example is the classic IRIW. With non-multi copy
>>             atomic stores, but
>>             > ordered (say through a dependency) loads in the
>>             following example:
>>             >
>>             > Memory: foo = bar = 0
>>             > _T1_         _T2_         _T3_                       _T4_
>>             > st (foo),1   st (bar),1   ld r1, (bar)                 
>>                 ld r3,(foo)
>>             >                           <addr dep / local "fence"
>>             here>   <addr dep>
>>             >                           ld r2, (foo)                 
>>                 ld r4, (bar)
>>             >
>>             > You may observe r1 = 1, r2 = 0, r3 = 1, r4 = 0 on
>>             non-multi-copy atomic
>>             > machines.  On TSO boxes, this is not possible.  That
>>             means that the
>>             > memory fence that will prevent such a behaviour (DMB on
>>             ARM) needs to
>>             > carry some additional oomph in ensuring multi-copy
>>             atomicity, or rather
>>             > prevent you from seeing it (which is the same thing).
>>
>>             I take it as given that any code for which you may have
>>             ordering
>>             constraints, must first have basic atomicity properties
>>             for loads and
>>             stores. I would not expect any kind of fence to add
>>             multi-copy-atomicity
>>             where there was none.
>>
>>             David
>>
>>
>>             > Stephan
>>             >
>>             > _______________________________________________
>>             > Concurrency-interest mailing list
>>             > Concurrency-interest at cs.oswego.edu
>>             <mailto:Concurrency-interest at cs.oswego.edu>
>>             > http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>>
>>             _______________________________________________
>>             Concurrency-interest mailing list
>>             Concurrency-interest at cs.oswego.edu
>>             <mailto:Concurrency-interest at cs.oswego.edu>
>>             http://cs.oswego.edu/mailman/listinfo/concurrency-interest
>>
>>
>>
>> _______________________________________________
>> 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/20141201/800e3d3f/attachment-0001.html>


More information about the Concurrency-interest mailing list