Re: XDP socket rings, and LKMM litmus tests

On Fri, Mar 05, 2021 at 09:12:30AM +0800, Boqun Feng wrote: > On Thu, Mar 04, 2021 at 11:11:42AM -0500, Alan Stern wrote: > > Forget about local variables for the time being and just consider > > > > dep ; [Plain] ; rfi > > > > For example: > > > > A: r1 = READ_ONCE(x); > >y =

Re: XDP socket rings, and LKMM litmus tests

On Thu, Mar 04, 2021 at 11:11:42AM -0500, Alan Stern wrote: > On Thu, Mar 04, 2021 at 02:33:32PM +0800, Boqun Feng wrote: > > > Right, I was thinking about something unrelated.. but how about the > > following case: > > > > local_v = > > r1 = READ_ONCE(*x); // f > > > > if (r1 ==

Re: XDP socket rings, and LKMM litmus tests

On Thu, Mar 04, 2021 at 04:27:53PM -0500, Alan Stern wrote: > On Thu, Mar 04, 2021 at 11:05:15AM -0800, Paul E. McKenney wrote: > > On Thu, Mar 04, 2021 at 10:35:24AM -0500, Alan Stern wrote: > > > On Wed, Mar 03, 2021 at 09:04:07PM -0800, Paul E. McKenney wrote: > > > > On Wed, Mar 03, 2021 at

Re: XDP socket rings, and LKMM litmus tests

On Thu, Mar 04, 2021 at 11:05:15AM -0800, Paul E. McKenney wrote: > On Thu, Mar 04, 2021 at 10:35:24AM -0500, Alan Stern wrote: > > On Wed, Mar 03, 2021 at 09:04:07PM -0800, Paul E. McKenney wrote: > > > On Wed, Mar 03, 2021 at 10:21:01PM -0500, Alan Stern wrote: > > > > On Wed, Mar 03, 2021 at

Re: XDP socket rings, and LKMM litmus tests

On Thu, Mar 04, 2021 at 04:44:34PM +0100, maranget wrote: > > > > On 3 Mar 2021, at 21:22, Alan Stern wrote: > > > >>> > >>> Local variables absolutely should be treated just like CPU registers, if > >>> possible. In fact, the compiler has the option of keeping local > >>> variables stored

Re: XDP socket rings, and LKMM litmus tests

On Thu, Mar 04, 2021 at 10:35:24AM -0500, Alan Stern wrote: > On Wed, Mar 03, 2021 at 09:04:07PM -0800, Paul E. McKenney wrote: > > On Wed, Mar 03, 2021 at 10:21:01PM -0500, Alan Stern wrote: > > > On Wed, Mar 03, 2021 at 02:03:48PM -0800, Paul E. McKenney wrote: > > > > On Wed, Mar 03, 2021 at

Re: XDP socket rings, and LKMM litmus tests

On Thu, Mar 04, 2021 at 02:33:32PM +0800, Boqun Feng wrote: > Right, I was thinking about something unrelated.. but how about the > following case: > > local_v = > r1 = READ_ONCE(*x); // f > > if (r1 == 1) { > local_v = // e > } else { >

Re: XDP socket rings, and LKMM litmus tests

> On 3 Mar 2021, at 21:22, Alan Stern wrote: > >>> >>> Local variables absolutely should be treated just like CPU registers, if >>> possible. In fact, the compiler has the option of keeping local >>> variables stored in registers. >>> >>> (Of course, things may get complicated if anyone

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 09:04:07PM -0800, Paul E. McKenney wrote: > On Wed, Mar 03, 2021 at 10:21:01PM -0500, Alan Stern wrote: > > On Wed, Mar 03, 2021 at 02:03:48PM -0800, Paul E. McKenney wrote: > > > On Wed, Mar 03, 2021 at 03:22:46PM -0500, Alan Stern wrote: > > > > > And I cannot

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 10:13:22PM -0500, Alan Stern wrote: > On Thu, Mar 04, 2021 at 09:26:31AM +0800, Boqun Feng wrote: > > On Wed, Mar 03, 2021 at 03:22:46PM -0500, Alan Stern wrote: > > > > Which brings us back to the case of the > > > > > > dep ; rfi > > > > > > dependency relation,

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 10:21:01PM -0500, Alan Stern wrote: > On Wed, Mar 03, 2021 at 02:03:48PM -0800, Paul E. McKenney wrote: > > On Wed, Mar 03, 2021 at 03:22:46PM -0500, Alan Stern wrote: > > > On Wed, Mar 03, 2021 at 09:40:22AM -0800, Paul E. McKenney wrote: > > > > On Wed, Mar 03, 2021 at

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 02:03:48PM -0800, Paul E. McKenney wrote: > On Wed, Mar 03, 2021 at 03:22:46PM -0500, Alan Stern wrote: > > On Wed, Mar 03, 2021 at 09:40:22AM -0800, Paul E. McKenney wrote: > > > On Wed, Mar 03, 2021 at 12:12:21PM -0500, Alan Stern wrote: > > > > > > Local variables

Re: XDP socket rings, and LKMM litmus tests

On Thu, Mar 04, 2021 at 09:26:31AM +0800, Boqun Feng wrote: > On Wed, Mar 03, 2021 at 03:22:46PM -0500, Alan Stern wrote: > > Which brings us back to the case of the > > > > dep ; rfi > > > > dependency relation, where the accesses in the middle are plain and > > non-racy. Should the LKMM

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 03:22:46PM -0500, Alan Stern wrote: > On Wed, Mar 03, 2021 at 09:40:22AM -0800, Paul E. McKenney wrote: > > On Wed, Mar 03, 2021 at 12:12:21PM -0500, Alan Stern wrote: > > > > Local variables absolutely should be treated just like CPU registers, if > > > possible. In

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 03:22:46PM -0500, Alan Stern wrote: > On Wed, Mar 03, 2021 at 09:40:22AM -0800, Paul E. McKenney wrote: > > On Wed, Mar 03, 2021 at 12:12:21PM -0500, Alan Stern wrote: > > > > Local variables absolutely should be treated just like CPU registers, if > > > possible. In

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 06:39:14PM +0100, maranget wrote: > > > > On 3 Mar 2021, at 18:37, maranget wrote: > > > > I have made a PR to herd7 that performs the change. The commit message > > states the new definition. > > For those who are interested >

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 06:37:36PM +0100, maranget wrote: > > > > On 3 Mar 2021, at 18:12, Alan Stern wrote: > > > > On Tue, Mar 02, 2021 at 03:50:19PM -0800, Paul E. McKenney wrote: > >> On Tue, Mar 02, 2021 at 04:14:46PM -0500, Alan Stern wrote: > > > >>> This result is wrong, apparently

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 09:40:22AM -0800, Paul E. McKenney wrote: > On Wed, Mar 03, 2021 at 12:12:21PM -0500, Alan Stern wrote: > > Local variables absolutely should be treated just like CPU registers, if > > possible. In fact, the compiler has the option of keeping local > > variables stored

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 12:12:21PM -0500, Alan Stern wrote: > On Tue, Mar 02, 2021 at 03:50:19PM -0800, Paul E. McKenney wrote: > > On Tue, Mar 02, 2021 at 04:14:46PM -0500, Alan Stern wrote: > > > > This result is wrong, apparently because of a bug in herd7. There > > > should be control

Re: XDP socket rings, and LKMM litmus tests

> On 3 Mar 2021, at 18:37, maranget wrote: > > I have made a PR to herd7 that performs the change. The commit message states > the new definition. For those who are interested —Luc

Re: XDP socket rings, and LKMM litmus tests

> On 3 Mar 2021, at 18:12, Alan Stern wrote: > > On Tue, Mar 02, 2021 at 03:50:19PM -0800, Paul E. McKenney wrote: >> On Tue, Mar 02, 2021 at 04:14:46PM -0500, Alan Stern wrote: > >>> This result is wrong, apparently because of a bug in herd7. There >>> should be control dependencies from

Re: XDP socket rings, and LKMM litmus tests

On Tue, Mar 02, 2021 at 03:50:19PM -0800, Paul E. McKenney wrote: > On Tue, Mar 02, 2021 at 04:14:46PM -0500, Alan Stern wrote: > > This result is wrong, apparently because of a bug in herd7. There > > should be control dependencies from each of the two loads in P0 to each > > of the two

Re: XDP socket rings, and LKMM litmus tests

On Wed, Mar 03, 2021 at 07:37:42AM +0100, maranget wrote: > Hi all, > > I agree that herd7 computation of control dependencies is problematic here. > > Thanks for reporting the problem. Paul kindly takes the responsibility for > the problem, but frankly do not remember having followed his

Re: XDP socket rings, and LKMM litmus tests

Hi all, I agree that herd7 computation of control dependencies is problematic here. Thanks for reporting the problem. Paul kindly takes the responsibility for the problem, but frankly do not remember having followed his recommendations here. I am quite busy today and canot really work on the

Re: XDP socket rings, and LKMM litmus tests

On Tue, Mar 02, 2021 at 04:14:46PM -0500, Alan Stern wrote: > On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote: > > Hi! > > > > Firstly; The long Cc-list is to reach the LKMM-folks. > > > > Some background; the XDP sockets use a ring-buffer to communicate > > between the kernel and

Re: XDP socket rings, and LKMM litmus tests

On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote: > Hi! > > Firstly; The long Cc-list is to reach the LKMM-folks. > > Some background; the XDP sockets use a ring-buffer to communicate > between the kernel and userland. It's a > single-consumer/single-producer ring, and described in >

Re: XDP socket rings, and LKMM litmus tests

On Tue, 2 Mar 2021 at 21:41, Paul E. McKenney wrote: > > On Tue, Mar 02, 2021 at 09:24:04PM +0100, Björn Töpel wrote: > > On Tue, 2 Mar 2021 at 20:57, Paul E. McKenney wrote: > > > > > > On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote: > > > > [...] > > > > > > > > Before digging in

Re: XDP socket rings, and LKMM litmus tests

On Tue, 2 Mar 2021 at 21:04, Paul E. McKenney wrote: > [...] > > And if the answer is "yes", how about this one? > With the == to != change in P1, this is OK! > P0(int *prod, int *cons, int *data) > { > int p; > > p = READ_ONCE(*prod); > if (p == READ_ONCE(*cons)) { ...and now

Re: XDP socket rings, and LKMM litmus tests

On Tue, Mar 02, 2021 at 09:24:04PM +0100, Björn Töpel wrote: > On Tue, 2 Mar 2021 at 20:57, Paul E. McKenney wrote: > > > > On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote: > > [...] > > > > > Before digging in too deeply, does the following simplification > > still capture your

Re: XDP socket rings, and LKMM litmus tests

On Tue, 2 Mar 2021 at 20:57, Paul E. McKenney wrote: > > On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote: [...] > > Before digging in too deeply, does the following simplification > still capture your intent? > Thanks for having a look, Paul! > P0(int *prod, int *cons, int *data)

Re: XDP socket rings, and LKMM litmus tests

On Tue, Mar 02, 2021 at 11:57:58AM -0800, Paul E. McKenney wrote: > On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote: > > Hi! > > > > Firstly; The long Cc-list is to reach the LKMM-folks. > > > > Some background; the XDP sockets use a ring-buffer to communicate > > between the kernel

Re: XDP socket rings, and LKMM litmus tests

On Tue, Mar 02, 2021 at 07:46:27PM +0100, Björn Töpel wrote: > Hi! > > Firstly; The long Cc-list is to reach the LKMM-folks. > > Some background; the XDP sockets use a ring-buffer to communicate > between the kernel and userland. It's a > single-consumer/single-producer ring, and described in >

XDP socket rings, and LKMM litmus tests

Hi! Firstly; The long Cc-list is to reach the LKMM-folks. Some background; the XDP sockets use a ring-buffer to communicate between the kernel and userland. It's a single-consumer/single-producer ring, and described in net/xdp/xsk_queue.h. --8<--- /* The structure of the shared state of the