From patchwork Thu Feb 15 15:58:53 2018 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Akira Yokosawa X-Patchwork-Id: 128482 Delivered-To: patch@linaro.org Received: by 10.46.124.24 with SMTP id x24csp1901462ljc; Thu, 15 Feb 2018 07:59:06 -0800 (PST) X-Google-Smtp-Source: AH8x227/TbJ8IxW8DxScAMzLo7hWNI8fRjHUFcQvx6JSsWnaAbWvqnVasedq+CAQE7tcz8p4cbbV X-Received: by 10.99.174.7 with SMTP id q7mr2592698pgf.170.1518710346369; Thu, 15 Feb 2018 07:59:06 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1518710346; cv=none; d=google.com; s=arc-20160816; b=YmOwOqvcYjIYbjigQ/J4/lOm4vLmjmmRyACKg5wHPr/LxcqriU/dDMkpCPbponFYpk Q63+7OHBm1jxWLpZQTWsOJs9HxvChJ6FdtnsL5THjo23D1B1ybABRQmZJFJ9PuQKh6Az Rn+xMQWPplHeysk1jXbC4LLvN6SL2qghR/HOSJMDvhvzZRTuQkQo5pIJB0G+lh1Pl0yY VXB2FMKVA+s4981Rc5cI1b5Waqcv6uRWhibe0A80yEhycmizEQvhtXdI4gEozn3Pa+tp d26Rovl4m1aqM9MNfJyJX6XTKh3+BX7MDtjyEC005zljEL4Y8gR2xCIkihQ/lDCO8wTy eheA== 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=0pRTmMeSrtbI9PlLEXbXlyYSz6JLJL+Z36sISq7J9t0=; b=iGe5YEf0OoZElhxd7HQspuI2UqmPC5bQ0ct6BraEg2kJGcdly1K9Ut7gp6Db7etpL/ SIh5ga9QNmyi91d5HSKft+K26unG7HY+5fRFSCGoNFe/yyVoU+uh1lAttSWxEbhWtYPp Q5GP+ofuf8PoX97H8U/y/vwELjO4O/9zqQyY6mKFAVr1TN8S3g3y2bYZJSOimcLa/J3E sDRvzMYXAPIfM1PhdlUwrVRZEusv78ZKsRUbULl+5kUslcntLQpic3viqyZQ66bc5IRI Z3C3wj1yCwyS3EW5itRwV5XFKWQBU8K/ietbvfSlQtRmNrpp5yrDwu+FkTRNBF5oh/Sc DtPQ== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=fy8sgxC0; 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 97-v6si4948856plc.406.2018.02.15.07.59.06; Thu, 15 Feb 2018 07:59:06 -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=fy8sgxC0; 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 S1425430AbeBOP7D (ORCPT + 28 others); Thu, 15 Feb 2018 10:59:03 -0500 Received: from mail-pg0-f66.google.com ([74.125.83.66]:46465 "EHLO mail-pg0-f66.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1424460AbeBOP7A (ORCPT ); Thu, 15 Feb 2018 10:59:00 -0500 Received: by mail-pg0-f66.google.com with SMTP id a11so57844pgu.13 for ; Thu, 15 Feb 2018 07:59:00 -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=0pRTmMeSrtbI9PlLEXbXlyYSz6JLJL+Z36sISq7J9t0=; b=fy8sgxC0Jj6WeJedEKAg+TrYvpEt0RZ+1UHhzpVkzx/1XYXJA3sQcRXoBjunouxbU3 p23Hq8G65qY0cyCP+RDqI+Ti0CFABCT3rzPplx0Omc3CjwcHmjthM7xdByXrP6r3hNpF /4E/6SBjmHoRUWjyGoF03bp89oJ64BVDUupycXbWOW6hiloaEEVO89Caj7PilYkRoDuM xJfv7sjnNVIQyWy0CGN+QrHHDviAan8XUWqP1V4G6qgz4vp8RkY/din0z9j0SaMa7y3u Y5IOLt0KIbhgqZfkEGDuSSQI1vLFYYkjo29qlZlN6Cd6jzy+Rue7mDJFeZ2vSZ/+ditx 6MLQ== 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=0pRTmMeSrtbI9PlLEXbXlyYSz6JLJL+Z36sISq7J9t0=; b=mxkwyW/E0HzLqhwhpee+H9g9rxQ/lzeWiEows/1nn1SEUMFjPnJ4Gxgb/yTbpM6g/c K5JDcfM9qfVfnDkA+uBum2/Ilpj+rbYi2V2lLS3hIJoVNlmLrdj7PK0/R4inRfm4oEzB uqVUmneYaLOCYJ0BXj9gKSdiaF9kxbFzgJam52Z4qa0xW21rL20CUD0M3ZTcAqVQ9sVl RvJo1/l6TS3PxsJDFBu1XkScQuvyXhewJg/YysKfJSiJzuuIsvT6n0W6IMLIjDLXNydY kh6ZnmMfaDw33/ddfkorzf31Sdsnc/0kM6oFbKECZdua9iEQ/DCmYRlIKHrmLG+/hnOm LWyw== X-Gm-Message-State: APf1xPAHNbySEOqQnl9hMDoPKbL+PjifmpB1b1YbEV3uuFxJfy0JvZ4r bbKn/Jvn3vfbs9lIXg6QyLU= X-Received: by 10.99.112.73 with SMTP id a9mr423500pgn.253.1518710339655; Thu, 15 Feb 2018 07:58:59 -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 y63sm19766977pff.90.2018.02.15.07.58.55 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 15 Feb 2018 07:58:58 -0800 (PST) Subject: Trial of conflict resolution of Alan's patch To: Alan Stern , "Paul E. McKenney" Cc: linux-kernel@vger.kernel.org, mingo@kernel.org, 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, Patrick Bellasi , Akira Yokosawa References: From: Akira Yokosawa Message-ID: Date: Fri, 16 Feb 2018 00:58:53 +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 81bd6374057f0d89894ead482b870e2f001d2998 Mon Sep 17 00:00:00 2001 From: Alan Stern Date: Fri, 16 Feb 2018 00:29:56 +0900 Subject: [PATCH] [TENTATIVE] Trial conflict resolution of Alan's patch This is a trial of conflict resolution of the patch Alan provided. Alan's message and original patch: Here's the relevant patch. It may need some manual adjustment, because it was not made against the files currently in the repository. Alan diff --git a/linux-kernel-hardware.cat b/linux-kernel-hardware.cat Index: memory-model/linux-kernel-hardware.cat =================================================================== --- memory-model.orig/linux-kernel-hardware.cat +++ memory-model/linux-kernel-hardware.cat @@ -31,7 +31,7 @@ let strong-fence = mb | gp (* Release Acquire *) let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] -let rfi-rel-acq = [Release] ; rfi ; [Acquire] +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po (**********************************) (* Fundamental coherence ordering *) @@ -57,13 +57,13 @@ let to-w = rwdep | addrpo | (overwrite & let rdw = po-loc & (fre ; rfe) let detour = po-loc & (coe ; rfe) let rrdep = addr | (dep ; rfi) -let to-r = rrdep | rfi-rel-acq -let fence = strong-fence | wmb | po-rel | rmb | acq-po +let to-r = rrdep +let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int) let ppo = to-r | to-w | fence | rdw | detour (* Happens Before *) let A-cumul(r) = rfe? ; r -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po let rec prop = (overwrite & ext)? ; cumul-fence ; hb* and hb = ppo | rfe | ((hb* ; prop) & int) Index: memory-model/linux-kernel.cat =================================================================== --- memory-model.orig/linux-kernel.cat +++ memory-model/linux-kernel.cat @@ -31,7 +31,7 @@ let strong-fence = mb | gp (* Release Acquire *) let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] -let rfi-rel-acq = [Release] ; rfi ; [Acquire] +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po (**********************************) (* Fundamental coherence ordering *) @@ -54,13 +54,13 @@ let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) let rrdep = addr | (dep ; rfi) -let to-r = rrdep | rfi-rel-acq -let fence = strong-fence | wmb | po-rel | rmb | acq-po +let to-r = rrdep +let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int) let ppo = to-r | to-w | fence (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = rfe? ; r -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po let prop = (overwrite & ext)? ; cumul-fence* ; rfe? (* Signed-off-by: Alan Stern [akiyks: Rebased to current master] Signed-off-by: Akira Yokosawa --- So, I attempted to rebase the patch to current (somewhat old) master of https://github.com/aparri/memory-model. Why? Because the lkmm branch in Paul's -rcu tree doesn't have linux-kernel-hardware.cat. However, after this change, Z6.0+pooncelock+pooncelock+pombonce still has the result "Sometimes". I must have done something wrong in the conflict resolution. Note: I have almost no idea what this patch is doing. I'm just hoping to give a starting point of a discussion. Thanks, Akira -- linux-kernel-hardware.cat | 9 ++++----- linux-kernel.cat | 9 ++++----- 2 files changed, 8 insertions(+), 10 deletions(-) -- 2.7.4 Acked-by: Andrea Parri diff --git a/linux-kernel-hardware.cat b/linux-kernel-hardware.cat index 7768bf7..6c35655 100644 --- a/linux-kernel-hardware.cat +++ b/linux-kernel-hardware.cat @@ -34,7 +34,7 @@ let strong-fence = mb | gp (* Release Acquire *) let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] -let rfi-rel-acq = [Release] ; rfi ; [Acquire] +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po (**********************************) (* Fundamental coherence ordering *) @@ -60,14 +60,13 @@ let to-w = rwdep | addrpo | (overwrite & int) let rdw = po-loc & (fre ; rfe) let detour = po-loc & (coe ; rfe) let rrdep = addr | (dep ; rfi) | rdw -let strong-rrdep = rrdep+ & rb-dep -let to-r = strong-rrdep | rfi-rel-acq -let fence = strong-fence | wmb | po-rel | rmb | acq-po +let to-r = rrdep +let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int) let ppo = (rrdep* ; (to-r | to-w | fence)) | rdw | detour (* Happens Before *) let A-cumul(r) = rfe? ; r -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po let rec prop = (overwrite & ext)? ; cumul-fence ; hb* and hb = ppo | rfe | ((hb* ; prop) & int) diff --git a/linux-kernel.cat b/linux-kernel.cat index 15b7a5d..c6b0752 100644 --- a/linux-kernel.cat +++ b/linux-kernel.cat @@ -39,7 +39,7 @@ let strong-fence = mb | gp (* Release Acquire *) let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] -let rfi-rel-acq = [Release] ; rfi ; [Acquire] +let rel-rf-acq-po = [Release] ; rf ; [Acquire] ; po (**********************************) (* Fundamental coherence ordering *) @@ -62,14 +62,13 @@ let rwdep = (dep | ctrl) ; [W] let overwrite = co | fr let to-w = rwdep | (overwrite & int) let rrdep = addr | (dep ; rfi) -let strong-rrdep = rrdep+ & rb-dep -let to-r = strong-rrdep | rfi-rel-acq -let fence = strong-fence | wmb | po-rel | rmb | acq-po +let to-r = rrdep +let fence = strong-fence | wmb | po-rel | rmb | acq-po | (rel-rf-acq-po & int) let ppo = rrdep* ; (to-r | to-w | fence) (* Propagation: Ordering from release operations and strong fences. *) let A-cumul(r) = rfe? ; r -let cumul-fence = A-cumul(strong-fence | po-rel) | wmb +let cumul-fence = A-cumul(strong-fence | po-rel) | wmb | rel-rf-acq-po let prop = (overwrite & ext)? ; cumul-fence* ; rfe? (*