Received: by 2002:ad5:474a:0:0:0:0:0 with SMTP id i10csp7556869imu; Mon, 3 Dec 2018 15:05:09 -0800 (PST) X-Google-Smtp-Source: AFSGD/VizHQfDB8L5ofNdbPp8W0dBqFlX9sPZIpTgOUqpe/EHUW/GWPssbzxJLniiDTtaoeadgzh X-Received: by 2002:a17:902:622:: with SMTP id 31mr17392440plg.171.1543878309539; Mon, 03 Dec 2018 15:05:09 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1543878309; cv=none; d=google.com; s=arc-20160816; b=H3gZjELSV6zPdXu7Mo1AkyT8aRZelLlesEMlL2JQiLuBDBsdCE/y9L5jtzmhwnOLuM KOqcn3vhURBPTcrYgJdcdQFPVH4kU9hfp8tX7BaXjHKNRUd/tYbl5brm2W2TlaRtELKI cm2B3ovL4wyrz1mu9D+OPOEc87/BGZ1HfwF8ySi2Df9hwqqnd0ECwXCTxNwt6ZW68oz7 nWxGQpWGWGR8CvWkgHyshNYzpfSJtFEeIEvxQdz+Lta8KEdGAFgg97SJ6FYCc6Dw8gYg iGmw2fKVP8BSrYEmdzQCIpftXWJpQ+wj05hTXk3VG4eDHsoEYSoOkq9w8UCcw4zHZ+Jc gLVw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-id:precedence:sender:message-id:user-agent:content-disposition :mime-version:reply-to:subject:cc:to:from:date; bh=YG8XN5ywyY2wlcOC8xvbX9qY1qlf5SRjjptV73J1ahk=; b=BjlovhqQ2kBnXIgZCPGQMOE6wIowbu9qP5cseG/KeRpun8YkOzHmibtRqVdYeuMW+u Zt4Mk2lwunwkrD7nZlQXyNo3b0q2J5WnOaGZX2mV0RM8xPxQ5wIOgbFUHKuiEsyMde+9 3gmSYvpv9BY8joBpfm9Uj2C1jFbJKUho6EnhGSzmG51qkPPks+xkI+j0qEb5mUyPuX2J TSjePeuDOP+huoHFghiVPEDRgJOUotL2qY0skXNL64Ug1A4eb3OHkYP/87nQCO2uHqtd o+qMKXj/SQ56bBeP5Zx1rSUnKs+NB9lEEQvHAy+b0+mXUsbXrh8RYAAWGV0BefXNaQrc UsMQ== 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; dmarc=fail (p=NONE sp=NONE dis=NONE) header.from=ibm.com Return-Path: Received: from vger.kernel.org (vger.kernel.org. [209.132.180.67]) by mx.google.com with ESMTP id a17si12776092pgv.456.2018.12.03.15.04.52; Mon, 03 Dec 2018 15:05:09 -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; 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=fail (p=NONE sp=NONE dis=NONE) header.from=ibm.com Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1725938AbeLCXEQ (ORCPT + 99 others); Mon, 3 Dec 2018 18:04:16 -0500 Received: from mx0b-001b2d01.pphosted.com ([148.163.158.5]:36394 "EHLO mx0a-001b2d01.pphosted.com" rhost-flags-OK-OK-OK-FAIL) by vger.kernel.org with ESMTP id S1725858AbeLCXEQ (ORCPT ); Mon, 3 Dec 2018 18:04:16 -0500 Received: from pps.filterd (m0098417.ppops.net [127.0.0.1]) by mx0a-001b2d01.pphosted.com (8.16.0.22/8.16.0.22) with SMTP id wB3N3n7W082514 for ; Mon, 3 Dec 2018 18:04:14 -0500 Received: from e16.ny.us.ibm.com (e16.ny.us.ibm.com [129.33.205.206]) by mx0a-001b2d01.pphosted.com with ESMTP id 2p5d3m1j2s-1 (version=TLSv1.2 cipher=AES256-GCM-SHA384 bits=256 verify=NOT) for ; Mon, 03 Dec 2018 18:04:14 -0500 Received: from localhost by e16.ny.us.ibm.com with IBM ESMTP SMTP Gateway: Authorized Use Only! Violators will be prosecuted for from ; Mon, 3 Dec 2018 23:04:14 -0000 Received: from b01cxnp22036.gho.pok.ibm.com (9.57.198.26) by e16.ny.us.ibm.com (146.89.104.203) with IBM ESMTP SMTP Gateway: Authorized Use Only! Violators will be prosecuted; (version=TLSv1/SSLv3 cipher=AES256-GCM-SHA384 bits=256/256) Mon, 3 Dec 2018 23:04:09 -0000 Received: from b01ledav003.gho.pok.ibm.com (b01ledav003.gho.pok.ibm.com [9.57.199.108]) by b01cxnp22036.gho.pok.ibm.com (8.14.9/8.14.9/NCO v10.0) with ESMTP id wB3N49Yo15335516 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-GCM-SHA384 bits=256 verify=FAIL); Mon, 3 Dec 2018 23:04:09 GMT Received: from b01ledav003.gho.pok.ibm.com (unknown [127.0.0.1]) by IMSVA (Postfix) with ESMTP id 03011B206A; Mon, 3 Dec 2018 23:04:09 +0000 (GMT) Received: from b01ledav003.gho.pok.ibm.com (unknown [127.0.0.1]) by IMSVA (Postfix) with ESMTP id D85D6B2064; Mon, 3 Dec 2018 23:04:08 +0000 (GMT) Received: from paulmck-ThinkPad-W541 (unknown [9.70.82.38]) by b01ledav003.gho.pok.ibm.com (Postfix) with ESMTP; Mon, 3 Dec 2018 23:04:08 +0000 (GMT) Received: by paulmck-ThinkPad-W541 (Postfix, from userid 1000) id DE7D616C1BF4; Mon, 3 Dec 2018 15:04:11 -0800 (PST) Date: Mon, 3 Dec 2018 15:04:11 -0800 From: "Paul E. McKenney" To: linux-kernel@vger.kernel.org, linux-arch@vger.kernel.org, mingo@kernel.org Cc: 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, akiyks@gmail.com Subject: [PATCH memory-model 0/3] Updates to the formal memory model Reply-To: paulmck@linux.ibm.com MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.5.21 (2010-09-15) X-TM-AS-GCONF: 00 x-cbid: 18120323-0072-0000-0000-000003D36257 X-IBM-SpamModules-Scores: X-IBM-SpamModules-Versions: BY=3.00010166; HX=3.00000242; KW=3.00000007; PH=3.00000004; SC=3.00000270; SDB=6.01126570; UDB=6.00582089; IPR=6.00906705; MB=3.00024430; MTD=3.00000008; XFM=3.00000015; UTC=2018-12-03 23:04:13 X-IBM-AV-DETECTION: SAVI=unused REMOTE=unused XFE=unused x-cbparentid: 18120323-0073-0000-0000-00004A5216AD Message-Id: <20181203230411.GA27476@linux.ibm.com> X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10434:,, definitions=2018-12-03_12:,, signatures=0 X-Proofpoint-Spam-Details: rule=outbound_notspam policy=outbound score=0 priorityscore=1501 malwarescore=0 suspectscore=0 phishscore=0 bulkscore=0 spamscore=0 clxscore=1015 lowpriorityscore=0 mlxscore=0 impostorscore=0 mlxlogscore=762 adultscore=0 classifier=spam adjust=0 reason=mlx scancount=1 engine=8.0.1-1810050000 definitions=main-1812030206 Sender: linux-kernel-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: linux-kernel@vger.kernel.org Hello, Ingo! This series contains updates to the Linux kernel's formal memory model in tools/memory-model. These patches are ready for inclusion into -tip. 1. Model smp_mb__after_unlock_lock(), courtesy of Andrea Parri. 2. Add scripts to check github litmus tests. 3. Make scripts take "-j" abbreviation for "--jobs". There is another series in preparation to model SRCU, but this series requires hot-off-the presses changes to the herd tool that have not yet been released. This SRCU series is therefore targeting the merge window after the upcoming one. People wishing to experiment with the prototype SRCU model may obtain it from my -rcu tree at branch "dev", and use a bleeding-edge herd7 built from https://github.com/herd/herdtools7/, version 7.51+2(dev), which is (commit 10403b24070c) or later. Thanx, Paul ------------------------------------------------------------------------ .gitignore | 1 README | 2 linux-kernel.bell | 3 linux-kernel.cat | 4 - linux-kernel.def | 1 scripts/README | 70 ++++++++++++++++++++++ scripts/checkalllitmus.sh | 53 +++++++---------- scripts/checkghlitmus.sh | 65 ++++++++++++++++++++ scripts/checklitmus.sh | 74 +++-------------------- scripts/checklitmushist.sh | 60 +++++++++++++++++++ scripts/cmplitmushist.sh | 87 +++++++++++++++++++++++++++ scripts/initlitmushist.sh | 68 +++++++++++++++++++++ scripts/judgelitmus.sh | 78 +++++++++++++++++++++++++ scripts/newlitmushist.sh | 61 +++++++++++++++++++ scripts/parseargs.sh | 140 ++++++++++++++++++++++++++++++++++++++++++++- scripts/runlitmushist.sh | 87 +++++++++++++++++++++++++++ 16 files changed, 757 insertions(+), 97 deletions(-)