>From d724a9b7ffb4b6d648290864c80cd1542297fa40 Mon Sep 17 00:00:00 2001
From: Akira Yokosawa <akiyks@xxxxxxxxx>
Date: Mon, 10 Dec 2018 20:39:28 +0900
Subject: [PATCH 1/4] CodeSamples: Add C-cmpxchg.litmus
Signed-off-by: Akira Yokosawa <akiyks@xxxxxxxxx>
---
CodeSamples/formal/litmus/C-cmpxchg.litmus | 24 ++++++++++++++++++++++++
1 file changed, 24 insertions(+)
create mode 100644 CodeSamples/formal/litmus/C-cmpxchg.litmus
diff --git a/CodeSamples/formal/litmus/C-cmpxchg.litmus b/CodeSamples/formal/litmus/C-cmpxchg.litmus
new file mode 100644
index 0000000..9579d4a
--- /dev/null
+++ b/CodeSamples/formal/litmus/C-cmpxchg.litmus
@@ -0,0 +1,24 @@
+C C-cmpxchg
+{
+}
+
+{
+#include "api.h"
+}
+
+P0(int *x)
+{
+ int r1;
+
+ r1 = cmpxchg(x, 1, 2);
+}
+
+P1(int *x)
+{
+ int r1;
+
+ r1 = cmpxchg(x, 0, 1);
+}
+
+locations [1:r1]
+exists (0:r1=1 /\ ~x=2)
--
2.7.4
