From: Andrea Parri <parri.andrea@gmail.com> To: Peter Zijlstra <peterz@infradead.org> Cc: linux-kernel@vger.kernel.org, Palmer Dabbelt <palmer@sifive.com>, Albert Ou <albert@sifive.com>, Daniel Lustig <dlustig@nvidia.com>, Alan Stern <stern@rowland.harvard.edu>, Will Deacon <will.deacon@arm.com>, Boqun Feng <boqun.feng@gmail.com>, Nicholas Piggin <npiggin@gmail.com>, David Howells <dhowells@redhat.com>, Jade Alglave <j.alglave@ucl.ac.uk>, Luc Maranget <luc.maranget@inria.fr>, "Paul E. McKenney" <paulmck@linux.vnet.ibm.com>, Akira Yokosawa <akiyks@gmail.com>, Ingo Molnar <mingo@kernel.org>, Linus Torvalds <torvalds@linux-foundation.org>, linux-riscv@lists.infradead.org Subject: Re: [RFC PATCH] riscv/locking: Strengthen spin_lock() and spin_unlock() Date: Thu, 22 Feb 2018 15:12:49 +0100 [thread overview] Message-ID: <20180222141249.GA14033@andrea> (raw) In-Reply-To: <20180222134004.GN25181@hirez.programming.kicks-ass.net> On Thu, Feb 22, 2018 at 02:40:04PM +0100, Peter Zijlstra wrote: > On Thu, Feb 22, 2018 at 01:19:50PM +0100, Andrea Parri wrote: > > > C unlock-lock-read-ordering > > > > {} > > /* s initially owned by P1 */ > > > > P0(int *x, int *y) > > { > > WRITE_ONCE(*x, 1); > > smp_wmb(); > > WRITE_ONCE(*y, 1); > > } > > > > P1(int *x, int *y, spinlock_t *s) > > { > > int r0; > > int r1; > > > > r0 = READ_ONCE(*y); > > spin_unlock(s); > > spin_lock(s); > > r1 = READ_ONCE(*y); > > } > > > > exists (1:r0=1 /\ 1:r1=0) > > > > RISCV RISCV-unlock-lock-read-ordering > > { > > 0:x2=x; 0:x4=y; > > 1:x2=y; 1:x4=x; 1:x6=s; > > s=1; > > } > > P0 | P1 ; > > ori x1,x0,1 | lw x1,0(x2) ; > > sw x1,0(x2) | amoswap.w.rl x0,x0,(x6) ; > > fence w,w | ori x5,x0,1 ; > > ori x3,x0,1 | amoswap.w.aq x0,x5,(x6) ; > > sw x3,0(x4) | lw x3,0(x4) ; > > exists > > (1:x1=1 /\ 1:x3=0) > > So I would indeed expect this to be forbidden. Could someone please > explain how this could be allowed? As mentioned in IRC, my understanding here is only based on the spec. referred below and on its (available) formalizations. I expect that RISC-V people will be able to provide more information. > > > C unlock-lock-write-ordering > > > > {} > > /* s initially owned by P0 */ > > > > P0(int *x, int *y, spinlock_t *s) > > { > > WRITE_ONCE(*x, 1); > > spin_unlock(s); > > spin_lock(s); > > WRITE_ONCE(*y, 1); > > } > > > > P1(int *x, int *y) > > { > > int r0; > > int r1; > > > > r0 = READ_ONCE(*y); > > smp_rmb(); > > r1 = READ_ONCE(*y); > > } > > > > exists (1:r0=1 /\ 1:r1=0) > > > > RISCV RISCV-unlock-lock-write-ordering > > { > > 0:x2=x; 0:x4=y; 0:x6=s; > > 1:x2=y; 1:x4=x; > > s=1; > > } > > P0 | P1 ; > > ori x1,x0,1 | lw x1,0(x2) ; > > sw x1,0(x2) | fence r,r ; > > amoswap.w.rl x0,x0,(x6) | lw x3,0(x4) ; > > ori x5,x0,1 | ; > > amoswap.w.aq x0,x5,(x6) | ; > > ori x3,x0,1 | ; > > sw x3,0(x4) | ; > > exists > > (1:x1=1 /\ 1:x3=0) > > And here I think the RISCV conversion is flawed, there should be a ctrl > dependency. The second store-word in P0 should depend on the result of > amoswap.w.aq being 0. You're right: AFAICT, this can be remedied by inserting "beq x0,x5,FAIL00" right after amoswap.w.aq (and this label at the end of P0); this does not change the verdict of the available formalizations reported above however. (So, AFAICT, the above question remains valid/open.) Andrea > > (strictly speaking there should be a ctrl-dep in the read example too, > except it'd be pointless for ordering reads, so I accept it being left > out) > > Again, I cannot see how this could be allowed. >
WARNING: multiple messages have this Message-ID (diff)
From: parri.andrea@gmail.com (Andrea Parri) To: linux-riscv@lists.infradead.org Subject: [RFC PATCH] riscv/locking: Strengthen spin_lock() and spin_unlock() Date: Thu, 22 Feb 2018 15:12:49 +0100 [thread overview] Message-ID: <20180222141249.GA14033@andrea> (raw) In-Reply-To: <20180222134004.GN25181@hirez.programming.kicks-ass.net> On Thu, Feb 22, 2018 at 02:40:04PM +0100, Peter Zijlstra wrote: > On Thu, Feb 22, 2018 at 01:19:50PM +0100, Andrea Parri wrote: > > > C unlock-lock-read-ordering > > > > {} > > /* s initially owned by P1 */ > > > > P0(int *x, int *y) > > { > > WRITE_ONCE(*x, 1); > > smp_wmb(); > > WRITE_ONCE(*y, 1); > > } > > > > P1(int *x, int *y, spinlock_t *s) > > { > > int r0; > > int r1; > > > > r0 = READ_ONCE(*y); > > spin_unlock(s); > > spin_lock(s); > > r1 = READ_ONCE(*y); > > } > > > > exists (1:r0=1 /\ 1:r1=0) > > > > RISCV RISCV-unlock-lock-read-ordering > > { > > 0:x2=x; 0:x4=y; > > 1:x2=y; 1:x4=x; 1:x6=s; > > s=1; > > } > > P0 | P1 ; > > ori x1,x0,1 | lw x1,0(x2) ; > > sw x1,0(x2) | amoswap.w.rl x0,x0,(x6) ; > > fence w,w | ori x5,x0,1 ; > > ori x3,x0,1 | amoswap.w.aq x0,x5,(x6) ; > > sw x3,0(x4) | lw x3,0(x4) ; > > exists > > (1:x1=1 /\ 1:x3=0) > > So I would indeed expect this to be forbidden. Could someone please > explain how this could be allowed? As mentioned in IRC, my understanding here is only based on the spec. referred below and on its (available) formalizations. I expect that RISC-V people will be able to provide more information. > > > C unlock-lock-write-ordering > > > > {} > > /* s initially owned by P0 */ > > > > P0(int *x, int *y, spinlock_t *s) > > { > > WRITE_ONCE(*x, 1); > > spin_unlock(s); > > spin_lock(s); > > WRITE_ONCE(*y, 1); > > } > > > > P1(int *x, int *y) > > { > > int r0; > > int r1; > > > > r0 = READ_ONCE(*y); > > smp_rmb(); > > r1 = READ_ONCE(*y); > > } > > > > exists (1:r0=1 /\ 1:r1=0) > > > > RISCV RISCV-unlock-lock-write-ordering > > { > > 0:x2=x; 0:x4=y; 0:x6=s; > > 1:x2=y; 1:x4=x; > > s=1; > > } > > P0 | P1 ; > > ori x1,x0,1 | lw x1,0(x2) ; > > sw x1,0(x2) | fence r,r ; > > amoswap.w.rl x0,x0,(x6) | lw x3,0(x4) ; > > ori x5,x0,1 | ; > > amoswap.w.aq x0,x5,(x6) | ; > > ori x3,x0,1 | ; > > sw x3,0(x4) | ; > > exists > > (1:x1=1 /\ 1:x3=0) > > And here I think the RISCV conversion is flawed, there should be a ctrl > dependency. The second store-word in P0 should depend on the result of > amoswap.w.aq being 0. You're right: AFAICT, this can be remedied by inserting "beq x0,x5,FAIL00" right after amoswap.w.aq (and this label at the end of P0); this does not change the verdict of the available formalizations reported above however. (So, AFAICT, the above question remains valid/open.) Andrea > > (strictly speaking there should be a ctrl-dep in the read example too, > except it'd be pointless for ordering reads, so I accept it being left > out) > > Again, I cannot see how this could be allowed. >
next prev parent reply other threads:[~2018-02-22 14:12 UTC|newest] Thread overview: 46+ messages / expand[flat|nested] mbox.gz Atom feed top 2018-02-22 12:19 [RFC PATCH] riscv/locking: Strengthen spin_lock() and spin_unlock() Andrea Parri 2018-02-22 12:19 ` Andrea Parri 2018-02-22 12:44 ` Andrea Parri 2018-02-22 12:44 ` Andrea Parri 2018-02-22 13:40 ` Peter Zijlstra 2018-02-22 13:40 ` Peter Zijlstra 2018-02-22 14:12 ` Andrea Parri [this message] 2018-02-22 14:12 ` Andrea Parri 2018-02-22 17:27 ` Daniel Lustig 2018-02-22 17:27 ` Daniel Lustig 2018-02-22 18:13 ` Paul E. McKenney 2018-02-22 18:13 ` Paul E. McKenney 2018-02-22 18:27 ` Peter Zijlstra 2018-02-22 18:27 ` Peter Zijlstra 2018-02-22 19:47 ` Daniel Lustig 2018-02-22 19:47 ` Daniel Lustig 2018-02-23 11:16 ` Andrea Parri 2018-02-23 11:16 ` Andrea Parri 2018-02-26 10:39 ` Will Deacon 2018-02-26 10:39 ` Will Deacon 2018-02-26 14:21 ` Luc Maranget 2018-02-26 14:21 ` Luc Maranget 2018-02-26 16:06 ` Linus Torvalds 2018-02-26 16:06 ` Linus Torvalds 2018-02-26 16:24 ` Will Deacon 2018-02-26 16:24 ` Will Deacon 2018-02-26 17:00 ` Linus Torvalds 2018-02-26 17:00 ` Linus Torvalds 2018-02-26 17:10 ` Will Deacon 2018-02-26 17:10 ` Will Deacon 2018-03-06 13:00 ` Peter Zijlstra 2018-03-06 13:00 ` Peter Zijlstra 2018-02-27 5:06 ` Boqun Feng 2018-02-27 5:06 ` Boqun Feng 2018-02-27 10:16 ` Boqun Feng 2018-02-27 10:16 ` Boqun Feng 2018-03-01 15:11 ` Andrea Parri 2018-03-01 15:11 ` Andrea Parri 2018-03-01 21:54 ` Palmer Dabbelt 2018-03-01 21:54 ` Palmer Dabbelt 2018-03-01 22:21 ` Daniel Lustig 2018-03-01 22:21 ` Daniel Lustig 2018-02-22 20:02 ` Paul E. McKenney 2018-02-22 20:02 ` Paul E. McKenney 2018-02-22 18:21 ` Peter Zijlstra 2018-02-22 18:21 ` Peter Zijlstra
Reply instructions: You may reply publicly to this message via plain-text email using any one of the following methods: * Save the following mbox file, import it into your mail client, and reply-to-all from there: mbox Avoid top-posting and favor interleaved quoting: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the --to, --cc, and --in-reply-to switches of git-send-email(1): git send-email \ --in-reply-to=20180222141249.GA14033@andrea \ --to=parri.andrea@gmail.com \ --cc=akiyks@gmail.com \ --cc=albert@sifive.com \ --cc=boqun.feng@gmail.com \ --cc=dhowells@redhat.com \ --cc=dlustig@nvidia.com \ --cc=j.alglave@ucl.ac.uk \ --cc=linux-kernel@vger.kernel.org \ --cc=linux-riscv@lists.infradead.org \ --cc=luc.maranget@inria.fr \ --cc=mingo@kernel.org \ --cc=npiggin@gmail.com \ --cc=palmer@sifive.com \ --cc=paulmck@linux.vnet.ibm.com \ --cc=peterz@infradead.org \ --cc=stern@rowland.harvard.edu \ --cc=torvalds@linux-foundation.org \ --cc=will.deacon@arm.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting the In-Reply-To header via mailto: links, try the mailto: linkBe sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes, see mirroring instructions on how to clone and mirror all data and code used by this external index.