Uncomment writer thread and provide example metadata

Enable shared memory fixed-point for latest rmem and provide example
metadata for further improving search speed.

Signed-off-by: Shaked Flur <shaked.flur@cl.cam.ac.uk>
Signed-off-by: Will Deacon <will.deacon@arm.com>

4 files changed, 46 insertions, 6 deletions

diff --git a/main.c b/main.c
index 5f143c5..1a0b22e 100644
--- a/main.c
+++ b/main.c
@@ -10,14 +10,11 @@ static int count = 0;
  */
 static void writer(void)
 {
-#if 0
 	arch_write_lock(&lock);
 	count = 1;
 	barrier();
 	count = 2;
 	arch_write_unlock(&lock);
-#endif
-	exit();
 }
 
 static void reader(void)
@@ -25,12 +22,10 @@ static void reader(void)
 	arch_read_lock(&lock);
 	assert(count != 1);
 	arch_read_unlock(&lock);
-	exit();
 }
 
 void _start(void)
 {
 	__rmem_thread_start(writer);
-	//__rmem_thread_start(reader);
 	reader();
 }
diff --git a/metadata/qrwlock.branch_targets b/metadata/qrwlock.branch_targets
new file mode 100644
index 0000000..9f1883b
--- /dev/null
+++ b/metadata/qrwlock.branch_targets
@@ -0,0 +1,23 @@
+# this file can be used with the rmem -branch_targets argument
+#
+# syntax:
+#   <thread-id>:<loc-source> -> {<loc-target-1>[,<loc-target-2>[,...]]};
+# where <thread-id> is a thread number, <loc-source> is the location of a
+# branch-register/ret instruction and <loc-target-i> are the locations the
+# instruction from <loc-source> can jump to. You can specify locations
+# using decimal numbers, hexadecimal numbers (with 0x prefix) and symbols
+# from the ELF header, with an offset, e.g.:
+#   _start - 4
+#   0xfffff0 + 8
+#
+# When running rmem with the -v argument, when a new jump is observed it
+# will be printed to the screen, and after every iteration of exhaustive
+# search is completed all the observed jumps will be printed to the screen.
+# You can copy/paste those into a file.
+#
+# If you under specify the targets, rmem will need more iterations to reach
+# a fixed point; if you specify targets that are not reachable, each iteration
+# will take longer.
+
+0:0x4001d4 -> {0x40039c}; # ret from call to queued_read_lock_slowpath
+1:0x4002a0 -> {0x4002e4}; # ret from call to queued_write_lock_slowpath
diff --git a/metadata/qrwlock.shared_mem b/metadata/qrwlock.shared_mem
new file mode 100644
index 0000000..74a181c
--- /dev/null
+++ b/metadata/qrwlock.shared_mem
@@ -0,0 +1,22 @@
+# this file can be used with the rmem -shared_memory argument
+#
+# syntax:
+#   <location>[+ <offset>][/<size>];
+#   <num_min> - <num_max>;
+# where <location> can be a decimal number, hexadecimal number (with 0x
+# prefix) or a symbol from the ELF header. If you use a symbol without
+# offset and size the size will be taken from the ELF header. Otherwise,
+# if size is omitted the location is considered to be 1 byte. The second
+# version is interpreted as a range (inclusive).
+#
+# When running rmem with the -v argument, when a new shared location is
+# observed it will be printed to the screen, and after every iteration
+# of exhaustive search is completed all the observed shared locations
+# will be printed to the screen. You can copy/paste those into a file.
+#
+# If you under specify the shared locations, rmem will need more iterations
+# to reach a fixed point; if you specify locations that are not really
+# shared, each iteration will take longer.
+
+lock/4;
+count/4;
diff --git a/run-batch.sh b/run-batch.sh
index 13fcf19..a97479b 100755
--- a/run-batch.sh
+++ b/run-batch.sh
@@ -13,4 +13,4 @@ if ! [ -x ${RMEM} ]; then
 	exit 1
 fi
 
-${RMEM} -model flat -shallow_embedding true -eager true -hash_prune true -interactive false -loop_limit 1 -elf_threads $2 $1 -isa_defs_path ./ -model forbid_tree_speculation -prune_restarts true -prune_discards true -priority_reduction true -v -allow_partial true
+${RMEM} -model flat -shallow_embedding true -eager true -eager_local_mem true -hash_prune true -interactive false -loop_limit 1 -elf_threads $2 $1 -isa_defs_path ./ -model forbid_tree_speculation -prune_restarts true -prune_discards true -priority_reduction true -v -allow_partial true