[pypy-commit] stmgc c7: Use checkfence to check a particular lockfree subalgorithm used in c7/core.c

[arigo]

Author: Armin Rigo <arigo at tunes.org>
Branch: c7
Changeset: r599:09c6e26a06fe
Date: 2014-01-04 16:30 +0100
http://bitbucket.org/pypy/stmgc/changeset/09c6e26a06fe/

Log:	Use checkfence to check a particular lockfree subalgorithm used in
	c7/core.c

diff --git a/checkfence/c7/run b/checkfence/c7/run
new file mode 100755
--- /dev/null
+++ b/checkfence/c7/run
@@ -0,0 +1,11 @@
+#!/bin/sh
+
+export C2LSL_HOME=./c2lsl
+export CHECKFENCE_HOME=./checkfence
+
+
+$C2LSL_HOME/bin/c2lsl.exe "$1" _run.lsl || exit 1
+shift
+$CHECKFENCE_HOME/run/clean || exit 1
+echo -------------------------------------------------------------------------
+$CHECKFENCE_HOME/run/checkfence -i _run.lsl "$@" || exit 1
diff --git a/checkfence/c7/unshare_page.c b/checkfence/c7/unshare_page.c
new file mode 100644
--- /dev/null
+++ b/checkfence/c7/unshare_page.c
@@ -0,0 +1,57 @@
+#include "lsl_protos.h"
+
+
+int __sync_lock_test_and_set(int *lock, int nvalue)
+{
+    /* the x86 behavior of this instruction, which is really a XCHG */
+    int old = *lock;
+    lsl_assume(lsl_cas_32(lock, old, nvalue));
+    lsl_fence("load-load");
+    return old;
+}
+
+
+enum { SHARED_PAGE=0, REMAPPING_PAGE, PRIVATE_PAGE };  /* flag_page_private */
+int flag_page_private;
+int privatized_data;
+
+void INIT(void)
+{
+    flag_page_private = SHARED_PAGE;
+}
+
+void _stm_privatize(void)
+{
+    int previous = __sync_lock_test_and_set(&flag_page_private,
+                                            REMAPPING_PAGE);
+    switch (previous) {
+    case PRIVATE_PAGE:
+        lsl_assert(flag_page_private != SHARED_PAGE);
+        flag_page_private = PRIVATE_PAGE;
+        return;
+
+    case REMAPPING_PAGE:
+        lsl_assert(flag_page_private != SHARED_PAGE);
+        /* here we wait until 'flag_page_private' is changed away from
+           REMAPPING_PAGE, and we assume that it eventually occurs */
+        lsl_assume(flag_page_private != REMAPPING_PAGE);
+        lsl_fence("load-load");
+        return;
+
+    case SHARED_PAGE:
+        lsl_observe_label("privatizing");
+        privatized_data = 42;
+        lsl_fence("store-store");
+        lsl_assert(flag_page_private == REMAPPING_PAGE);
+        flag_page_private = PRIVATE_PAGE;
+        return;
+    }
+    lsl_assert(0);
+}
+
+void PRIVATIZE(void)
+{
+    _stm_privatize();
+    int data = privatized_data;
+    lsl_observe_output("data", data);
+}
diff --git a/checkfence/c7/unshare_page.lsl b/checkfence/c7/unshare_page.lsl
new file mode 100644
--- /dev/null
+++ b/checkfence/c7/unshare_page.lsl
@@ -0,0 +1,2 @@
+
+test T1 = INIT ( PRIVATIZE PRIVATIZE | PRIVATIZE PRIVATIZE | PRIVATIZE PRIVATIZE )