From patchwork Fri Feb 9 23:46:25 2018 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Akira Yokosawa X-Patchwork-Id: 127883 Delivered-To: patch@linaro.org Received: by 10.46.124.24 with SMTP id x24csp1090330ljc; Fri, 9 Feb 2018 15:46:34 -0800 (PST) X-Google-Smtp-Source: AH8x224pftrmEJzPfmHhH6fcBFSw9RX/ErK9imNPwG8RTGdrLmwVT/V2UP2DGSmLxrtMkaVyQIR0 X-Received: by 2002:a17:902:402:: with SMTP id 2-v6mr3923768ple.353.1518219993886; Fri, 09 Feb 2018 15:46:33 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1518219993; cv=none; d=google.com; s=arc-20160816; b=VOmW18qWq/Mmlvn2mRCZmmxRnX/GwWvEa2dMRxeaYJ5VVmH+k397cMThoLTsYalA4t Leo24c1pm39FCQIJro5a0FiFc6ehcQDL0+UMgn6PUJ3dnLVKSxGQqSKiDkOQpK8Y3KJL 8dXK1hSrotXWJImfalv/TAq7nrvS3mU3UB6Eb/1Gd1GvkMhm4v5wbKb33iaCUYzwBYTT 09dmSWCJbYO6UqJNeRs5mMTfeMN2rdZv1A2Rv+Sjg2BFRTIS+ZszZtjvGul+41ZWjkUI xTuDP/e7n3lrESy4FJMkyl0IecaEGKc1hcdGqC9qM9ZULrE8iE5HKV5eMK8RR+EgH6Em /bIQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:sender:content-transfer-encoding :content-language:in-reply-to:mime-version:user-agent:date :message-id:from:references:cc:to:subject:dkim-signature :arc-authentication-results; bh=Aw734cYytgp7B3d20ZXAsXCr8kYh15BwyF2XEZvIRf8=; b=jXJdsuS7DpfWwjyLFwBJ2rnLeCEFCdTOTCql4PRTtTN8hNvUWjGm/dqsjSFTlT1Iwk HnouDgsEho1NXumhopLBuzGwmqORaa7zdpPfRXabMsoYYMvKiJeAAXFXJYVySQJY87EM /6/IeBnR18mFtHkCh15gKBChQx1rJFZr45NA/DcLTq8FJp/EAaBQDoyT8YE4iSvpfqS+ r2Ki8yPgXUiJKA3SS0qASndQFNLZAHBekDrT/5/ecy0867FbIzzV0kkIILl4Pbe0NTdY VN1QGc3eINPiiCZwmeyjQma2LaffAHbTWA7CBPDZkK+/0vnx1kVGxSRLADdhGQxkl9uH ATOw== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ADadyBIk; 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; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Return-Path: Received: from vger.kernel.org (vger.kernel.org. [209.132.180.67]) by mx.google.com with ESMTP id i187si578081pfc.90.2018.02.09.15.46.33; Fri, 09 Feb 2018 15:46:33 -0800 (PST) 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; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ADadyBIk; 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; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1753287AbeBIXqb (ORCPT + 18 others); Fri, 9 Feb 2018 18:46:31 -0500 Received: from mail-io0-f195.google.com ([209.85.223.195]:41830 "EHLO mail-io0-f195.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1753196AbeBIXqa (ORCPT ); Fri, 9 Feb 2018 18:46:30 -0500 Received: by mail-io0-f195.google.com with SMTP id f4so11474031ioh.8 for ; Fri, 09 Feb 2018 15:46:30 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=subject:to:cc:references:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding; bh=Aw734cYytgp7B3d20ZXAsXCr8kYh15BwyF2XEZvIRf8=; b=ADadyBIkC7WmAV1/W+4nh82CGMhBl1MZIcqxANLDPyYqPNUWZO90uW9qjOxrojldTk CXW7z4c1LtuVkZdNTeTv6a8NQy101y4RLlB5OrUAMOkim90Cgg0qnBYB7+CmHD1QpLRO f50XhyEMvsM5mf8jiqv/p1icZ1Bb8evDs7noF500hNMZ0/2MMWgQcGk+eRDAPau+dwa+ oXG8EQp7p9prlTqP40TtPvK+1OCdF3NNUhFVTBOToOKpWbjVTp1TIsww4/14rPxLc2TH R/4ONonkgKdj2PXVK1GmJ+ddmzHAhfLqsYgPm9tSAqgRZ/Gs4aadbldsLJQnL0kwbN2a ZS4A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:subject:to:cc:references:from:message-id:date :user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding; bh=Aw734cYytgp7B3d20ZXAsXCr8kYh15BwyF2XEZvIRf8=; b=p88yMym0beSyQHhvgHOhi+jc4kCP3fB7dN/k6pPzTKGme5TaEQVgh7Aezdp9ItYGpK 7dcPNPpVk+kN/s1jJ2HJ6IQP0Ow1tM+lzNKGCd3gYN0iQgAefpDCSSR3ZIqAprOZYyWJ xfmpmIkAbv1wVd8zT4LrdA39c45ntujnT6FHDGR/Khi83OCnEmglr93TO1FefjLTgN6V 6vQyBkzSuXDWQuXuzM4GX/3unhfvyKRQXdIzEke920ji7o8Z5d557O0ui4sCAWIIQ8sP /YUPqXvxNsTQFyxluwv8Vgn+mwIpWTJwOOIpcSp3XOQJZV+SKwcQtiTSqtUIAb8Td0nY hrhA== X-Gm-Message-State: APf1xPBLBH05SgpcXg3I5On1nC8IFsbUPJdpYSFUmXsckbdhaTQQOXBv hVwNJ3UxK+qzOQwcwY6RfaU= X-Received: by 10.107.44.68 with SMTP id s65mr4943988ios.172.1518219989977; Fri, 09 Feb 2018 15:46:29 -0800 (PST) Received: from [192.168.11.4] (KD106167171201.ppp-bb.dion.ne.jp. [106.167.171.201]) by smtp.gmail.com with ESMTPSA id k5sm4034533ioe.59.2018.02.09.15.46.25 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 09 Feb 2018 15:46:29 -0800 (PST) Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") To: paulmck@linux.vnet.ibm.com, linux-kernel@vger.kernel.org Cc: mingo@kernel.org, stern@rowland.harvard.edu, parri.andrea@gmail.com, will.deacon@arm.com, peterz@infradead.org, boqun.feng@gmail.com, npiggin@gmail.com, dhowells@redhat.com, j.alglave@ucl.ac.uk, luc.maranget@inria.fr, Akira Yokosawa , Patrick Bellasi References: <20180209141832.GA17505@linux.vnet.ibm.com> From: Akira Yokosawa Message-ID: Date: Sat, 10 Feb 2018 08:46:25 +0900 User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:52.0) Gecko/20100101 Thunderbird/52.6.0 MIME-Version: 1.0 In-Reply-To: Content-Language: en-US Sender: linux-kernel-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org >From 7c1f497a9a51e8db1a94c8a7ef0b74b235aaab88 Mon Sep 17 00:00:00 2001 From: Akira Yokosawa Date: Fri, 9 Feb 2018 04:51:05 -0800 Subject: [PATCH v2] tools/memory-model: Make compat with herd7 7.47 ("-" -> "_") As of herd7 7.47, these '-'s are not permitted and end up in errors such as: File "./linux-kernel.def", line 44, characters 29-30: unexpected '-' (in macros) Partial revert of commit 2d5fba7782d6 ("linux-kernel*: Make RCU identifiers match ASPLOS paper") in the repository at https://github.com/aparri/memory-model can restore the compatibility with herd7 7.47. Reported-by: Patrick Bellasi Suggested-by: Andrea Parri Signed-off-by: Akira Yokosawa --- Paul, FWIW, this is a squashed version relative to patch 07/10 in the RFC series. Thanks, Akira -- tools/memory-model/linux-kernel.bell | 14 +++++++------- tools/memory-model/linux-kernel.cat | 2 +- tools/memory-model/linux-kernel.def | 8 ++++---- 3 files changed, 12 insertions(+), 12 deletions(-) -- 2.7.4 diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index b984bbd..436791b 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -25,9 +25,9 @@ enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || 'mb (*smp_mb*) || 'rb_dep (*smp_read_barrier_depends*) || - 'rcu-lock (*rcu_read_lock*) || - 'rcu-unlock (*rcu_read_unlock*) || - 'sync-rcu (*synchronize_rcu*) || + 'rcu_lock (*rcu_read_lock*) || + 'rcu_unlock (*rcu_read_unlock*) || + 'sync_rcu (*synchronize_rcu*) || 'before_atomic (*smp_mb__before_atomic*) || 'after_atomic (*smp_mb__after_atomic*) || 'after_spinlock (*smp_mb__after_spinlock*) @@ -35,8 +35,8 @@ instructions F[Barriers] (* Compute matching pairs of nested Rcu-lock and Rcu-unlock *) let matched = let rec - unmatched-locks = Rcu-lock \ domain(matched) - and unmatched-unlocks = Rcu-unlock \ range(matched) + unmatched-locks = Rcu_lock \ domain(matched) + and unmatched-unlocks = Rcu_unlock \ range(matched) and unmatched = unmatched-locks | unmatched-unlocks and unmatched-po = [unmatched] ; po ; [unmatched] and unmatched-locks-to-unlocks = @@ -46,8 +46,8 @@ let matched = let rec in matched (* Validate nesting *) -flag ~empty Rcu-lock \ domain(matched) as unbalanced-rcu-locking -flag ~empty Rcu-unlock \ range(matched) as unbalanced-rcu-locking +flag ~empty Rcu_lock \ domain(matched) as unbalanced-rcu-locking +flag ~empty Rcu_unlock \ range(matched) as unbalanced-rcu-locking (* Outermost level of nesting only *) let crit = matched \ (po^-1 ; matched ; po^-1) diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index babe2b3..d0085d5 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -32,7 +32,7 @@ let mb = ([M] ; fencerel(Mb) ; [M]) | ([M] ; fencerel(Before_atomic) ; [RMW] ; po? ; [M]) | ([M] ; po? ; [RMW] ; fencerel(After_atomic) ; [M]) | ([M] ; po? ; [LKW] ; fencerel(After_spinlock) ; [M]) -let gp = po ; [Sync-rcu] ; po? +let gp = po ; [Sync_rcu] ; po? let strong-fence = mb | gp diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index a397387..fc08371 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -41,10 +41,10 @@ spin_unlock(X) { __unlock(X) ; } spin_trylock(X) __trylock(X) // RCU -rcu_read_lock() { __fence{rcu-lock}; } -rcu_read_unlock() { __fence{rcu-unlock};} -synchronize_rcu() { __fence{sync-rcu}; } -synchronize_rcu_expedited() { __fence{sync-rcu}; } +rcu_read_lock() { __fence{rcu_lock}; } +rcu_read_unlock() { __fence{rcu_unlock};} +synchronize_rcu() { __fence{sync_rcu}; } +synchronize_rcu_expedited() { __fence{sync_rcu}; } // Atomic atomic_read(X) READ_ONCE(*X)