From mboxrd@z Thu Jan 1 00:00:00 1970 From: "Joel Fernandes (Google)" Subject: [PATCH 2/3] LKMM: Add litmus test for RCU GP guarantee where reader stores Date: Fri, 20 Mar 2020 02:55:51 -0400 Message-ID: <20200320065552.253696-2-joel@joelfernandes.org> References: <20200320065552.253696-1-joel@joelfernandes.org> Mime-Version: 1.0 Content-Transfer-Encoding: 8bit Return-path: In-Reply-To: <20200320065552.253696-1-joel@joelfernandes.org> Sender: linux-kernel-owner@vger.kernel.org To: linux-kernel@vger.kernel.org Cc: "Joel Fernandes (Google)" , Akira Yokosawa , Alan Stern , Andrea Parri , Boqun Feng , Daniel Lustig , David Howells , Jade Alglave , linux-arch@vger.kernel.org, Luc Maranget , Nicholas Piggin , "Paul E. McKenney" , Peter Zijlstra , Will Deacon List-Id: linux-arch.vger.kernel.org This adds an example for the important RCU grace period guarantee, which shows an RCU reader can never span a grace period. Signed-off-by: Joel Fernandes (Google) --- .../litmus-tests/RCU+sync+read.litmus | 37 +++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tools/memory-model/litmus-tests/RCU+sync+read.litmus diff --git a/tools/memory-model/litmus-tests/RCU+sync+read.litmus b/tools/memory-model/litmus-tests/RCU+sync+read.litmus new file mode 100644 index 0000000000000..73557772e2a32 --- /dev/null +++ b/tools/memory-model/litmus-tests/RCU+sync+read.litmus @@ -0,0 +1,37 @@ +C RCU+sync+read + +(* + * Result: Never + * + * This litmus test demonstrates that after a grace period, an RCU updater always + * sees all stores done in prior RCU read-side critical sections. Such + * read-side critical sections would have ended before the grace period ended. + * + * This guarantee also implies, an RCU reader can never span a grace period and + * is an important RCU grace period memory ordering guarantee. + *) + +{ +x = 0; +y = 0; +} + +P0(int *x, int *y) +{ + rcu_read_lock(); + WRITE_ONCE(*x, 1); + WRITE_ONCE(*y, 1); + rcu_read_unlock(); +} + +P1(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*x); + synchronize_rcu(); + r1 = READ_ONCE(*y); +} + +exists (1:r0=1 /\ 1:r1=0) -- 2.25.1.696.g5e7596f4ac-goog From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-qv1-f65.google.com ([209.85.219.65]:39108 "EHLO mail-qv1-f65.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1726829AbgCTG4E (ORCPT ); Fri, 20 Mar 2020 02:56:04 -0400 Received: by mail-qv1-f65.google.com with SMTP id v38so2427868qvf.6 for ; Thu, 19 Mar 2020 23:56:02 -0700 (PDT) From: "Joel Fernandes (Google)" Subject: [PATCH 2/3] LKMM: Add litmus test for RCU GP guarantee where reader stores Date: Fri, 20 Mar 2020 02:55:51 -0400 Message-ID: <20200320065552.253696-2-joel@joelfernandes.org> In-Reply-To: <20200320065552.253696-1-joel@joelfernandes.org> References: <20200320065552.253696-1-joel@joelfernandes.org> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit Sender: linux-arch-owner@vger.kernel.org List-ID: To: linux-kernel@vger.kernel.org Cc: "Joel Fernandes (Google)" , Akira Yokosawa , Alan Stern , Andrea Parri , Boqun Feng , Daniel Lustig , David Howells , Jade Alglave , linux-arch@vger.kernel.org, Luc Maranget , Nicholas Piggin , "Paul E. McKenney" , Peter Zijlstra , Will Deacon Message-ID: <20200320065551.aF3_aYIJOr0mx02BizOEGxAU0FQpo2ycWnLlSsPcOSI@z> This adds an example for the important RCU grace period guarantee, which shows an RCU reader can never span a grace period. Signed-off-by: Joel Fernandes (Google) --- .../litmus-tests/RCU+sync+read.litmus | 37 +++++++++++++++++++ 1 file changed, 37 insertions(+) create mode 100644 tools/memory-model/litmus-tests/RCU+sync+read.litmus diff --git a/tools/memory-model/litmus-tests/RCU+sync+read.litmus b/tools/memory-model/litmus-tests/RCU+sync+read.litmus new file mode 100644 index 0000000000000..73557772e2a32 --- /dev/null +++ b/tools/memory-model/litmus-tests/RCU+sync+read.litmus @@ -0,0 +1,37 @@ +C RCU+sync+read + +(* + * Result: Never + * + * This litmus test demonstrates that after a grace period, an RCU updater always + * sees all stores done in prior RCU read-side critical sections. Such + * read-side critical sections would have ended before the grace period ended. + * + * This guarantee also implies, an RCU reader can never span a grace period and + * is an important RCU grace period memory ordering guarantee. + *) + +{ +x = 0; +y = 0; +} + +P0(int *x, int *y) +{ + rcu_read_lock(); + WRITE_ONCE(*x, 1); + WRITE_ONCE(*y, 1); + rcu_read_unlock(); +} + +P1(int *x, int *y) +{ + int r0; + int r1; + + r0 = READ_ONCE(*x); + synchronize_rcu(); + r1 = READ_ONCE(*y); +} + +exists (1:r0=1 /\ 1:r1=0) -- 2.25.1.696.g5e7596f4ac-goog