>From aafc555fe798bcf3c65d0092ca5c8b2d4f6880d3 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Wed, 31 Oct 2018 07:40:45 +0900
Subject: [PATCH 2/8] CodeSamples/formal: Add C-RCU-remove.litmus
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
CodeSamples/formal/herd/C-RCU-remove.litmus | 27 +++++++++++++++++++++++++++
1 file changed, 27 insertions(+)
create mode 100644 CodeSamples/formal/herd/C-RCU-remove.litmus
diff --git a/CodeSamples/formal/herd/C-RCU-remove.litmus b/CodeSamples/formal/herd/C-RCU-remove.litmus
new file mode 100644
index 0000000..0dc806e
--- /dev/null
+++ b/CodeSamples/formal/herd/C-RCU-remove.litmus
@@ -0,0 +1,27 @@
+C C-RCU-remove
+//\begin[snippet][labelbase=ln:formal:C-RCU-remove:whole,commandchars=\\\@\$]
+
+{
+ int *z=1; (* \lnlbl[tail:2] *)
+ int *y=2; (* \lnlbl[tail:1] *)
+ int *x=y; (* \lnlbl[head] *)
+}
+
+P0(int *x, int *y, int *z) //\lnlbl[P0start]
+{
+ rcu_assign_pointer(*x, z); //\lnlbl[assignnewtail]
+ synchronize_rcu(); //\lnlbl[sync]
+ WRITE_ONCE(*y, 0); //\lnlbl[free]
+} //\lnlbl[P0end]
+
+P1(int *x, int *y, int *z) //\lnlbl[P1start]
+{
+ rcu_read_lock(); //\lnlbl[rl]
+ r1 = rcu_dereference(*x); //\lnlbl[rderef]
+ r2 = READ_ONCE(*r1); //\lnlbl[read]
+ rcu_read_unlock(); //\lnlbl[rul]
+} //\lnlbl[P1end]
+
+//\end[snippet][locationslabel=locations_,existslabel=exists_]
+locations [0:r1; 1:r1; x; y; z]
+exists (1:r2=0)
--
2.7.4
