X-Git-Url: https://git.lttng.org/?p=urcu.git;a=blobdiff_plain;f=formal-model%2Fooomem-double-update%2Fmem.spin;h=48c40f19af0abdf966e8f1c3ce4d0c657c87057e;hp=4c5d6fd31f0676ea5d592ceed9887a6d20bde80b;hb=dfa8abef9f88fd28e232b0eab9a105fc50e71959;hpb=67ef1a2cd793e5dde7db32ef5210fc002c3325cd

diff --git a/formal-model/ooomem-double-update/mem.spin b/formal-model/ooomem-double-update/mem.spin
index 4c5d6fd..48c40f1 100644
--- a/formal-model/ooomem-double-update/mem.spin
+++ b/formal-model/ooomem-double-update/mem.spin
@@ -20,8 +20,23 @@
 
 /* Promela validation variables. */
 
-#define NR_READERS 1
-#define NR_WRITERS 1
+/*
+ * Produced process control and data flow. Updated after each instruction to
+ * show which variables are ready. Using one-hot bit encoding per variable to
+ * save state space. Used as triggers to execute the instructions having those
+ * variables as input. Leaving bits active to inhibit instruction execution.
+ * Scheme used to make instruction disabling and automatic dependency fall-back
+ * automatic.
+ */
+
+#define CONSUME_TOKENS(state, bits, notbits)			\
+	((!(state & (notbits))) && (state & (bits)) == (bits))
+
+#define PRODUCE_TOKENS(state, bits)				\
+	state = state | (bits);
+
+#define CLEAR_TOKENS(state, bits)				\
+	state = state & ~(bits)
 
 #define NR_PROCS 2
 
@@ -33,17 +48,18 @@
  * both.
  */
 
-#define DECLARE_CACHED_VAR(type, x, v)	\
-	type mem_##x = v;		\
-	type cached_##x[NR_PROCS] = v;	\
-	bit cache_dirty_##x[NR_PROCS] = 0
+#define DECLARE_CACHED_VAR(type, x, v)		\
+	type mem_##x = v;			\
+	type cached_##x[NR_PROCS] = v;		\
+	bit cache_dirty_##x[NR_PROCS] = 0;
 
 #define IS_CACHE_DIRTY(x, id)	(cache_dirty_##x[id])
 
-#define READ_CACHED_VAR(x)	(cached_##x[get_pid()])
+#define READ_CACHED_VAR(x)			\
+	(cached_##x[get_pid()])
 
-#define WRITE_CACHED_VAR(x, v)		\
-	atomic {			\
+#define WRITE_CACHED_VAR(x, v)			\
+	atomic {				\
 		cached_##x[get_pid()] = v;	\
 		cache_dirty_##x[get_pid()] = 1;	\
 	}
@@ -57,37 +73,50 @@
 		skip				\
 	fi;
 
-#define CACHE_READ_FROM_MEM(x, id)	\
-	if				\
-	:: !IS_CACHE_DIRTY(x, id) ->	\
-		cached_##x[id] = mem_##x;\
-	:: else ->			\
-		skip			\
+#define CACHE_READ_FROM_MEM(x, id)		\
+	if					\
+	:: !IS_CACHE_DIRTY(x, id) ->		\
+		cached_##x[id] = mem_##x;	\
+	:: else ->				\
+		skip				\
 	fi;
 
 /*
  * May update other caches if cache is dirty, or not.
  */
-#define RANDOM_CACHE_WRITE_TO_MEM(x, id)\
-	if				\
+#define RANDOM_CACHE_WRITE_TO_MEM(x, id)	\
+	if					\
 	:: 1 -> CACHE_WRITE_TO_MEM(x, id);	\
-	:: 1 -> skip			\
+	:: 1 -> skip				\
 	fi;
 
 #define RANDOM_CACHE_READ_FROM_MEM(x, id)\
-	if				\
+	if					\
 	:: 1 -> CACHE_READ_FROM_MEM(x, id);	\
-	:: 1 -> skip			\
+	:: 1 -> skip				\
 	fi;
 
+inline ooo_mem()
+{
+	atomic {
+		RANDOM_CACHE_WRITE_TO_MEM(alpha, get_pid());
+		RANDOM_CACHE_WRITE_TO_MEM(beta, get_pid());
+		RANDOM_CACHE_READ_FROM_MEM(alpha, get_pid());
+		RANDOM_CACHE_READ_FROM_MEM(beta, get_pid());
+	}
+}
+
+/* must consume all prior read tokens */
 inline smp_rmb()
 {
 	atomic {
+		/* todo : consume all read tokens .. ? */
 		CACHE_READ_FROM_MEM(alpha, get_pid());
 		CACHE_READ_FROM_MEM(beta, get_pid());
 	}
 }
 
+/* must consume all prior write tokens */
 inline smp_wmb()
 {
 	atomic {
@@ -96,10 +125,15 @@ inline smp_wmb()
 	}
 }
 
+/* sync_core() must consume all prior read and write tokens, including rmb/wmb
+ * tokens */
+
+/* must consume all prior read and write tokens */
 inline smp_mb()
 {
 	atomic {
 		smp_wmb();
+		/* sync_core() */
 		smp_rmb();
 	}
 }
@@ -108,60 +142,108 @@ inline smp_mb()
 DECLARE_CACHED_VAR(byte, alpha, 0);
 DECLARE_CACHED_VAR(byte, beta, 0);
 
-inline ooo_mem()
-{
-	atomic {
-		RANDOM_CACHE_WRITE_TO_MEM(alpha, get_pid());
-		RANDOM_CACHE_WRITE_TO_MEM(beta, get_pid());
-		RANDOM_CACHE_READ_FROM_MEM(alpha, get_pid());
-		RANDOM_CACHE_READ_FROM_MEM(beta, get_pid());
-	}
-}
-
 /* value 2 is uninitialized */
 byte read_one = 2;
 byte read_two = 2;
 
+/*
+ * Bit encoding, proc_one_produced :
+ */
+
+#define P1_PROD_NONE	(1 << 0)
+
+#define P1_READ_ONE	(1 << 1)
+#define P1_RMB		(1 << 2)
+#define P1_READ_TWO	(1 << 3)
+
+/* Only need a single color. */
+byte proc_one_produced;
+
 active proctype test_proc_one()
 {
 	assert(get_pid() < NR_PROCS);
 
-	ooo_mem();
-	WRITE_CACHED_VAR(alpha, 1);
-	ooo_mem();
-#ifndef NO_WMB
-	smp_wmb();
-	ooo_mem();
-#endif
-#ifndef NO_RMB
-	smp_rmb();
-	ooo_mem();
+	PRODUCE_TOKENS(proc_one_produced, P1_PROD_NONE);
+#ifdef NO_RMB
+	PRODUCE_TOKENS(proc_one_produced, P1_RMB);
 #endif
-	read_one = READ_CACHED_VAR(beta);
-	ooo_mem();
-	// test : [] (read_one == 0 -> read_two != 0)
-	// test : [] (read_two == 0 -> read_one != 0)
-	assert(!(read_one == 0 && read_two == 0));
+
+	do
+	:: CONSUME_TOKENS(proc_one_produced,
+			P1_PROD_NONE, P1_READ_ONE) ->
+		ooo_mem();
+		read_one = READ_CACHED_VAR(beta);
+		ooo_mem();
+		PRODUCE_TOKENS(proc_one_produced, P1_READ_ONE);
+	:: CONSUME_TOKENS(proc_one_produced,
+			P1_READ_ONE, P1_RMB) ->
+		smp_rmb();
+		PRODUCE_TOKENS(proc_one_produced, P1_RMB);
+	:: CONSUME_TOKENS(proc_one_produced,
+			P1_RMB, P1_READ_TWO) ->
+		ooo_mem();
+		read_two = READ_CACHED_VAR(alpha);
+		ooo_mem();
+		PRODUCE_TOKENS(proc_one_produced, P1_READ_TWO);
+	:: CONSUME_TOKENS(proc_one_produced,
+			P1_PROD_NONE | P1_READ_ONE | P1_RMB
+			| P1_READ_TWO, 0) ->
+		break;
+	od;
+
+	//CLEAR_TOKENS(proc_one_produced,
+	//	P1_PROD_NONE | P1_READ_ONE | P1_RMB | P1_READ_TWO);
+
+	// test : [] (read_one == 1 -> read_two == 1)
+	assert(read_one != 1 || read_two == 1);
 }
 
+
+/*
+ * Bit encoding, proc_two_produced :
+ */
+
+#define P2_PROD_NONE	(1 << 0)
+
+#define P2_WRITE_ONE	(1 << 1)
+#define P2_WMB		(1 << 2)
+#define P2_WRITE_TWO	(1 << 3)
+
+/* Only need a single color. */
+byte proc_two_produced;
+
 active proctype test_proc_two()
 {
 	assert(get_pid() < NR_PROCS);
 
-	ooo_mem();
-	WRITE_CACHED_VAR(beta, 1);
-	ooo_mem();
-#ifndef NO_WMB
-	smp_wmb();
-	ooo_mem();
+	PRODUCE_TOKENS(proc_two_produced, P2_PROD_NONE);
+#ifdef NO_WMB
+	PRODUCE_TOKENS(proc_two_produced, P2_WMB);
 #endif
-#ifndef NO_RMB
-	smp_rmb();
-	ooo_mem();
-#endif
-	read_two = READ_CACHED_VAR(alpha);
-	ooo_mem();
-	// test : [] (read_one == 0 -> read_two != 0)
-	// test : [] (read_two == 0 -> read_one != 0)
-	assert(!(read_one == 0 && read_two == 0));
+
+	do
+	:: CONSUME_TOKENS(proc_two_produced,
+			P2_PROD_NONE, P2_WRITE_ONE) ->
+		ooo_mem();
+		WRITE_CACHED_VAR(alpha, 1);
+		ooo_mem();
+		PRODUCE_TOKENS(proc_two_produced, P2_WRITE_ONE);
+	:: CONSUME_TOKENS(proc_two_produced,
+			P2_WRITE_ONE, P2_WMB) ->
+		smp_wmb();
+		PRODUCE_TOKENS(proc_two_produced, P2_WMB);
+	:: CONSUME_TOKENS(proc_two_produced,
+			P2_WMB, P2_WRITE_TWO) ->
+		ooo_mem();
+		WRITE_CACHED_VAR(beta, 1);
+		ooo_mem();
+		PRODUCE_TOKENS(proc_two_produced, P2_WRITE_TWO);
+	:: CONSUME_TOKENS(proc_two_produced,
+			P2_PROD_NONE | P2_WRITE_ONE
+			| P2_WMB | P2_WRITE_TWO, 0) ->
+		break;
+	od;
+
+	//CLEAR_TOKENS(proc_two_produced,
+	//	P2_PROD_NONE | P2_WRITE_ONE | P2_WMB | P2_WRITE_TWO);
 }