lkml.org 
[lkml]   [2019]   [Aug]   [26]   [last100]   RSS Feed
Views: [wrap][no wrap]   [headers]  [forward] 
 
Messages in this thread
    /
    Date
    From
    SubjectRe: numlist_push() barriers Re: [RFC PATCH v4 1/9] printk-rb: add a new printk ringbuffer implementation
    Sorry for top posting, but I forgot to mention: as you might have
    noticed, my @amarulasolutions address is not active anymore; FWIW,
    you should still be able to reach me at this @gmail address.

    Thanks,
    Andrea


    On Mon, Aug 26, 2019 at 10:34:36AM +0200, Andrea Parri wrote:
    > > > + /*
    > > > + * bA:
    > > > + *
    > > > + * Setup the node to be a list terminator: next_id == id.
    > > > + */
    > > > + WRITE_ONCE(n->next_id, id);
    > >
    > > Do we need WRITE_ONCE() here?
    > > Both "n" and "id" are given as parameters and do not change.
    > > The assigment must be done before "id" is set as nl->head_id.
    > > The ordering is enforced by cmpxchg_release().
    >
    > (Disclaimer: this is still a very much debated issue...)
    >
    > According to the LKMM, this question boils down to the question:
    >
    > Is there "ordering"/synchronization between the above access and
    > the "matching accesses" bF and aA' to the same location?
    >
    > Again according to the LKMM's analysis, such synchronization is provided
    > by the RELEASE -> "reads-from" -> ADDR relation. (Encoding address dep.
    > in litmus tests is kind of tricky but possible, e.g., for the pattern in
    > question, we could write/model as follows:
    >
    > C S+ponarelease+addroncena
    >
    > {
    > int *y = &a;
    > }
    >
    > P0(int *x, int **y, int *a)
    > {
    > int *r0;
    >
    > *x = 2;
    > r0 = cmpxchg_release(y, a, x);
    > }
    >
    > P1(int *x, int **y)
    > {
    > int *r0;
    >
    > r0 = READ_ONCE(*y);
    > *r0 = 1;
    > }
    >
    > exists (1:r0=x /\ x=2)
    >
    > Then
    >
    > $ herd7 -conf linux-kernel.cfg S+ponarelease+addroncena
    > Test S+ponarelease+addroncena Allowed
    > States 2
    > 1:r0=a; x=2;
    > 1:r0=x; x=1;
    > No
    > Witnesses
    > Positive: 0 Negative: 2
    > Condition exists (1:r0=x /\ x=2)
    > Observation S+ponarelease+addroncena Never 0 2
    > Time S+ponarelease+addroncena 0.01
    > Hash=7eaf7b5e95419a3c352d7fd50b9cd0d5
    >
    > that is, the test is not racy and the "exists" clause is not satisfiable
    > in the LKMM. Notice that _if the READ_ONCE(*y) in P1 were replaced by a
    > plain read, then we would obtain:
    >
    > Test S+ponarelease+addrnana Allowed
    > States 2
    > 1:r0=x; x=1;
    > 1:r0=x; x=2;
    > Ok
    > Witnesses
    > Positive: 1 Negative: 1
    > Flag data-race [ <-- the LKMM warns about a data-race ]
    > Condition exists (1:r0=x /\ x=2)
    > Observation S+ponarelease+addrnana Sometimes 1 1
    > Time S+ponarelease+addrnana 0.00
    > Hash=a61acf2e8e51c2129d33ddf5e4c76a49
    >
    > N.B. This analysis generally depends on the assumption that every marked
    > access (e.g., the cmpxchg_release() called out above and the READ_ONCE()
    > heading the address dependencies) are _single-copy atomic, an assumption
    > which has been recently shown to _not be valid in such generality:
    >
    > https://lkml.kernel.org/r/20190821103200.kpufwtviqhpbuv2n@willie-the-truck
    >
    > (Bug in the LKMM? or in the Linux implementation of these primitives? or
    > in the compiler? your blame here...)
    >
    >
    > [...]
    >
    > > > + /*
    > > > + * bD:
    > > > + *
    > > > + * Set @seq to +1 of @seq from the previous head.
    > > > + *
    > > > + * Memory barrier involvement:
    > > > + *
    > > > + * If bB reads from bE, then bC->aA reads from bD.
    > > > + *
    > > > + * Relies on:
    > > > + *
    > > > + * RELEASE from bD to bE
    > > > + * matching
    > > > + * ADDRESS DEP. from bB to bC->aA
    > > > + */
    > > > + WRITE_ONCE(n->seq, seq + 1);
    > >
    > > Do we really need WRITE_ONCE() here?
    > > It is the same problem as with setting n->next_id above.
    >
    > Same considerations as above would apply here.
    >
    > Andrea

    \
     
     \ /
      Last update: 2019-08-26 10:45    [W:4.189 / U:0.052 seconds]
    ©2003-2020 Jasper Spaans|hosted at Digital Ocean and TransIP|Read the blog|Advertise on this site