On Tue, 22 Jan 2019, Andrea Parri wrote:
> > @@ -131,7 +159,7 @@ let rec rcu-fence = rcu-gp | srcu-gp |
> > (rcu-fence ; rcu-link ; rcu-fence)
> >
> > (* rb orders instructions just as pb does *)
> > -let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb*
> > +let rb = prop ; po ; rcu-fence ; po?
> @@ -131,7 +159,7 @@ let rec rcu-fence = rcu-gp | srcu-gp |
> (rcu-fence ; rcu-link ; rcu-fence)
>
> (* rb orders instructions just as pb does *)
> -let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb*
> +let rb = prop ; po ; rcu-fence ; po? ; hb* ; pb* ; [marked]
Testing has revealed some s
On Thu, Jan 17, 2019 at 02:43:54PM -0500, Alan Stern wrote:
> On Wed, 16 Jan 2019, Andrea Parri wrote:
>
> > Can the compiler (maybe, it does?) transform, at the C or at the "asm"
> > level, LB1's P0 in LB2's P0 (LB1 and LB2 are reported below)?
> >
> > C LB1
> >
> > {
> > int *x = &a;
> > }
On Fri, 18 Jan 2019, Andrea Parri wrote:
> > A relatively simple solution to this problem would be to say that
> > smp_wmb doesn't order plain writes.
>
> It seems so; I don't have other solutions to suggest ATM. (But, TBH,
> I'm still in the process of reviewing/testing these changes... )
>
>
On Fri, Jan 18, 2019 at 10:10:22AM -0500, Alan Stern wrote:
> On Thu, 17 Jan 2019, Andrea Parri wrote:
>
> > > Can the compiler (maybe, it does?) transform, at the C or at the "asm"
> > > level, LB1's P0 in LB2's P0 (LB1 and LB2 are reported below)?
> > >
> > > C LB1
> > >
> > > {
> > > int *x
On Thu, 17 Jan 2019, Andrea Parri wrote:
> > Can the compiler (maybe, it does?) transform, at the C or at the "asm"
> > level, LB1's P0 in LB2's P0 (LB1 and LB2 are reported below)?
> >
> > C LB1
> >
> > {
> > int *x = &a;
> > }
> >
> > P0(int **x, int *y)
> > {
> > int *r0;
> >
> >
On Thu, 17 Jan 2019, Andrea Parri wrote:
> > > There is a special case (data;rfi) that doesn't
> > > provide ordering in itself but can contribute to other
> > > orderings. A data;rfi link corresponds to situations
> > > where a value is stored in a tempora
On Wed, 16 Jan 2019, Andrea Parri wrote:
> Can the compiler (maybe, it does?) transform, at the C or at the "asm"
> level, LB1's P0 in LB2's P0 (LB1 and LB2 are reported below)?
>
> C LB1
>
> {
> int *x = &a;
> }
>
> P0(int **x, int *y)
> {
> int *r0;
>
> r0 = rcu_dereference
On Wed, Jan 16, 2019 at 10:36:58PM +0100, Andrea Parri wrote:
> [...]
>
> > The difficulty with incorporating plain accesses in the memory model
> > is that the compiler has very few constraints on how it treats plain
> > accesses. It can eliminate them, duplicate them, rearrange them,
> > merge
[...]
> The difficulty with incorporating plain accesses in the memory model
> is that the compiler has very few constraints on how it treats plain
> accesses. It can eliminate them, duplicate them, rearrange them,
> merge them, split them up, and goodness knows what else. To make some
> sense o
On Wed, 16 Jan 2019, Paul E. McKenney wrote:
> On Wed, Jan 16, 2019 at 12:57:52PM +0100, Peter Zijlstra wrote:
> > On Tue, Jan 15, 2019 at 10:19:10AM -0500, Alan Stern wrote:
> > > On Tue, 15 Jan 2019, Andrea Parri wrote:
> > >
> > > > Unless I'm mis-reading/-applying this definition, this will f
On Wed, Jan 16, 2019 at 12:57:52PM +0100, Peter Zijlstra wrote:
> On Tue, Jan 15, 2019 at 10:19:10AM -0500, Alan Stern wrote:
> > On Tue, 15 Jan 2019, Andrea Parri wrote:
> >
> > > Unless I'm mis-reading/-applying this definition, this will flag the
> > > following test (a variation on your "race.
On Tue, Jan 15, 2019 at 10:19:10AM -0500, Alan Stern wrote:
> On Tue, 15 Jan 2019, Andrea Parri wrote:
>
> > Unless I'm mis-reading/-applying this definition, this will flag the
> > following test (a variation on your "race.litmus") with "data-race":
> >
> > C no-race
> >
> > {}
> >
> > P0(int
On Tue, Jan 15, 2019 at 10:03:26AM -0500, Alan Stern wrote:
> On Tue, 15 Jan 2019, Dmitry Vyukov wrote:
>
> > On Tue, Jan 15, 2019 at 12:54 AM Paul E. McKenney
> > wrote:
> > >
> > > On Mon, Jan 14, 2019 at 02:41:49PM -0500, Alan Stern wrote:
> > > > The patch below is my first attempt at adapti
On Tue, 15 Jan 2019, Andrea Parri wrote:
> Unless I'm mis-reading/-applying this definition, this will flag the
> following test (a variation on your "race.litmus") with "data-race":
>
> C no-race
>
> {}
>
> P0(int *x, spinlock_t *s)
> {
> spin_lock(s);
> WRITE_ONCE(*x, 1);/*
On Tue, 15 Jan 2019, Dmitry Vyukov wrote:
> On Tue, Jan 15, 2019 at 12:54 AM Paul E. McKenney
> wrote:
> >
> > On Mon, Jan 14, 2019 at 02:41:49PM -0500, Alan Stern wrote:
> > > The patch below is my first attempt at adapting the Linux Kernel
> > > Memory Model to handle plain accesses (i.e., tho
On Mon, Jan 14, 2019 at 02:41:49PM -0500, Alan Stern wrote:
> The patch below is my first attempt at adapting the Linux Kernel
> Memory Model to handle plain accesses (i.e., those which aren't
> specially marked as READ_ONCE, WRITE_ONCE, acquire, release,
> read-modify-write, or lock accesses). Th
On Tue, Jan 15, 2019 at 12:54 AM Paul E. McKenney wrote:
>
> On Mon, Jan 14, 2019 at 02:41:49PM -0500, Alan Stern wrote:
> > The patch below is my first attempt at adapting the Linux Kernel
> > Memory Model to handle plain accesses (i.e., those which aren't
> > specially marked as READ_ONCE, WRITE
18 matches
Mail list logo
