Author: Armin Rigo <ar...@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:anonym...@checkfence.cvs.sourceforge.net:/cvsroot/checkfence co -P
checkfence
+
+cvs -z3
-d:pserver:anonym...@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 )
_______________________________________________
pypy-commit mailing list
pypy-commit@python.org
http://mail.python.org/mailman/listinfo/pypy-commit
