[pypy-commit] stmgc default: Add the first nice checkfence demo with a minimal stm.

[arigo]

Author: Armin Rigo <arigo at tunes.org>
Branch: 
Changeset: r486:6d314a5409dd
Date: 2013-08-20 21:29 +0200
http://bitbucket.org/pypy/stmgc/changeset/6d314a5409dd/

Log:	Add the first nice checkfence demo with a minimal stm.

	Add the 'howto-checkfence' from arigo/arigo, complete it with how to
	run the demo.

diff --git a/checkfence/README b/checkfence/README
new file mode 100644
--- /dev/null
+++ b/checkfence/README
@@ -0,0 +1,56 @@
+Installing checkfence on Linux 64
+---------------------------------
+
+apt-get install bison flex ocaml ocaml-findlib
+
+cvs -z3 -d:pserver:anonymous at checkfence.cvs.sourceforge.net:/cvsroot/checkfence co -P checkfence
+
+cvs -z3 -d:pserver:anonymous at checkfence.cvs.sourceforge.net:/cvsroot/checkfence co -P c2lsl
+
+
+http://www.princeton.edu/~chaff/zchaff.html
+   for Linux 64 you need zchaff.64bit.2007.3.12.zip.
+   I did not try the 32-bit version.
+
+   Build with "make -j1".
+
+   This is C++ code with errors: it's missing these lines
+       #include <cstdlib>
+       #include <cstring>
+   at the top of some files.  Add as you get the errors.
+
+
+CIL version 1.3.7 (the more recent 1.7.3 doesn't work here)
+   http://sourceforge.net/projects/cil/files/cil/cil-1.3.7/
+
+   cd /usr/lib/ocaml
+   sudo ln -s libcamlstr.a libstr.a
+   
+   ./configure
+   make -j1
+
+
+Compiling checkfence:
+   cd checkfence/build
+   
+   edit the Makefile: ZCHAFFDIR=/path/to/zchaff64
+   make opt
+
+
+Compiling C2LSL:
+   cd c2lsl
+   
+   edit the Makefile: CILDIR=/path/to/cil-1.3.7
+   and also: CILINCLUDES=....x86_LINUX (instead of x86_WIN32)
+
+   make -j1
+
+
+
+Running the examples:
+   cd c4
+   ln -s /full/path/to/c2lsl
+   ln -s /full/path/to/checkfence
+   ./run test1.c test1.lsl
+
+   Look at 'T0.bsc-overview.htm' in your web browser.
diff --git a/checkfence/c4/run b/checkfence/c4/run
new file mode 100755
--- /dev/null
+++ b/checkfence/c4/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/c4/test1.c b/checkfence/c4/test1.c
new file mode 100644
--- /dev/null
+++ b/checkfence/c4/test1.c
@@ -0,0 +1,93 @@
+#include "lsl_protos.h"
+
+
+#define PREBUILT_FLAGS     0
+#define LOCKED             5
+
+typedef int revision_t;
+
+
+typedef struct {
+    int        h_flags;
+    revision_t h_revision;
+    revision_t h_original;
+    int        value;
+} object_t;
+
+object_t o1, o2;
+int global_timestamp;
+
+struct tx_descriptor {
+    int starttime;
+    int lock;
+    object_t *copy_of_o1;
+};
+
+void init_descriptor(struct tx_descriptor *d)
+{
+    d->starttime = global_timestamp; lsl_fence("load-load");
+    d->copy_of_o1 = NULL;
+    //d->lock = lsl_get_thread_id() + 1000000;
+}
+
+
+object_t *stm_write_barrier(struct tx_descriptor *d, object_t *P)
+{
+    lsl_observe_label("write_barrier");
+
+    if (d->copy_of_o1 == NULL) {
+        lsl_assume(P->h_revision <= d->starttime);  /* otherwise, abort */
+
+        object_t *W = lsl_malloc(sizeof(object_t));
+        W->value = P->value;
+        d->copy_of_o1 = W;
+    }
+    return d->copy_of_o1;
+}
+
+
+void i()
+{
+    o1.h_flags    = PREBUILT_FLAGS;
+    o1.h_revision = 0;
+    o1.h_original = 0;
+    o1.value      = 50;
+    global_timestamp = 2;
+}
+
+void commit(struct tx_descriptor *d)
+{
+    lsl_observe_label("commit");
+
+    if (d->copy_of_o1 != NULL) {
+        int old = o1.h_revision;
+        lsl_assume(old <= d->starttime);   /* otherwise, abort */
+        lsl_assume(lsl_cas_32(&o1.h_revision, old, LOCKED));  /* retry */
+    }
+
+    int endtime = global_timestamp + 1;
+    lsl_fence("load-load");
+    lsl_assume(lsl_cas_32(&global_timestamp, endtime - 1, endtime));
+    /* otherwise, retry */
+
+    if (d->copy_of_o1 != NULL) {
+        int o1_value = d->copy_of_o1->value;
+        o1.value = o1_value;
+        lsl_fence("store-store");
+        o1.h_revision = endtime;
+        lsl_observe_output("o1_value", o1_value);
+        d->copy_of_o1 = NULL;
+    }
+}
+
+void W1()
+{
+    struct tx_descriptor d;
+
+    init_descriptor(&d);
+
+    object_t *p1 = stm_write_barrier(&d, &o1);
+    ++p1->value;
+
+    commit(&d);
+}
diff --git a/checkfence/c4/test1.lsl b/checkfence/c4/test1.lsl
new file mode 100644
--- /dev/null
+++ b/checkfence/c4/test1.lsl
@@ -0,0 +1,2 @@
+
+test T0 = i ( W1 | W1 )