Received: by 2002:ac0:a5a6:0:0:0:0:0 with SMTP id m35-v6csp586722imm; Fri, 31 Aug 2018 08:05:23 -0700 (PDT) X-Google-Smtp-Source: ANB0VdbREnh+BGNm2e2ZSOotyhxRG4NaNmOb6BLnSTEaRmN60ZenHm+XF29O8YKHikvwDIpJ5y7d X-Received: by 2002:a17:902:654b:: with SMTP id d11-v6mr15807893pln.8.1535727923802; Fri, 31 Aug 2018 08:05:23 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1535727923; cv=none; d=google.com; s=arc-20160816; b=wUKiHe9wkJdigD4BF5w9v76nQNIMK/aSlt6XZ2ltswUf7NMhO/IsJsd3syS09Ufhnw 21pI/XIeSqOOLHsQIsmLpNNH1YfPyCV0Y3LRJoIrGPf4nX6zWOfqQBiFwyRsHSxlAT9w 7Jdw1s9K23gHoMZqXOkciYKhu65toEFP/FsVWhGLG+XWboR0Hik+n5mKxRJQUb3lECgD PBMXw9Kghrh93Tv4TjKkUbe5QgiJNyE+ON6Z4boxw+4VxO4WpEypR0rrFiPtweXU1KGj DdzZ3ptZrRByhHWk618/NUFzOXIgf0UXXOibQYhBg/fjpAxKQMYoYuT39ZUpBJLfkX+f +tAA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:sender:mime-version:message-id:in-reply-to :subject:cc:to:from:date:arc-authentication-results; bh=KRq7C7jfLlLIzAH6JzgNSj0dLTiDWgkz7gsYf1fNI08=; b=G5NCIGoUUwqd5gHanoN4MD+tmw7JlpLiwIZuydTDjxon3MP/YclrR9SUiJmhkxLnWl u9eaYj4U0kEcnDbA5w8nlLgLsq5/ucWrj0SpgG1U+IsCEALyHmOwiRhWXKrnCaRCm2Cw 6iDc6r1CO+EvKNeMo+Nnl2N2rP4rvcn6MfMEl8caMWQKHLSjFIVb7BVox8PBZkG2AYIl rwE9HNnKAMPfbKO+DGz4X/tLjMRBOM3ab2ZbSf1t85poAPLM7DT8aYzFHy1I10gp0eTs xg77O7RKCCeoLbS2JjF8dgruLDlQFnt5HXSnjIfJXqRoqUOB5WNOSteGc/LC4KaugXmb om/w== ARC-Authentication-Results: i=1; mx.google.com; spf=pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Return-Path: Received: from vger.kernel.org (vger.kernel.org. [209.132.180.67]) by mx.google.com with ESMTP id m18-v6si9645929pgb.136.2018.08.31.08.05.08; Fri, 31 Aug 2018 08:05:23 -0700 (PDT) Received-SPF: pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) client-ip=209.132.180.67; Authentication-Results: mx.google.com; spf=pass (google.com: best guess record for domain of linux-kernel-owner@vger.kernel.org designates 209.132.180.67 as permitted sender) smtp.mailfrom=linux-kernel-owner@vger.kernel.org Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1728370AbeHaTAq (ORCPT + 99 others); Fri, 31 Aug 2018 15:00:46 -0400 Received: from netrider.rowland.org ([192.131.102.5]:57689 "HELO netrider.rowland.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with SMTP id S1727990AbeHaTAq (ORCPT ); Fri, 31 Aug 2018 15:00:46 -0400 Received: (qmail 9454 invoked by uid 500); 31 Aug 2018 10:52:54 -0400 Received: from localhost (sendmail-bs@127.0.0.1) by localhost with SMTP; 31 Aug 2018 10:52:54 -0400 Date: Fri, 31 Aug 2018 10:52:54 -0400 (EDT) From: Alan Stern X-X-Sender: stern@netrider.rowland.org To: Andrea Parri cc: "Paul E. McKenney" , , , , , , , , , , , Subject: Re: [PATCH RFC LKMM 1/7] tools/memory-model: Add extra ordering for locks and remove it for ordinary release/acquire In-Reply-To: <20180831091641.GA3634@andrea> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: linux-kernel-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org On Fri, 31 Aug 2018, Andrea Parri wrote: > On Thu, Aug 30, 2018 at 05:31:32PM -0400, Alan Stern wrote: > > On Thu, 30 Aug 2018, Andrea Parri wrote: > > > > > > All the architectures supported by the Linux kernel (including RISC-V) > > > > do provide this ordering for locks, albeit for varying reasons. > > > > Therefore this patch changes the model in accordance with the > > > > developers' wishes. > > > > > > > > Signed-off-by: Alan Stern > > > > Signed-off-by: Paul E. McKenney > > > > Reviewed-by: Will Deacon > > > > Acked-by: Peter Zijlstra (Intel) > > > > > > Round 2 ;-), I guess... Let me start from the uncontroversial points: > > > > > > 1) being able to use the LKMM to reason about generic locking code > > > is useful and desirable (paraphrasing Peter in [1]); > > > > > > 2) strengthening the ordering requirements of such code isn't going > > > to boost performance (that's "real maths"). > > > > > > This patch is taking (1) away from us and it is formalizing (2), with > > > almost _no_ reason (no reason at all, if we stick to the commit msg.). > > > > That's not quite fair. Generic code isn't always universally > > applicable; some of it is opt-in -- meant only for the architectures > > that can support it. In general, the LKMM allows us to reason about > > higher abstractions (such as locking) at a higher level, without > > necessarily being able to verify the architecture-specific details of > > the implementations. > > No, generic code is "universally applicable" by definition; see below > for more on this point. Then perhaps we should be talking about "partially generic" code; i.e., code that applies to many but not all architectures. > > > In [2], Will wrote: > > > > > > "[...] having them [the RMWs] closer to RCsc[/to the semantics of > > > locks] would make it easier to implement and reason about generic > > > locking implementations (i.e. reduce the number of special ordering > > > cases and/or magic barrier macros)" > > > > > > "magic barrier macros" as in "mmh, if we accept this patch, we _should_ > > > be auditing the various implementations/code to decide where to place a > > > > > > smp_barrier_promote_ordinary_release_acquire_to_unlock_lock()" ;-) > > > > > > or the like, and "special ordering cases" as in "arrgh, (otherwise) we > > > are forced to reason on a per-arch basis while looking at generic code". > > > > Currently the LKMM does not permit architecture-specific reasoning. It > > would have to be extended (in a different way for each architecture) > > first. > > Completely agreed; that's why I said that this patch is detrimental to > the applicability of the LKMM... This ignores the attitude of the kernel developers who want locking to have the stronger RCtso semantics. From their point of view, the patch enhances the LKMM's applicability. > > For example, one could use herd's POWER model combined with the POWER > > compilation scheme and the POWER-specific implementation of spinlocks > > for such reasoning. The LKMM alone is not sufficient. > > > > Sure, programming and reasoning about the kernel would be easier if all > > architectures were the same. Unfortunately, we (and the kernel) have > > to live in the real world. > > > > > (Remark: ordinary release/acquire are building blocks for code such as > > > qspinlock, (q)rwlock, mutex, rwsem, ... and what else??). > > > > But are these building blocks used the same way for all architectures? > > The more, the better! (because then we have the LKMM tools) > > We already discussed the "fast path" example: the fast paths of the > above all resemble: > > *_lock(s): atomic_cmpxchg_acquire(&s->val, UNLOCKED_VAL, LOCKED_VAL) ... > *_unlock(s): ... atomic_set_release(&s->val, UNLOCKED_VAL) > > When I read this code, I think "Of course." (unless some arch. has > messed the implementation of cmpxchg_* up, which can happen...); but > then I read the subject line of this patch and I think "Wait, what?". > > You can argue that this is not generic code, sure; but why on Earth > would you like to do so?! Because the code might not work! On RISC-V, for example, the implementation of ordinary release/acquire is currently not as strong as atomic release/acquire. Yes, it's true that implementing locks with atomic_cmpxchg_acquire should be correct on all existing architectures. And Paul has invited a patch to modify the LKMM accordingly. If you feel that such a change would be a useful enhancement to the LKMM's applicability, please write it. Alan