Author: Armin Rigo <[email protected]>
Branch: c6
Changeset: r587:52cf82f83a37
Date: 2013-12-28 19:35 +0100
http://bitbucket.org/pypy/stmgc/changeset/52cf82f83a37/
Log: Adding some more versions of the test
diff --git a/checkfence/c6/test1.c b/checkfence/c6/test1.c
--- a/checkfence/c6/test1.c
+++ b/checkfence/c6/test1.c
@@ -4,15 +4,14 @@
typedef boolean_t bool;
-#define NUM_OBJECTS 2
+#define NUM_OBJECTS 1
#define NUM_THREADS 2
-#define NUM_HISTORY 5
+#define NUM_HISTORY 2
#define UNDOLOG NUM_THREADS
-typedef void *uid_t;
-#define get_uid() lsl_malloc_noreuse(1)
+typedef unsigned uid_t;
typedef struct {
@@ -44,13 +43,11 @@
n_global_history = 0;
lsl_initlock(&undo_lock);
- int t = 0;
- while (1) {
- tl[t].n_modified_objects = 0;
- t++;
- if (t == NUM_THREADS)
- break;
- }
+ /* XXX manual unrolling */
+ tl[0].n_modified_objects = 0;
+ tl[0].transaction_read_version = 0;
+ tl[1].n_modified_objects = 0;
+ tl[1].transaction_read_version = 0;
}
@@ -109,11 +106,55 @@
}
}
+int update_to_leader(int t, int check)
+{
+ /* becomes the leader */
+ uid_t my_version = tl[t].transaction_read_version;
+ int result = check;
+ int nglob = n_global_history;
+
+ if (nglob > 0) {
+ while (1) {
+ int objnum = global_history[--nglob];
+ if (result)
+ result = (obj[t][objnum].read_version != my_version);
+ obj[t][objnum].flag_modified = false;
+ memcpy_obj_without_header(t, objnum, 1 - t, objnum);
+ if (nglob == 0)
+ break;
+ }
+ n_global_history = 0;
+ }
+ int nundo = tl[1 - t].n_modified_objects;
+ if (nundo > 0) {
+ while (1) {
+ int objnum = tl[1 - t].modified_objects[--nundo];
+ if (result)
+ result = (obj[t][objnum].read_version != my_version);
+ obj[t][objnum].flag_modified = false;
+ memcpy_obj_without_header(t, objnum, UNDOLOG, objnum);
+ if (nundo == 0)
+ break;
+ }
+ }
+ return result;
+}
+
+void update_state(int t)
+{
+ lsl_lock(&undo_lock);
+ if (leader_thread_num != t) {
+ update_to_leader(t, 0);
+ leader_thread_num = t;
+ }
+ lsl_unlock(&undo_lock);
+}
+
void start_transaction(int t)
{
lsl_assert(tl[t].n_modified_objects == 0);
lsl_assert(!obj[t][0].flag_modified);
- tl[t].transaction_read_version = get_uid();
+ tl[t].transaction_read_version++;
}
int stop_transaction(int t)
@@ -126,39 +167,18 @@
lsl_lock(&undo_lock);
- int nglob = n_global_history;
- int result = 1;
-
- if (leader_thread_num != t) {
- /* becomes the leader */
- uid_t my_version = tl[t].transaction_read_version;
-
- if (nglob > 0) {
- while (1) {
- int objnum = global_history[--nglob];
- result &= (obj[t][objnum].read_version != my_version);
- obj[t][objnum].flag_modified = false;
- memcpy_obj_without_header(t, objnum, 1 - t, objnum);
- if (nglob == 0)
- break;
- }
- }
- int nundo = tl[1 - t].n_modified_objects;
- if (nundo > 0) {
- while (1) {
- int objnum = tl[1 - t].modified_objects[--nundo];
- result &= (obj[t][objnum].read_version != my_version);
- obj[t][objnum].flag_modified = false;
- memcpy_obj_without_header(t, objnum, 1 - t, objnum);
- if (nundo == 0)
- break;
- }
- }
+ int result;
+ if (leader_thread_num == t) {
+ result = 1;
+ }
+ else {
+ result = update_to_leader(t, 1);
if (result)
leader_thread_num = t;
}
if (result) {
+ int nglob = n_global_history;
while (1) {
int objnum = tl[t].modified_objects[--nmod];
global_history[nglob++] = objnum;
@@ -166,6 +186,7 @@
if (nmod == 0)
break;
}
+ n_global_history = nglob;
}
else {
while (1) {
@@ -177,9 +198,7 @@
if (nmod == 0)
break;
}
- lsl_assert(nglob == 0);
}
- n_global_history = nglob;
tl[t].n_modified_objects = 0;
lsl_unlock(&undo_lock);
@@ -202,14 +221,17 @@
{
int t = 0;
setup();
- while (1) {
- obj[t][0].flag_modified = false;
- obj[t][0].value1 = 100;
- obj[t][0].value2 = 200;
- t++;
- if (t == NUM_THREADS)
- break;
- }
+
+ /* XXX manual unrolling */
+ obj[0][0].flag_modified = false;
+ obj[0][0].read_version = 0;
+ obj[0][0].value1 = 100;
+ obj[0][0].value2 = 200;
+
+ obj[1][0].flag_modified = false;
+ obj[1][0].read_version = 0;
+ obj[1][0].value1 = 100;
+ obj[1][0].value2 = 200;
}
void R0(void)
@@ -233,15 +255,24 @@
{
int t = lsl_get_thread_id();
int nvalue1, nvalue2;
- while (1) {
+ //update_state(t);
+
+ start_transaction(t);
+ stm_write(t, 0);
+ nvalue1 = ++obj[t][0].value1;
+ nvalue2 = ++obj[t][0].value2;
+ lsl_assert(nvalue1 == obj[t][0].value1);
+ lsl_assert(nvalue2 == obj[t][0].value2);
+ if (!stop_transaction(t)) {
start_transaction(t);
stm_write(t, 0);
nvalue1 = ++obj[t][0].value1;
nvalue2 = ++obj[t][0].value2;
lsl_assert(nvalue1 == obj[t][0].value1);
lsl_assert(nvalue2 == obj[t][0].value2);
- if (stop_transaction(t))
- break;
+ if (!stop_transaction(t)) {
+ lsl_observe_output("XXX W0INC1 failed twice", 0);
+ }
}
lsl_observe_output("W0INC1:nvalue1", nvalue1);
diff --git a/checkfence/c6/test1.lsl b/checkfence/c6/test1.lsl
--- a/checkfence/c6/test1.lsl
+++ b/checkfence/c6/test1.lsl
@@ -1,6 +1,6 @@
-test T0 = SETUP ( A | A )
+//test T0 = SETUP ( A | A )
-test T1 = SETUP100 ( R0 | R0 )
+//test T1 = SETUP100 ( R0 | R0 )
-test T2 = SETUP100 ( W0INC1 R0 | W0INC1 R0 )
+test T2 = SETUP100 ( W0INC1 | W0INC1 )
diff --git a/checkfence/c6/test2.c b/checkfence/c6/test2.c
new file mode 100644
--- /dev/null
+++ b/checkfence/c6/test2.c
@@ -0,0 +1,240 @@
+#include "lsl_protos.h"
+
+typedef unsigned short uint16_t;
+typedef boolean_t bool;
+
+
+#define NUM_THREADS 2
+#define UNDOLOG NUM_THREADS
+
+
+typedef unsigned uid_t;
+
+
+typedef struct {
+ uid_t read_version;
+ bool flag_modified;
+ int value1, value2;
+} object_t;
+
+typedef struct {
+ int n_modified_objects;
+ uid_t transaction_read_version;
+} thread_local_t;
+
+thread_local_t tl[NUM_THREADS];
+object_t obj[NUM_THREADS+1];
+int n_global_history;
+int leader_thread_num;
+lsl_lock_t undo_lock;
+
+
+void setup(void)
+{
+ /* initialize global state */
+ leader_thread_num = 0;
+ n_global_history = 0;
+ lsl_initlock(&undo_lock);
+
+ /* XXX manual unrolling */
+ tl[0].n_modified_objects = 0;
+ tl[0].transaction_read_version = 0;
+ tl[1].n_modified_objects = 0;
+ tl[1].transaction_read_version = 0;
+}
+
+
+int fetch_and_add(volatile int *loc, int increment)
+{
+ int oldvalue = *loc;
+ lsl_assume(lsl_cas_64(loc, oldvalue, oldvalue + increment));
+ return oldvalue;
+}
+
+/* int stm_allocate(int t) */
+/* { */
+/* int result = fetch_and_add(&next_free_glob, 1); */
+/* lsl_observe_output("stm_allocate", result); */
+
+/* obj[t][result].flag_modified = true; */
+/* return result; */
+/* } */
+
+int acquire_lock_if_leader(int t)
+{
+ //XXX:
+ //if (leader_thread_num != t)
+ // return 0;
+ lsl_lock(&undo_lock);
+ if (leader_thread_num == t)
+ return 1;
+ lsl_unlock(&undo_lock);
+ return 0;
+}
+
+void memcpy_obj_without_header(int tdst, int tsrc)
+{
+ obj[tdst].value1 = obj[tsrc].value1;
+ obj[tdst].value2 = obj[tsrc].value2;
+}
+
+#define stm_read(t) \
+ (obj[t].read_version = tl[t].transaction_read_version)
+
+void stm_write(int t)
+{
+ if (obj[t].flag_modified)
+ return; /* already modified during this transaction */
+
+ stm_read(t);
+
+ int is_leader = acquire_lock_if_leader(t);
+ obj[t].flag_modified = true;
+ tl[t].n_modified_objects = 1;
+ if (is_leader) {
+ memcpy_obj_without_header(UNDOLOG, t);
+ lsl_unlock(&undo_lock);
+ }
+}
+
+int update_to_leader(int t, int check)
+{
+ /* becomes the leader */
+ uid_t my_version = tl[t].transaction_read_version;
+ int result = check;
+
+ if (n_global_history > 0) {
+ if (result)
+ result = (obj[t].read_version != my_version);
+ obj[t].flag_modified = false;
+ int src = (obj[1 - t].flag_modified ? UNDOLOG : 1 - t);
+ memcpy_obj_without_header(t, src);
+ n_global_history = 0;
+ }
+ leader_thread_num = t;
+ return result;
+}
+
+void update_state(int t)
+{
+ lsl_lock(&undo_lock);
+ if (leader_thread_num != t) {
+ update_to_leader(t, 0);
+ }
+ lsl_unlock(&undo_lock);
+}
+
+void start_transaction(int t)
+{
+ lsl_assert(tl[t].n_modified_objects == 0);
+ lsl_assert(!obj[t].flag_modified);
+ tl[t].transaction_read_version++;
+}
+
+int stop_transaction(int t)
+{
+ int nmod = tl[t].n_modified_objects;
+ if (nmod == 0) {
+ /* no modified objects in this transaction */
+ return 1;
+ }
+
+ lsl_lock(&undo_lock);
+
+ int result;
+ if (leader_thread_num == t) {
+ result = 1;
+ }
+ else {
+ result = update_to_leader(t, 1);
+ }
+
+ if (result) {
+ obj[t].flag_modified = false;
+ n_global_history = 1;
+ }
+ else {
+ if (obj[t].flag_modified) {
+ obj[t].flag_modified = false;
+ memcpy_obj_without_header(t, 1 - t);
+ }
+ }
+ tl[t].n_modified_objects = 0;
+
+ lsl_unlock(&undo_lock);
+ return result;
+}
+
+
+/* void A(void) */
+/* { */
+/* int t = lsl_get_thread_id(); */
+/* int num = stm_allocate(t); */
+/* } */
+
+void SETUP(void)
+{
+ setup();
+}
+
+void SETUP100(void)
+{
+ int t = 0;
+ setup();
+
+ /* XXX manual unrolling */
+ obj[0].flag_modified = false;
+ obj[0].read_version = 0;
+ obj[0].value1 = 100;
+ obj[0].value2 = 200;
+
+ obj[1].flag_modified = false;
+ obj[1].read_version = 0;
+ obj[1].value1 = 100;
+ obj[1].value2 = 200;
+}
+
+void R0(void)
+{
+ int t = lsl_get_thread_id();
+ int result1, result2;
+ while (1) {
+ start_transaction(t);
+ stm_read(t);
+ result1 = obj[t].value1;
+ result2 = obj[t].value2;
+ if (stop_transaction(t))
+ break;
+ }
+
+ lsl_observe_output("R0:value1", result1);
+ lsl_observe_output("R0:value2", result2);
+}
+
+void W0INC1(void)
+{
+ int t = lsl_get_thread_id();
+ int nvalue1, nvalue2;
+ //update_state(t);
+
+ start_transaction(t);
+ stm_write(t);
+ nvalue1 = ++obj[t].value1;
+ nvalue2 = ++obj[t].value2;
+ lsl_assert(nvalue1 == obj[t].value1);
+ lsl_assert(nvalue2 == obj[t].value2);
+ if (!stop_transaction(t)) {
+ start_transaction(t);
+ stm_write(t);
+ nvalue1 = ++obj[t].value1;
+ nvalue2 = ++obj[t].value2;
+ lsl_assert(nvalue1 == obj[t].value1);
+ lsl_assert(nvalue2 == obj[t].value2);
+ if (!stop_transaction(t)) {
+ lsl_observe_output("XXX W0INC1 failed twice", 0);
+ }
+ }
+
+ lsl_observe_output("W0INC1:nvalue1", nvalue1);
+ lsl_observe_output("W0INC1:nvalue2", nvalue2);
+}
diff --git a/checkfence/c6/test2.lsl b/checkfence/c6/test2.lsl
new file mode 100644
--- /dev/null
+++ b/checkfence/c6/test2.lsl
@@ -0,0 +1,4 @@
+
+//test T1 = SETUP100 ( R0 | R0 )
+
+test T2 = SETUP100 ( W0INC1 | W0INC1 R0 )
diff --git a/checkfence/c6/test3.c b/checkfence/c6/test3.c
new file mode 100644
--- /dev/null
+++ b/checkfence/c6/test3.c
@@ -0,0 +1,260 @@
+#include "lsl_protos.h"
+
+typedef unsigned short uint16_t;
+typedef boolean_t bool;
+
+
+#define NUM_THREADS 2
+#define UNDOLOG NUM_THREADS
+
+
+typedef unsigned uid_t;
+
+
+typedef struct {
+ uid_t read_version;
+ char flag_modified;
+ int value1, value2;
+} object_t;
+
+typedef struct {
+ int n_modified_objects;
+ uid_t transaction_read_version;
+} thread_local_t;
+
+thread_local_t tl[NUM_THREADS];
+object_t obj[NUM_THREADS+1];
+int n_global_history;
+int leader_thread_num;
+lsl_lock_t undo_lock;
+
+
+void setup(void)
+{
+ /* initialize global state */
+ leader_thread_num = 0;
+ n_global_history = 0;
+ lsl_initlock(&undo_lock);
+
+ /* XXX manual unrolling */
+ tl[0].n_modified_objects = 0;
+ tl[0].transaction_read_version = 0;
+ tl[1].n_modified_objects = 0;
+ tl[1].transaction_read_version = 0;
+}
+
+
+int fetch_and_add(volatile int *loc, int increment)
+{
+ int oldvalue = *loc;
+ lsl_assume(lsl_cas_64(loc, oldvalue, oldvalue + increment));
+ return oldvalue;
+}
+
+/* int stm_allocate(int t) */
+/* { */
+/* int result = fetch_and_add(&next_free_glob, 1); */
+/* lsl_observe_output("stm_allocate", result); */
+
+/* obj[t][result].flag_modified = true; */
+/* return result; */
+/* } */
+
+int acquire_lock_if_leader(int t)
+{
+ //XXX:
+ //if (leader_thread_num != t)
+ // return 0;
+ lsl_lock(&undo_lock);
+ if (leader_thread_num == t)
+ return 1;
+ lsl_unlock(&undo_lock);
+ return 0;
+}
+
+void memcpy_obj_without_header(int tdst, int tsrc)
+{
+ obj[tdst].value1 = obj[tsrc].value1;
+ obj[tdst].value2 = obj[tsrc].value2;
+}
+
+#define stm_read(t) \
+ (obj[t].read_version = tl[t].transaction_read_version)
+
+void stm_write(int t)
+{
+ if (obj[t].flag_modified)
+ return; /* already modified during this transaction */
+
+ stm_read(t);
+
+ int is_leader = acquire_lock_if_leader(t);
+ obj[t].flag_modified = true;
+ tl[t].n_modified_objects = 1;
+ if (is_leader) {
+ memcpy_obj_without_header(UNDOLOG, t);
+ lsl_unlock(&undo_lock);
+ }
+}
+
+int update_to_leader(int t, int check)
+{
+ /* becomes the leader, and update the local copy of the objects */
+ uid_t my_version = tl[t].transaction_read_version;
+ int result = check;
+
+ if (n_global_history > 0) {
+
+ /* loop over objects modified by the leader, and set their
+ local 'flag_modified' to '2' */
+ if (tl[1 - t].n_modified_objects) {
+ obj[t].flag_modified = 109;
+ }
+
+ /* now loop over objects in 'global_history': if they have been
+ read by the current transaction, the current transaction must
+ abort; then either copy, or mark as copy later */
+ if (result)
+ result = (obj[t].read_version != my_version);
+ if (obj[t].flag_modified == 109) {
+ obj[t].flag_modified = 67;
+ }
+ else {
+ memcpy_obj_without_header(t, 1 - t);
+ }
+
+ /* finally, loop again over objects modified by the leader,
+ and copy the marked ones out of the undo log */
+ if (tl[1 - t].n_modified_objects) {
+ if (obj[t].flag_modified == 67) {
+ memcpy_obj_without_header(t, UNDOLOG);
+ }
+ obj[t].flag_modified = false;
+ }
+
+ n_global_history = 0;
+ }
+ leader_thread_num = t;
+ return result;
+}
+
+/* void update_state(int t) */
+/* { */
+/* lsl_lock(&undo_lock); */
+/* if (leader_thread_num != t) { */
+/* update_to_leader(t, 0); */
+/* } */
+/* lsl_unlock(&undo_lock); */
+/* } */
+
+void start_transaction(int t)
+{
+ lsl_assert(tl[t].n_modified_objects == 0);
+ lsl_assert(!obj[t].flag_modified);
+ tl[t].transaction_read_version++;
+}
+
+int stop_transaction(int t)
+{
+ int nmod = tl[t].n_modified_objects;
+ if (nmod == 0) {
+ /* no modified objects in this transaction */
+ return 1;
+ }
+
+ lsl_lock(&undo_lock);
+
+ int result;
+ if (leader_thread_num == t) {
+ result = 1;
+ }
+ else {
+ result = update_to_leader(t, 1);
+ }
+
+ if (result) {
+ obj[t].flag_modified = false;
+ n_global_history = 1;
+ }
+ else {
+ obj[t].flag_modified = false;
+ }
+ tl[t].n_modified_objects = 0;
+
+ lsl_unlock(&undo_lock);
+ return result;
+}
+
+
+/* void A(void) */
+/* { */
+/* int t = lsl_get_thread_id(); */
+/* int num = stm_allocate(t); */
+/* } */
+
+void SETUP(void)
+{
+ setup();
+}
+
+void SETUP100(void)
+{
+ int t = 0;
+ setup();
+
+ /* XXX manual unrolling */
+ obj[0].flag_modified = false;
+ obj[0].read_version = 0;
+ obj[0].value1 = 100;
+ obj[0].value2 = 200;
+
+ obj[1].flag_modified = false;
+ obj[1].read_version = 0;
+ obj[1].value1 = 100;
+ obj[1].value2 = 200;
+}
+
+void R0(void)
+{
+ int t = lsl_get_thread_id();
+ int result1, result2;
+ while (1) {
+ start_transaction(t);
+ stm_read(t);
+ result1 = obj[t].value1;
+ result2 = obj[t].value2;
+ if (stop_transaction(t))
+ break;
+ }
+
+ lsl_observe_output("R0:value1", result1);
+ lsl_observe_output("R0:value2", result2);
+}
+
+void W0INC1(void)
+{
+ int t = lsl_get_thread_id();
+ int nvalue1, nvalue2;
+ //update_state(t);
+
+ start_transaction(t);
+ stm_write(t);
+ nvalue1 = ++obj[t].value1;
+ nvalue2 = ++obj[t].value2;
+ lsl_assert(nvalue1 == obj[t].value1);
+ lsl_assert(nvalue2 == obj[t].value2);
+ if (!stop_transaction(t)) {
+ start_transaction(t);
+ stm_write(t);
+ nvalue1 = ++obj[t].value1;
+ nvalue2 = ++obj[t].value2;
+ lsl_assert(nvalue1 == obj[t].value1);
+ lsl_assert(nvalue2 == obj[t].value2);
+ if (!stop_transaction(t)) {
+ lsl_observe_output("XXX W0INC1 failed twice", 0);
+ }
+ }
+
+ lsl_observe_output("W0INC1:nvalue1", nvalue1);
+ lsl_observe_output("W0INC1:nvalue2", nvalue2);
+}
diff --git a/checkfence/c6/test3.lsl b/checkfence/c6/test3.lsl
new file mode 100644
--- /dev/null
+++ b/checkfence/c6/test3.lsl
@@ -0,0 +1,4 @@
+
+//test T1 = SETUP100 ( R0 | R0 )
+
+test T2 = SETUP100 ( W0INC1 | W0INC1 )
_______________________________________________
pypy-commit mailing list
[email protected]
https://mail.python.org/mailman/listinfo/pypy-commit
