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>
diff --git a/main.c b/main.c
index 5f143c5..1a0b22e 100644
--- a/main.c
+++ b/main.c
@@ -10,14 +10,11 @@
*/
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 @@
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 @@
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
