>From 892d8e1014c5bca1c83fbc35bcc1951c6c497b7f Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Mon, 17 Jul 2017 20:56:19 +0900
Subject: [RFC PATCH] advsync: Add litmus tests of control dependency
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
Hi Paul,
So I converted the 2 examples of control dependency to litmus tests.
I mentioned the name "C-SB+o-c-o+o-c-o", but it should have been
"C-LB+o-c-o+o-c-o".
They correspond to the example after the partial revert to the
two-CPU example I submitted earlier.
Do they make sense?
Thanks, Akira
--
CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus | 27 ++++++++++++++++++
.../advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus | 32 ++++++++++++++++++++++
2 files changed, 59 insertions(+)
create mode 100644 CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
create mode 100644 CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
diff --git a/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus b/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
new file mode 100644
index 0000000..023af2e
--- /dev/null
+++ b/CodeSamples/advsync/herd/C-LB+o-c-o+o-c-o.litmus
@@ -0,0 +1,27 @@
+C C-LB+o-c-o+o-c-o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 >= 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 >= 0)
+ WRITE_ONCE(*x, 1);
+}
+
+exists (0:r1=1 /\ 1:r2=1)
diff --git a/CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus b/CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
new file mode 100644
index 0000000..80dc2f6
--- /dev/null
+++ b/CodeSamples/advsync/herd/C-WWC+o-c-o+o-c-o+o.litmus
@@ -0,0 +1,32 @@
+C C-WWC+o-c-o+o-c-o+o
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x, int *y)
+{
+ int r1;
+
+ r1 = READ_ONCE(*x);
+ if (r1 >= 0)
+ WRITE_ONCE(*y, 1);
+}
+
+P1(int *x, int *y)
+{
+ int r2;
+
+ r2 = READ_ONCE(*y);
+ if (r2 >= 0)
+ WRITE_ONCE(*x, 1);
+}
+
+P2(int *x)
+{
+ WRITE_ONCE(*x, 2);
+}
+
+exists (0:r1=2 /\ 1:r2=1 /\ x=2)
--
2.7.4
--
To unsubscribe from this list: send the line "unsubscribe perfbook" in
the body of a message to majordomo@xxxxxxxxxxxxxxx
More majordomo info at http://vger.kernel.org/majordomo-info.html
