From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org X-Spam-Level: X-Spam-Status: No, score=-7.5 required=3.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,MAILING_LIST_MULTI,SPF_HELO_NONE, SPF_PASS,USER_AGENT_SANE_1 autolearn=no autolearn_force=no version=3.4.0 Received: from mail.kernel.org (mail.kernel.org [198.145.29.99]) by smtp.lore.kernel.org (Postfix) with ESMTP id 35B94C28CC5 for ; Wed, 3 Mar 2021 11:02:25 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 08E0C64EDF for ; Wed, 3 Mar 2021 11:02:24 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1357290AbhCCKtS (ORCPT ); Wed, 3 Mar 2021 05:49:18 -0500 Received: from mail.kernel.org ([198.145.29.99]:50650 "EHLO mail.kernel.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S232917AbhCBXvL (ORCPT ); Tue, 2 Mar 2021 18:51:11 -0500 Received: by mail.kernel.org (Postfix) with ESMTPSA id 481D864F45; Tue, 2 Mar 2021 23:50:20 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1614729020; bh=mD9oG7Zn/uIeJEBEoZqcRpiShRlD9VUAPEWMowEB/fY=; h=Date:From:To:Cc:Subject:Reply-To:References:In-Reply-To:From; b=R4QCmm//yfC21yKBgDEZF8tbH3abijkWkFXS63v48Ul2N9hT825pjCGZ5hCyVcBnf 5kEVjfcaVlw4K97a1eTXvOn2TmM5rwFQp1juKYb9K5atFDOzcPMXsvv/ijg4SuKMdc 5Xvg7nPO8JoW3+vH10eb86w7rW9RBNS6RcneolnawfC1RS82RiXE7acqSP+GNI7PNw lIpCVcJhztCVQgunQvN2AkyahMLv+kuAzpBFoLeR8VxpaI8EQnWb/39y3z102Ye6cg biwAiKTqe7tApMHLRCB+zrNYjfdg8IQLyyR2Zs+Ycn9D8qH1OSHT1mbAJ/wuwhY8qF E92VipNgz/lUw== Received: by paulmck-ThinkPad-P72.home (Postfix, from userid 1000) id DF3183522829; Tue, 2 Mar 2021 15:50:19 -0800 (PST) Date: Tue, 2 Mar 2021 15:50:19 -0800 From: "Paul E. McKenney" To: Alan Stern Cc: =?iso-8859-1?Q?Bj=F6rn_T=F6pel?= , bpf , LKML , parri.andrea@gmail.com, Will Deacon , Peter Zijlstra , boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, akiyks@gmail.com, dlustig@nvidia.com, joel@joelfernandes.org, Toke =?iso-8859-1?Q?H=F8iland-J=F8rgensen?= , "Karlsson, Magnus" Subject: Re: XDP socket rings, and LKMM litmus tests Message-ID: <20210302235019.GT2696@paulmck-ThinkPad-P72> Reply-To: paulmck@kernel.org References: <20210302211446.GA1541641@rowland.harvard.edu> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <20210302211446.GA1541641@rowland.harvard.edu> User-Agent: Mutt/1.9.4 (2018-02-28) Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org 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 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 rings are the same as the > > * ring buffer in kernel/events/ring_buffer.c. For the Rx and completion > > * ring, the kernel is the producer and user space is the consumer. For > > * the Tx and fill rings, the kernel is the consumer and user space is > > * the producer. > > * > > * producer consumer > > * > > * if (LOAD ->consumer) { LOAD ->producer > > * (A) smp_rmb() (C) > > * STORE $data LOAD $data > > * smp_wmb() (B) smp_mb() (D) > > * STORE ->producer STORE ->consumer > > * } > > * > > * (A) pairs with (D), and (B) pairs with (C). > > ... > > -->8--- > > > > I'd like to replace the smp_{r,w,}mb() barriers with acquire-release > > semantics [1], without breaking existing userspace applications. > > > > So, I figured I'd use herd7 and the LKMM model to build a litmus test > > for the barrier version, then for the acquire-release version, and > > finally permutations of both. > > > > The idea is to use a one element ring, with a state machine outlined > > in the litmus test. > > > > The basic test for the existing smp_{r,w,}mb() barriers looks like: > > > > $ cat spsc-rb+1p1c.litmus > > C spsc-rb+1p1c > > > > // Stupid one entry ring: > > // prod cons allowed action prod cons > > // 0 0 => prod => 1 0 > > // 0 1 => cons => 0 0 > > // 1 0 => cons => 1 1 > > // 1 1 => prod => 0 1 > > > > { prod = 1; } > > > > // Here, we start at prod==1,cons==0, data==0, i.e. producer has > > // written data=0, so from here only the consumer can start, and should > > // consume data==0. Afterwards, producer can continue and write 1 to > > // data. Can we enter state prod==0, cons==1, but consumer observerd > > // the write of 1? > > > > P0(int *prod, int *cons, int *data) > > { > > int p; > > int c; > > int cond = 0; > > > > p = READ_ONCE(*prod); > > c = READ_ONCE(*cons); > > if (p == 0) > > if (c == 0) > > cond = 1; > > if (p == 1) > > if (c == 1) > > cond = 1; > > > > if (cond) { > > smp_mb(); > > WRITE_ONCE(*data, 1); > > smp_wmb(); > > WRITE_ONCE(*prod, p ^ 1); > > } > > } > > > > P1(int *prod, int *cons, int *data) > > { > > int p; > > int c; > > int d = -1; > > int cond = 0; > > > > p = READ_ONCE(*prod); > > c = READ_ONCE(*cons); > > if (p == 1) > > if (c == 0) > > cond = 1; > > if (p == 0) > > if (c == 1) > > cond = 1; > > > > if (cond == 1) { > > smp_rmb(); > > d = READ_ONCE(*data); > > smp_mb(); > > WRITE_ONCE(*cons, c ^ 1); > > } > > } > > > > exists( 1:d=1 /\ prod=0 /\ cons=1 ); > > > > -- > > > > The weird state changing if-statements is because that I didn't get > > '&&' and '||' to work with herd. > > > > When this is run: > > > > $ herd7 -conf linux-kernel.cfg litmus-tests/spsc-rb+1p1c.litmus > > Test spsc-rb+1p1c Allowed > > States 2 > > 1:d=0; cons=1; prod=0; > > 1:d=0; cons=1; prod=1; > > No > > Witnesses > > Positive: 0 Negative: 2 > > Condition exists (1:d=1 /\ prod=0 /\ cons=1) > > Observation spsc-rb+1p1c Never 0 2 > > Time spsc-rb+1p1c 0.04 > > Hash=b399756d6a1301ca5bda042f32130791 > > > > Now to my question; In P0 there's an smp_mb(). Without that, the d==1 > > can be observed from P1 (consumer): > > > > $ herd7 -conf linux-kernel.cfg litmus-tests/spsc-rb+1p1c.litmus > > Test spsc-rb+1p1c Allowed > > States 3 > > 1:d=0; cons=1; prod=0; > > 1:d=0; cons=1; prod=1; > > 1:d=1; cons=1; prod=0; > > Ok > > Witnesses > > Positive: 1 Negative: 2 > > Condition exists (1:d=1 /\ prod=0 /\ cons=1) > > Observation spsc-rb+1p1c Sometimes 1 2 > > Time spsc-rb+1p1c 0.04 > > Hash=0047fc21fa77da9a9aee15e35ec367ef > > 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 stores, but herd7 doesn't detect them. > > Maybe Luc can find some time to check whether this really is a bug and > if it is, fix it. I agree that herd7's control dependency tracking could be improved. But sadly, it is currently doing exactly what I asked Luc to make it do, which is to confine the control dependency to its "if" statement. But as usual I wasn't thinking globally enough. And I am not exactly sure what to ask for. Here a store to a local was control-dependency ordered after a read, and so that should propagate to a read from that local variable. Maybe treat local variables as if they were registers, so that from herd7's viewpoint the READ_ONCE()s are able to head control-dependency chains in multiple "if" statements? Thoughts? Thanx, Paul > > In commit c7f2e3cd6c1f ("perf: Optimize ring-buffer write by depending > > on control dependencies") removes the corresponding smp_mb(), and also > > the circular buffer in circular-buffers.txt (pre commit 6c43c091bdc5 > > ("documentation: Update circular buffer for > > load-acquire/store-release")) is missing the smp_mb() at the > > producer-side. > > > > I'm trying to wrap my head around why it's OK to remove the smp_mb() > > in the cases above? I'm worried that the current XDP socket ring > > implementation (which is missing smp_mb()) might be broken. > > Because of the control dependencies, the smp_mb isn't needed. The > dependencies will order both of the stores after both of the loads. > > Alan Stern