Received: by 2002:a05:6358:489b:b0:bb:da1:e618 with SMTP id x27csp5163561rwn; Mon, 12 Sep 2022 05:29:30 -0700 (PDT) X-Google-Smtp-Source: AA6agR7OeDnSC2wBhAZ6WKw5V5nQBW1+uFLxbB05pA2SXF8zkqJoTvB2Z2N2jnthoCCCJpAJ2Pd7 X-Received: by 2002:a05:6402:228d:b0:44e:f15e:a841 with SMTP id cw13-20020a056402228d00b0044ef15ea841mr21426587edb.157.1662985770756; Mon, 12 Sep 2022 05:29:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1662985770; cv=none; d=google.com; s=arc-20160816; b=luUYAW0cR5EaZHg7Ac4HYLf7eBnyaUKwQPZdNhSTz9r+bW9OtaLZjXmnmWw6P3GqZm bE+ZvQ71XMzWN3j+/Q0dAlQ3+rWxOX3U939AmxfHCdez4sK8meOnOubkNoo+vN5A4mg3 Y5BCOkjjicQtPXHuq8Av5bZk/4WnKjbWEnPPWR9J8Y21CAlgWhebC0KGbCwgB6XTkcV/ rCakMy7t1/f+T1/MPBl5Xalleg0+AmpExt//F+ZDUlLSCWIrYYzqq2ClLfbnYkv3fBgn 4YpVSSb/xdSQxJdqC50e/EnYSEKPGhAOl6jORKtooUFgqve0peOUOemz6NRjZsLPkFsk 4cWw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:in-reply-to:content-disposition:mime-version :references:message-id:subject:cc:to:from:date; bh=piKzC0vZamW0BPgJ96W8bJxCy9WEOGyNhScTi8Xevjw=; b=dp5y6WG2arFFlK0xOvFXo+SUetALmA9fmTRWblOTXcIlJl9epDMpOQFpB3+ViUKSK9 9XJziDpNIAdjloVQ2H+DXtEVmB20ZiIzKn+Hi5WNdMIsFNfmqr6bZFQwjQTF4PT2J/NO KvuK361LG9+NY+XGpoMTWE+wyhqaZR5916uyn1GKCdhYnMoVcv8GNaA1V0exy7D7AP28 jqv22MJvqxcdsfcTgKggOloIO9t09oHyRG0s4R6I80MOKkyt9vKXqFnDc8fTExUA7/yg JrMEw33vw2OR+EKTkqotxChD5cLWS1yEFR6yBpKieuPqwNwpRFZnJOnya1D0iMD3a8kV 83Ww== ARC-Authentication-Results: i=1; mx.google.com; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Return-Path: Received: from out1.vger.email (out1.vger.email. [2620:137:e000::1:20]) by mx.google.com with ESMTP id jg10-20020a170907970a00b0077d26491aa5si1948412ejc.315.2022.09.12.05.29.02; Mon, 12 Sep 2022 05:29:30 -0700 (PDT) Received-SPF: pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) client-ip=2620:137:e000::1:20; Authentication-Results: mx.google.com; spf=pass (google.com: domain of linux-kernel-owner@vger.kernel.org designates 2620:137:e000::1:20 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S229925AbiILMDW (ORCPT + 99 others); Mon, 12 Sep 2022 08:03:22 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:56176 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S230038AbiILMCx (ORCPT ); Mon, 12 Sep 2022 08:02:53 -0400 Received: from netrider.rowland.org (netrider.rowland.org [192.131.102.5]) by lindbergh.monkeyblade.net (Postfix) with SMTP id 4ACC130546 for ; Mon, 12 Sep 2022 05:02:45 -0700 (PDT) Received: (qmail 565895 invoked by uid 1000); 12 Sep 2022 08:02:43 -0400 Date: Mon, 12 Sep 2022 08:02:43 -0400 From: Alan Stern To: Jonas Oberhauser Cc: Hernan Luis Ponce de Leon , Boqun Feng , Peter Zijlstra , "Paul E. McKenney" , "parri.andrea@gmail.com" , "will@kernel.org" , "npiggin@gmail.com" , "dhowells@redhat.com" , "j.alglave@ucl.ac.uk" , "luc.maranget@inria.fr" , "akiyks@gmail.com" , "dlustig@nvidia.com" , "joel@joelfernandes.org" , "linux-kernel@vger.kernel.org" , "linux-arch@vger.kernel.org" Subject: Re: "Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models" Message-ID: References: <20220826124812.GA3007435@paulmck-ThinkPad-P17-Gen-1> <674d0fda790d4650899e2fcf43894053@huawei.com> <1326fa48d44b4571b436c07ae9f32d83@huawei.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <1326fa48d44b4571b436c07ae9f32d83@huawei.com> X-Spam-Status: No, score=-1.7 required=5.0 tests=BAYES_00, HEADER_FROM_DIFFERENT_DOMAINS,SPF_HELO_PASS,SPF_PASS, T_SCC_BODY_TEXT_LINE autolearn=no autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on lindbergh.monkeyblade.net Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Mon, Sep 12, 2022 at 10:46:38AM +0000, Jonas Oberhauser wrote: > Hi Alan, > > Sorry for the confusion. > > > [...] it's certainly true (in all of these > models) than for any finite number N, there is a feasible execution in which a loop runs for more than N iterations before the termination condition eventually becomes true. > > Indeed; but more interestingly, as the Theorem 5.3 in "making weak memory models fair" states, under certain conditions it suffices to look at graphs where N=1 to decide whether a loop can run forever (despite all writes propagating to all cores eventually) or will always terminate. Cool! > And since herd can generate all such graphs, herd could be extended to make that decision and output it, just like many other tools already do. > > To illuminate this on an example, consider the program sent by Peter earlier: > WRITE_ONCE(foo, 1); while (!READ_ONCE(foo)); > > Without the assumption that fr is prefix finite, the graph with infinitely many reads of thread 2 all reading the initial value (and hence being fr-before the store foo=1) would be allowed. However, the tools used to analyze the qspinlock all assume that fr is prefix finite, and hence that such a graph with infinitely many fr-before events does not exist. Because of that, all of the tools will say that this loop always terminates. > > However, if you change the code into the following: > > WRITE_ONCE(foo, 1); WRITE_ONCE(foo, 0); while (!READ_ONCE(foo)); > > then even under the assumption of fr-prefix-finiteness, the coherence order in which WRITE_ONCE(foo, 1); is overwritten by WRITE_ONCE(foo, 0); of thread 2 would lead to non-terminating behaviors, and these are detected by those tools. Furthermore, if we synchronize the two stores as follows: > > while (! READ_ONCE(bar)) {}; WRITE_ONCE(foo, 1); WRITE_ONCE(foo, 0); smp_store_release(&bar,1); while (!READ_ONCE(foo)); > > then the graphs with that co become prohibited as they all have hb cycles, and the tools again will not detect any liveness violations. But if we go further and relax the release barrier as below > > > while (! READ_ONCE(bar)) {}; WRITE_ONCE(foo, 1); WRITE_ONCE(foo, 0); WRITE_ONCE(bar,1); while (!READ_ONCE(foo)); > > then the hb cycle disappears, and the coherence order in which foo=0 overwrites foo=1 becomes allowed. Again, the tools will detect this and state that thread 2 could be stuck in its while loop forever. Neat stuff; I'll have to think about this. > In each of these cases, the decision can be made by looking for a graph in which the loop is executed for one iteration which reads from foo=0, and checking whether that store is co-maximal. So in some sense this is all that is needed to express the idea that a program can run forever, even though only in some very limited (but common) circumstances, namely that the loop iteration that repeats forever does not create modifications to state that are observed outside the loop. Luckily this is a very common case, so these checks have proven quite useful in practice. > > The same kind of check could be implemented in herd together with either the implicit assumption that fr is prefix finite (like in other tools) or with some special syntax like > > prefix-finite fr | co as fairness > > which hopefully clears up the question below: > > > > From an engineering perspective, I think the only issue is that cat > > > *currently* does not have any syntax for this, > > > Syntax for what? The difference between wmb and mb? > > [...] > > > Thanks for your patience and hoping I explained it more clearly, Yes indeed, thank you very much. Alan