diff --git a/dirs-and-confs.txt b/dirs-and-confs.txt
index 3cb4d38fec..1d77ebb707 100644
--- a/dirs-and-confs.txt
+++ b/dirs-and-confs.txt
@@ -7,4 +7,4 @@
 ./herd/tests/instructions/AArch64.self ./herd/tests/instructions/AArch64.self/self.cfg
 ./herd/tests/instructions/AArch64.kvm ./herd/tests/instructions/AArch64.kvm/kvm.cfg
 ./herd/tests/instructions/AArch64.vmsa+mte ./herd/tests/instructions/AArch64.vmsa+mte/vmsa+mte.cfg
-catalogue/aarch64-ifetch/tests catalogue/aarch64-ifetch/cfgs/new-web.cfg
\ No newline at end of file
+catalogue/aarch64-ifetch/tests catalogue/aarch64-ifetch/cfgs/new-web.cfg
diff --git a/litmus/dumpRun.ml b/litmus/dumpRun.ml
index eff24b42ba..b41576669d 100644
--- a/litmus/dumpRun.ml
+++ b/litmus/dumpRun.ml
@@ -125,6 +125,15 @@ end = struct
         (List.rev sources) ;
       fprintf chan "\n"
     end ;
+    begin
+      begin match Cfg.mode with
+        | Mode.Kvm -> ()
+        | Mode.Std | Mode.PreSi ->
+           fprintf chan "SRCDIR = $(CURDIR)\n"
+      end ;
+      fprintf chan "SHARED_SRC_DIR = $(CURDIR)/lib\n" ;
+      fprintf chan "GCCOPTS += -I $(SHARED_SRC_DIR)\n\n"
+    end ;
     begin
       match Cfg.mode with
       | Mode.Std|Mode.PreSi -> ()
@@ -143,9 +152,15 @@ end = struct
            if flags.Flags.pac then
              "auth.o"::utils
            else utils in
-         fprintf chan "UTILS=%s\n"
+         fprintf chan "UTILS = %s\n\n"
            (String.concat " " utils)
     end ;
+    begin
+      fprintf chan "UTILS_SRC = $(wildcard $(SHARED_SRC_DIR)/*.c)\n\n"
+    end ;
+    begin
+      fprintf chan "UTILS_OBJ = $(UTILS_SRC:.c=.o)\n\n"
+    end ;
     ()
 
   let makefile_clean chan extra =
@@ -167,10 +182,10 @@ end = struct
             b :: k
           else k) utils [] in
     List.iter
-      (fun u ->
+      (fun u -> 
         let src = u ^ ".c" and obj = u ^ ".o" in
         fprintf chan "%s: %s\n" obj src ;
-        fprintf chan "\t$(GCC) $(GCCOPTS) %s-O2 -c %s\n"
+        fprintf chan "\t$(GCC) $(GCCOPTS) %s-O2 -c -o $@ %s\n"
           (if
             TargetOS.is_freebsd Cfg.targetos &&
             u = "affinity"
@@ -180,9 +195,11 @@ end = struct
         fprintf chan "\n")
       utils ;
 (* UTIL objs *)
+    fprintf chan "$(SHARED_SRC_DIR)/%%.o: $(SHARED_SRC_DIR)/%%.c\n";
+    fprintf chan "\t$(GCC) $(GCCOPTS) -O2 -c -o $@ $<\n\n" ;
     let utils_objs =
       String.concat " " (List.map (fun s -> s ^ ".o") utils) in
-    fprintf chan "UTILS=%s\n\n" utils_objs ;
+    fprintf chan "UTILS = %s\n\n" utils_objs ;
     ()
 ;;
 
@@ -477,9 +494,9 @@ let dump_shell_cont arch flags sources utils =
           | TargetOS.Linux|TargetOS.AIX
           | TargetOS.FreeBsd|TargetOS.Android8
             -> 's' in
-          fprintf chan "%%.exe:%%.%c $(UTILS)\n" src_ext ;
+          fprintf chan "%%.exe:%%.%c $(UTILS) $(UTILS_OBJ)\n" src_ext ;
           fprintf chan
-            "\t$(GCC) $(GCCOPTS) $(LINKOPTS) -o $@ $(UTILS) $<\n" ;
+            "\t$(GCC) $(GCCOPTS) $(LINKOPTS) -o $@ $(UTILS) $(UTILS_OBJ) $<\n" ;
           fprintf chan "\n" ;
 (* .s pattern rule *)
           fprintf chan "%%.s:%%.c\n" ;
@@ -668,12 +685,12 @@ let dump_c_cont xcode arch flags sources utils nts =
             fprintf chan "\tsed -e 's|.c$$|.o|g' < src > obj\n\n"
           end ;
           let o1 =
-            if infile then "$(UTILS) obj run.o"
-            else "$(UTILS) $(OBJ) run.o" in
+            if infile then "$(UTILS) $(UTILS_OBJ) obj run.o"
+            else "$(UTILS) $(UTILS_OBJ) $(OBJ) run.o" in
           let o2 =
-            if infile then "$(UTILS) @obj run.o"
+            if infile then "$(UTILS) $(UTILS_OBJ) @obj run.o"
             else o1 in
-          fprintf chan "$(EXE): %s\n" o1 ;
+          fprintf chan "$(EXE): %s\n" o1;
           fprintf chan "\t$(GCC)  $(GCCOPTS) $(LINKOPTS) -o $@ %s\n" o2 ;
           fprintf chan "\n" ;
           (* .o pattern rule *)
diff --git a/litmus/libdir/_aarch64/_auth.h b/litmus/libdir/_aarch64/_auth.h
index c6b51a69e3..3529e3db5d 100644
--- a/litmus/libdir/_aarch64/_auth.h
+++ b/litmus/libdir/_aarch64/_auth.h
@@ -4,7 +4,7 @@
 /* Jade Alglave, University College London, UK.                             */
 /* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
 /*                                                                          */
-/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
 /* en Automatique and the authors. All rights reserved.                     */
 /*                                                                          */
 /* This software is governed by the CeCILL-B license under French law and   */
diff --git a/litmus/libdir/_aarch64/_memtag.c b/litmus/libdir/_aarch64/_memtag.c
index 97e2fb50d0..6c4b2bb02d 100644
--- a/litmus/libdir/_aarch64/_memtag.c
+++ b/litmus/libdir/_aarch64/_memtag.c
@@ -14,9 +14,6 @@
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
 
-#ifndef _MEMTAG_H
-#define _MEMTAG_H 1
-
 #include "kvm-headers.h"
 #include "memtag.h"
 
@@ -109,5 +106,3 @@ void mte_init(tag_check_key tag_check)
     set_tcr_el1(tcr); // also issues isb and flushes tlb
   }
 }
-
-#endif /* _MEMTAG_H */
diff --git a/litmus/libdir/_aarch64/_memtag.h b/litmus/libdir/_aarch64/_memtag.h
index 0bfec73e7c..e450516fd5 100644
--- a/litmus/libdir/_aarch64/_memtag.h
+++ b/litmus/libdir/_aarch64/_memtag.h
@@ -4,7 +4,7 @@
 /* Jade Alglave, University College London, UK.                             */
 /* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
 /*                                                                          */
-/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
 /* en Automatique and the authors. All rights reserved.                     */
 /*                                                                          */
 /* This software is governed by the CeCILL-B license under French law and   */
@@ -13,6 +13,8 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
+#ifndef _MEMTAG_H
+#define _MEMTAG_H 1
 
 typedef enum
 { tag_check_Off = 0b0000,
@@ -22,3 +24,4 @@ typedef enum
 } tag_check_key;
 
 void mte_init(tag_check_key tag_check);
+#endif
diff --git a/litmus/libdir/_aarch64/asmhandler.c b/litmus/libdir/_aarch64/asmhandler.c
index bbd5d1a829..4c27fc608e 100644
--- a/litmus/libdir/_aarch64/asmhandler.c
+++ b/litmus/libdir/_aarch64/asmhandler.c
@@ -1,4 +1,21 @@
-static void exceptions_init_test(void *p) {
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#include <asmhandler.h>
+
+void exceptions_init_test(void *p) {
   asm __volatile__ (
 "msr vbar_el1,%0\n\t"
 "isb\n"
diff --git a/litmus/libdir/_aarch64/asmhandler.h b/litmus/libdir/_aarch64/asmhandler.h
new file mode 100644
index 0000000000..d707d10c2c
--- /dev/null
+++ b/litmus/libdir/_aarch64/asmhandler.h
@@ -0,0 +1,19 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef ASMHANDLER_H
+#define ASMHANDLER_H 1
+void exceptions_init_test(void *p);
+#endif
diff --git a/litmus/libdir/_aarch64/barrier.c b/litmus/libdir/_aarch64/barrier.c
index d21f3c26a1..5ce6a7197f 100644
--- a/litmus/libdir/_aarch64/barrier.c
+++ b/litmus/libdir/_aarch64/barrier.c
@@ -16,14 +16,9 @@
 /**********************/
 /* User level barrier */
 /**********************/
+#include "barrier.h"
 
-
-typedef struct {
-  volatile int c,sense;
-  int n ;
-} sense_t;
-
-static void barrier_init (sense_t *p,int n) {
+void barrier_init (sense_t *p,int n) {
   p->n = p->c = n;
   p->sense = 0;
 }
@@ -53,7 +48,7 @@ static void barrier_init (sense_t *p,int n) {
 	dmb	ish
 	ret
 */
-static void barrier_wait(sense_t *p) {
+void barrier_wait(sense_t *p) {
   int sense = p->sense ;
   int r1,r3 ;
 asm __volatile (
@@ -87,7 +82,7 @@ asm __volatile (
 }
 #if 0
 /* C version */
-static void barrier_wait(sense_t *p) {
+void barrier_wait(sense_t *p) {
   int sense = p->sense ;
   __sync_synchronize() ;
   int rem = __sync_add_and_fetch(&p->c,-1) ;
diff --git a/litmus/libdir/_aarch64/barrier.h b/litmus/libdir/_aarch64/barrier.h
new file mode 100644
index 0000000000..1b4c9a1478
--- /dev/null
+++ b/litmus/libdir/_aarch64/barrier.h
@@ -0,0 +1,30 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2015-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+/**********************/
+/* User level barrier */
+/**********************/
+#ifndef BARRIER_H
+#define BARRIER_H 1
+
+typedef struct {
+  volatile int c,sense;
+  int n ;
+} sense_t;
+
+void barrier_init (sense_t *p,int n);
+
+void barrier_wait(sense_t *p);
+#endif
diff --git a/litmus/libdir/_aarch64/instruction.h b/litmus/libdir/_aarch64/instruction.h
index 9284c75901..f53ed7f3df 100644
--- a/litmus/libdir/_aarch64/instruction.h
+++ b/litmus/libdir/_aarch64/instruction.h
@@ -1 +1,22 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef INSTRUCTION_H
+#define INSTRUCTION_H
+#include <stdint.h>
+
 typedef uint32_t ins_t; /* Type of instructions */
+#endif
diff --git a/litmus/libdir/_aarch64/intrinsics.h b/litmus/libdir/_aarch64/intrinsics.h
index 58cd256afe..2c9a25e54f 100644
--- a/litmus/libdir/_aarch64/intrinsics.h
+++ b/litmus/libdir/_aarch64/intrinsics.h
@@ -1,3 +1,19 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
 #ifdef __ARM_NEON
 #include <arm_neon.h>
 #define cast(v)			\
diff --git a/litmus/libdir/_aarch64/kvm-headers.h b/litmus/libdir/_aarch64/kvm-headers.h
index 3e7ab51591..2378aee07d 100644
--- a/litmus/libdir/_aarch64/kvm-headers.h
+++ b/litmus/libdir/_aarch64/kvm-headers.h
@@ -13,6 +13,8 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
+#ifndef KVM_HEADERS_H
+#define KVM_HEADERS_H 1
 
 #include <vmalloc.h>
 #include <alloc_page.h>
@@ -355,3 +357,4 @@ inline static parel1_t pack_par_el1(int pa, parel1_t p) {
     ((parel1_t)pa << OA_PACKED) |
     pack_flag(p, msk_f, 0);
 }
+#endif
diff --git a/litmus/libdir/_aarch64/kvm-self.c b/litmus/libdir/_aarch64/kvm-self.c
index b38ff8ad48..6eb47c4b90 100644
--- a/litmus/libdir/_aarch64/kvm-self.c
+++ b/litmus/libdir/_aarch64/kvm-self.c
@@ -16,8 +16,28 @@
 /* Authors:                                                                 */
 /* Nikos Nikoleris, Arm Limited.                                            */
 /****************************************************************************/
+#include <kvm-self.h>
+#include <_find_ins.h>
+#include <../kvm-headers.h>
 
-static void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
+static ins_t getret(void) {
+  ins_t *x1;
+  ins_t r;
+  asm __volatile__ (
+  "adr %[x1],0f\n\t"
+  "ldr %w[x2],[%[x1]]\n\t"
+  "b 1f\n"
+  "0:\n\t"
+  "ret\n"
+  "1:\n"
+:[x1] "=&r" (x1),[x2] "=&r" (r)
+:
+: "cc","memory"
+);
+  return r;
+}
+
+void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
 {
   while (vaddr < vaddr_end) {
     selfbar((void *)vaddr);
@@ -25,11 +45,11 @@ static void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
   }
 }
 
-static size_t code_size(ins_t *p,int skip) {
+size_t code_size(ins_t *p,int skip) {
   return (find_ins(getret(), p, skip) + 1) * sizeof(ins_t);
 }
 
-static void litmus_pte_unset_el0(uintptr_t vaddr, uintptr_t vaddr_end)
+void litmus_pte_unset_el0(uintptr_t vaddr, uintptr_t vaddr_end)
 {
   while (vaddr < vaddr_end) {
     pteval_t *pte = litmus_tr_pte((void *)vaddr);
@@ -43,7 +63,7 @@ static void litmus_pte_unset_el0(uintptr_t vaddr, uintptr_t vaddr_end)
   );
 }
 
-static void code_init(void *code, void *src, size_t sz)
+void code_init(void *code, void *src, size_t sz)
 {
   memcpy(code, src, sz);
   litmus_icache_sync((uintptr_t)code, (uintptr_t)code + sz);
diff --git a/litmus/libdir/_aarch64/kvm-self.h b/litmus/libdir/_aarch64/kvm-self.h
new file mode 100644
index 0000000000..68b765ea57
--- /dev/null
+++ b/litmus/libdir/_aarch64/kvm-self.h
@@ -0,0 +1,31 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef KVM_SELF_H
+#define KVM_SELF_H 1
+
+#include <stdint.h>
+#include <stddef.h>
+#include <instruction.h>
+#include <self.h>
+
+void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end);
+
+size_t code_size(ins_t *p,int skip);
+
+void litmus_pte_unset_el0(uintptr_t vaddr, uintptr_t vaddr_end);
+
+void code_init(void *code, void *src, size_t sz);
+#endif
diff --git a/litmus/libdir/_aarch64/kvm.c.rules b/litmus/libdir/_aarch64/kvm.c.rules
index 8d3e609198..010e960c62 100644
--- a/litmus/libdir/_aarch64/kvm.c.rules
+++ b/litmus/libdir/_aarch64/kvm.c.rules
@@ -1,5 +1,5 @@
 clean:
-	/bin/rm -f *.o *.s *.t *.elf *.flat *~ *.t $(H)
+	/bin/rm -f *.o lib/*.o *.s *.t *.elf *.flat *~ *.t $(H)
 
 %.s: %.c
 	$(CC) -DASS $(GCCOPTS) -S $<
@@ -15,7 +15,7 @@ clean:
 
 %.elf: LDFLAGS = -nostdlib -pie -n
 
-run.elf: run.o $(OBJ) $(UTILS) $(FLATLIBS) $(SRCDIR)/arm/flat.lds $(cstart.o)
+run.elf: run.o $(OBJ) $(UTILS) $(UTILS_OBJ) $(FLATLIBS) $(SRCDIR)/arm/flat.lds $(cstart.o)
 	$(CC) $(CFLAGS) -c -o $(@:.elf=.aux.o) $(SRCDIR)/lib/auxinfo.c \
 		-DPROGNAME=\"$(@:.elf=.flat)\" -DAUXFLAGS=$(AUXFLAGS)
 	$(LD) $(LDFLAGS) -o $@ -T $(SRCDIR)/arm/flat.lds \
diff --git a/litmus/libdir/_aarch64/kvm.rules b/litmus/libdir/_aarch64/kvm.rules
index 2e52b063da..7870c4b2a2 100644
--- a/litmus/libdir/_aarch64/kvm.rules
+++ b/litmus/libdir/_aarch64/kvm.rules
@@ -1,8 +1,8 @@
 clean:
-	/bin/rm -f *.o *.s *.t *.elf *.flat *~ $(H)
+	/bin/rm -f *.o lib/*.o *.s *.t *.elf *.flat *~ $(H)
 
 cleansource:
-	/bin/rm -f *.o *.c *.h *.s *~
+	/bin/rm -rf *.o *.c *.h *.s *~ lib
 
 %.s: %.c
 	$(CC) $(GCCOPTS) -S $<
@@ -13,7 +13,7 @@ cleansource:
 	awk -f show.awk $< > $@
 
 %.elf: LDFLAGS = -nostdlib -pie -n
-%.elf: %.o $(UTILS) $(FLATLIBS) $(SRCDIR)/arm/flat.lds $(cstart.o)
+%.elf: %.o $(UTILS) $(UTILS_OBJ) $(FLATLIBS) $(SRCDIR)/arm/flat.lds $(cstart.o)
 	$(CC) $(CFLAGS) -c -o $(@:.elf=.aux.o) $(SRCDIR)/lib/auxinfo.c \
 		-DPROGNAME=\"$(@:.elf=.flat)\" -DAUXFLAGS=$(AUXFLAGS)
 	$(LD) $(LDFLAGS) -o $@ -T $(SRCDIR)/arm/flat.lds \
@@ -25,3 +25,8 @@ cleansource:
 	$(call arch_elf_check, $^)
 	$(OBJCOPY) -O binary $^ $@
 	@chmod a-x $@
+
+.PRECIOUS: $(UTILS_OBJ)
+
+$(SHARED_SRC_DIR)/%.o: $(SHARED_SRC_DIR)/%.c
+	$(CC) $(GCCOPTS) -c -o $@ $<
\ No newline at end of file
diff --git a/litmus/libdir/_aarch64/kvm_fault_define.h b/litmus/libdir/_aarch64/kvm_fault_define.h
new file mode 100644
index 0000000000..ff8865b1aa
--- /dev/null
+++ b/litmus/libdir/_aarch64/kvm_fault_define.h
@@ -0,0 +1,20 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef KVM_FAULT_DEFINE_H
+#define KVM_FAULT_DEFINE_H 1
+#define MAX_FAULTS_PER_THREAD 8
+#endif
diff --git a/litmus/libdir/_aarch64/kvm_fault_handler.c b/litmus/libdir/_aarch64/kvm_fault_handler.h
similarity index 69%
rename from litmus/libdir/_aarch64/kvm_fault_handler.c
rename to litmus/libdir/_aarch64/kvm_fault_handler.h
index 7404a5c110..e3f8131583 100644
--- a/litmus/libdir/_aarch64/kvm_fault_handler.c
+++ b/litmus/libdir/_aarch64/kvm_fault_handler.h
@@ -1,6 +1,24 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
 /*********************/
 /* Handle MMU faults */
 /*********************/
+#ifndef KVM_FAULT_HANDLER_H
+#define KVM_FAULT_HANDLER_H 1
 
 #ifdef SEE_FAULTS
 static bool is_iabt(unsigned long esr)
@@ -89,3 +107,4 @@ static void install_fault_handler(int cpu) {
   ti->exception_handlers[EL0_SYNC_64][ESR_EL1_EC_PAC] = fault_handler;
 #endif
 }
+#endif
diff --git a/litmus/libdir/_aarch64/kvm_fault_type.c b/litmus/libdir/_aarch64/kvm_fault_type.c
index 04b21dcc34..a8fdc3aff0 100644
--- a/litmus/libdir/_aarch64/kvm_fault_type.c
+++ b/litmus/libdir/_aarch64/kvm_fault_type.c
@@ -1,31 +1,22 @@
-#define MAX_FAULTS_PER_THREAD 8
-
-enum fault_type_t {
-  FaultUndefinedInstruction,
-  FaultSupervisorCall,
-  FaultPacCheckIA,
-  FaultPacCheckIB,
-  FaultPacCheckDA,
-  FaultPacCheckDB,
-  FaultMMUAddressSize,
-  FaultMMUTranslation,
-  FaultMMUAccessFlag,
-  FaultMMUPermission,
-  FaultDMMUTranslation,
-  FaultDMMUAccessFlag,
-  FaultDMMUPermission,
-  FaultDMMUExclusive,
-  FaultIMMUTranslation,
-  FaultIMMUAccessFlag,
-  FaultIMMUPermission,
-  FaultIMMUExclusive,
-  FaultTagCheck,
-  FaultUnsupported,
-  FaultUnknown,
-  FaultTypes,
-};
-
-static const char *fault_type_names[] = {
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#include <kvm_fault_type.h>
+
+const char *fault_type_names[] = {
   "UndefinedInstruction",
   "SupervisorCall",
   "PacCheck:IA",
@@ -48,9 +39,7 @@ static const char *fault_type_names[] = {
   "Unsupported",
 };
 
-#define ESR_EL1_EC_PAC 0b011100
-
-static enum fault_type_t get_fault_type(unsigned long esr)
+enum fault_type_t get_fault_type(unsigned long esr)
 {
   unsigned int ec = esr >> ESR_EL1_EC_SHIFT;
   unsigned int fsc;
@@ -105,18 +94,7 @@ static enum fault_type_t get_fault_type(unsigned long esr)
   }
 }
 
-typedef struct {
-  int instr_symb;
-  int data_symb;
-  enum fault_type_t type;
-} fault_info_t;
-
-typedef struct {
-  fault_info_t faults[MAX_FAULTS_PER_THREAD];
-  int n;
-} th_faults_info_t;
-
-static void th_faults_info_init(th_faults_info_t *th_flts)
+void th_faults_info_init(th_faults_info_t *th_flts)
 {
   for (int i = 0; i < MAX_FAULTS_PER_THREAD; i++) {
     fault_info_t *f = &th_flts->faults[i];
@@ -127,7 +105,7 @@ static void th_faults_info_init(th_faults_info_t *th_flts)
   th_flts->n = 0;
 }
 
-static int th_faults_info_compare(th_faults_info_t *th_flts1, th_faults_info_t *th_flts2)
+int th_faults_info_compare(th_faults_info_t *th_flts1, th_faults_info_t *th_flts2)
 {
   if (th_flts1->n != th_flts2->n)
     return 0;
@@ -150,7 +128,7 @@ static int th_faults_info_compare(th_faults_info_t *th_flts1, th_faults_info_t *
   return 1;
 }
 
-static void pp_fault(int proc, int instr_symb, int data_symb, int ftype)
+void pp_fault(int proc, int instr_symb, int data_symb, int ftype, const char *instr_symb_name[], const char *data_symb_name[])
 {
   if (instr_symb != INSTR_SYMB_ID_UNKNOWN)
     printf("fault(P%s", instr_symb_name[instr_symb]);
@@ -163,19 +141,18 @@ static void pp_fault(int proc, int instr_symb, int data_symb, int ftype)
   printf(");");
 }
 
-static bool fault_reported[NTHREADS][MAX_FAULTS_PER_THREAD];
 
-static void pp_log_faults_init(void)
+void pp_log_faults_init(int nthreads, bool (*fault_reported)[MAX_FAULTS_PER_THREAD])
 {
-  for (int i = 0; i < NTHREADS; i++) {
+  for (int i = 0; i < nthreads; i++) {
     for (int j = 0; j < MAX_FAULTS_PER_THREAD; j++) {
       fault_reported[i][j] = false;
     }
   }
 }
 
-static void pp_log_faults(FILE *chan, th_faults_info_t *th_flts, int proc, int instr_symb,
-                          int data_symb, int ftype)
+void pp_log_faults(FILE *chan, th_faults_info_t *th_flts, int proc, int instr_symb,
+                   int data_symb, int ftype, bool (*fault_reported)[MAX_FAULTS_PER_THREAD], const char *instr_symb_name[], const char *data_symb_name[])
 {
   int found = 0;
   for (int i = 0; i < th_flts->n; i++) {
@@ -195,27 +172,27 @@ static void pp_log_faults(FILE *chan, th_faults_info_t *th_flts, int proc, int i
       printf(" ");
 
       if (!fault_reported[proc][i]) {
-        pp_fault(proc, flt->instr_symb, flt->data_symb, flt->type);
+        pp_fault(proc, flt->instr_symb, flt->data_symb, flt->type, instr_symb_name, data_symb_name);
         fault_reported[proc][i] = true;
       }
     }
   }
   if (!found) {
     printf(" ~");
-    pp_fault(proc, instr_symb, data_symb, ftype);
+    pp_fault(proc, instr_symb, data_symb, ftype, instr_symb_name, data_symb_name);
   }
 }
 
-static int eq_faults(th_faults_info_t *th_flts1, th_faults_info_t *th_flts2)
+int eq_faults(th_faults_info_t *th_flts1, th_faults_info_t *th_flts2, int nthreads)
 {
-  for (int i = 0; i < NTHREADS; i++) {
+  for (int i = 0; i < nthreads; i++) {
     if (!th_faults_info_compare(&th_flts1[i], &th_flts2[i]))
       return 0;
   }
   return 1;
 }
 
-static int exists_fault(th_faults_info_t *th_flts, int instr_symb, int data_symb, int ftype)
+int exists_fault(th_faults_info_t *th_flts, int instr_symb, int data_symb, int ftype)
 {
   for (int i = 0; i < th_flts->n; i++) {
     fault_info_t *flt = &th_flts->faults[i];
diff --git a/litmus/libdir/_aarch64/kvm_fault_type.h b/litmus/libdir/_aarch64/kvm_fault_type.h
new file mode 100644
index 0000000000..640ca5de62
--- /dev/null
+++ b/litmus/libdir/_aarch64/kvm_fault_type.h
@@ -0,0 +1,85 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2025-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef KVM_FAULT_TYPE_H
+#define KVM_FAULT_TYPE_H
+#include <arm64/asm/esr.h>
+#include <kvm_fault_define.h>
+#include <../utils.h>
+
+#ifndef INSTR_SYMB_ID_UNKNOWN
+#define INSTR_SYMB_ID_UNKNOWN 0
+#endif
+
+#ifndef DATA_SYMB_ID_UNKNOWN
+#define DATA_SYMB_ID_UNKNOWN 0
+#endif
+
+enum fault_type_t {
+  FaultUndefinedInstruction,
+  FaultSupervisorCall,
+  FaultPacCheckIA,
+  FaultPacCheckIB,
+  FaultPacCheckDA,
+  FaultPacCheckDB,
+  FaultMMUAddressSize,
+  FaultMMUTranslation,
+  FaultMMUAccessFlag,
+  FaultMMUPermission,
+  FaultDMMUTranslation,
+  FaultDMMUAccessFlag,
+  FaultDMMUPermission,
+  FaultDMMUExclusive,
+  FaultIMMUTranslation,
+  FaultIMMUAccessFlag,
+  FaultIMMUPermission,
+  FaultIMMUExclusive,
+  FaultTagCheck,
+  FaultUnsupported,
+  FaultUnknown,
+  FaultTypes,
+};
+
+#define ESR_EL1_EC_PAC 0b011100
+
+enum fault_type_t get_fault_type(unsigned long esr);
+
+typedef struct {
+  int instr_symb;
+  int data_symb;
+  enum fault_type_t type;
+} fault_info_t;
+
+typedef struct {
+  fault_info_t faults[MAX_FAULTS_PER_THREAD];
+  int n;
+} th_faults_info_t;
+
+void th_faults_info_init(th_faults_info_t *th_flts);
+
+int th_faults_info_compare(th_faults_info_t *th_flts1, th_faults_info_t *th_flts2);
+
+void pp_fault(int proc, int instr_symb, int data_symb, int ftype, const char *instr_symb_name[], const char *data_symb_name[]);
+
+void pp_log_faults_init(int nthreads, bool (*fault_reported)[MAX_FAULTS_PER_THREAD]);
+
+void pp_log_faults(FILE *chan, th_faults_info_t *th_flts, int proc, int instr_symb,
+                   int data_symb, int ftype, bool (*fault_reported)[MAX_FAULTS_PER_THREAD], const char *instr_symb_name[], const char *data_symb_name[]);
+
+int eq_faults(th_faults_info_t *th_flts1, th_faults_info_t *th_flts2, int nthreads);
+
+int exists_fault(th_faults_info_t *th_flts, int instr_symb, int data_symb, int ftype);
+#endif
diff --git a/litmus/libdir/_aarch64/kvm_timebase.c b/litmus/libdir/_aarch64/kvm_timebase.h
similarity index 95%
rename from litmus/libdir/_aarch64/kvm_timebase.c
rename to litmus/libdir/_aarch64/kvm_timebase.h
index 2f27ef6d7c..57065f18d0 100644
--- a/litmus/libdir/_aarch64/kvm_timebase.c
+++ b/litmus/libdir/_aarch64/kvm_timebase.h
@@ -13,7 +13,10 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
+#ifndef KVM_TIMEBASE_H
+#define KVM_TIMEBASE_H 1
 #include <asm/processor.h>
 inline static tb_t read_timebase(void) {
   return read_sysreg(cntpct_el0) ;
 }
+#endif
diff --git a/litmus/libdir/_aarch64/kvm_user_stacks.c b/litmus/libdir/_aarch64/kvm_user_stacks.c
deleted file mode 100644
index 12fdac4ef4..0000000000
--- a/litmus/libdir/_aarch64/kvm_user_stacks.c
+++ /dev/null
@@ -1,18 +0,0 @@
-/**************************/
-/* Setup user mode stacks */
-/**************************/
-
-#define USER_MODE 1
-
-static uint64_t user_stack[AVAIL];
-
-static void set_user_stack(int cpu) {
-  uint64_t sp_usr = (uint64_t)thread_stack_alloc();
-  sp_usr &= (~15UL); /* stack ptr needs 16-byte alignment */
-  //  printf("Cpu %d has stack 0x%" PRIx64 "\n",cpu,sp_usr);
-  struct thread_info *ti0 = current_thread_info();
-  struct thread_info *ti = thread_info_sp(sp_usr);
-  thread_info_init(ti, TIF_USER_MODE);
-  ti->pgtable = ti0->pgtable;
-  user_stack[cpu] = sp_usr;
-}
diff --git a/litmus/libdir/_aarch64/kvm_user_stacks.h b/litmus/libdir/_aarch64/kvm_user_stacks.h
new file mode 100644
index 0000000000..3e81287258
--- /dev/null
+++ b/litmus/libdir/_aarch64/kvm_user_stacks.h
@@ -0,0 +1,37 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris, France.                                       */
+/* Rémy Citérin, ARM Ltd, Cambridge, UK                                     */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+/**************************/
+/* Setup user mode stacks */
+/**************************/
+
+#ifndef KVM_USER_STACKS_H
+#define KVM_USER_STACKS_H 1
+#define USER_MODE 1
+
+static uint64_t user_stack[AVAIL];
+
+static void set_user_stack(int cpu) {
+  uint64_t sp_usr = (uint64_t)thread_stack_alloc();
+  sp_usr &= (~15UL); /* stack ptr needs 16-byte alignment */
+  //  printf("Cpu %d has stack 0x%" PRIx64 "\n",cpu,sp_usr);
+  struct thread_info *ti0 = current_thread_info();
+  struct thread_info *ti = thread_info_sp(sp_usr);
+  thread_info_init(ti, TIF_USER_MODE);
+  ti->pgtable = ti0->pgtable;
+  user_stack[cpu] = sp_usr;
+}
+#endif
diff --git a/litmus/libdir/_aarch64/presi-self.c b/litmus/libdir/_aarch64/presi-self.c
index f272c19f7e..eb4dcf203f 100644
--- a/litmus/libdir/_aarch64/presi-self.c
+++ b/litmus/libdir/_aarch64/presi-self.c
@@ -4,7 +4,7 @@
 /* Jade Alglave, University College London, UK.                             */
 /* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
 /*                                                                          */
-/* Copyright 2019-present Institut National de Recherche en Informatique et */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
 /* en Automatique and the authors. All rights reserved.                     */
 /*                                                                          */
 /* This software is governed by the CeCILL-B license under French law and   */
@@ -16,8 +16,28 @@
 /* Authors:                                                                 */
 /* Nikos Nikoleris, Arm Limited.                                            */
 /****************************************************************************/
+#include <self.h>
+#include <presi-self.h>
+#include <_find_ins.h>
 
-static void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
+static ins_t getret(void) {
+  ins_t *x1;
+  ins_t r;
+  asm __volatile__ (
+  "adr %[x1],0f\n\t"
+  "ldr %w[x2],[%[x1]]\n\t"
+  "b 1f\n"
+  "0:\n\t"
+  "ret\n"
+  "1:\n"
+:[x1] "=&r" (x1),[x2] "=&r" (r)
+:
+: "cc","memory"
+);
+  return r;
+}
+
+void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
 {
   while (vaddr < vaddr_end) {
     selfbar((void *)vaddr);
@@ -25,11 +45,11 @@ static void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end)
   }
 }
 
-static size_t code_size(ins_t *p,int skip) {
+size_t code_size(ins_t *p,int skip) {
   return (find_ins(getret(), p, skip) + 1) * sizeof(ins_t);
 }
 
-static void code_init(void *code, void *src, size_t sz)
+void code_init(void *code, void *src, size_t sz)
 {
   memcpy(code, src, sz);
   litmus_icache_sync((uintptr_t)code, (uintptr_t)code + sz);
diff --git a/litmus/libdir/_aarch64/presi-self.h b/litmus/libdir/_aarch64/presi-self.h
new file mode 100644
index 0000000000..b925789a63
--- /dev/null
+++ b/litmus/libdir/_aarch64/presi-self.h
@@ -0,0 +1,23 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef PRESI_SELF_H
+#define PRESI_SELF_H 1
+void litmus_icache_sync(uintptr_t vaddr, uintptr_t vaddr_end);
+
+size_t code_size(ins_t *p,int skip);
+
+void code_init(void *code, void *src, size_t sz);
+#endif
diff --git a/litmus/libdir/_aarch64/self.c b/litmus/libdir/_aarch64/self.c
index b934560270..9cd23ab0ef 100644
--- a/litmus/libdir/_aarch64/self.c
+++ b/litmus/libdir/_aarch64/self.c
@@ -4,7 +4,7 @@
 /* Jade Alglave, University College London, UK.                             */
 /* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
 /*                                                                          */
-/* Copyright 2019-present Institut National de Recherche en Informatique et */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
 /* en Automatique and the authors. All rights reserved.                     */
 /*                                                                          */
 /* This software is governed by the CeCILL-B license under French law and   */
@@ -17,8 +17,13 @@
 /***********************************/
 /* Support for self-modifying code */
 /***********************************/
+#include <stdlib.h>
+#include <self.h>
+#include <../utils.h>
 
-static uint32_t getcachelinesize(void) {
+uint32_t cache_line_size;
+
+uint32_t getcachelinesize(void) {
   uint64_t csz;
   asm __volatile__ (
                     "mrs %[r],CTR_EL0"
@@ -32,19 +37,17 @@ static uint32_t getcachelinesize(void) {
   return (1 << x) * 4 ;
 }
 
-static uint32_t cache_line_size;
-
-inline static void selfbar(void *p) {
+void selfbar(void *p) {
   asm __volatile__
     ("dc cvau,%[p]\n\t" "dsb ish\n\t" "ic ivau,%[p]\n\t" "dsb ish\n\t" "isb"
      ::[p]"r"(p): "memory");
 }
 
-inline static void isync(void) {
+void isync(void) {
   asm __volatile__ ("isb" ::: "memory");
 }
 
-inline static void check_dic_idc(int need_dic, int need_idc) {
+void check_dic_idc(int need_dic, int need_idc) {
   uint64_t ctr_el0;
   asm volatile ("mrs %0, ctr_el0" : "=r" (ctr_el0));
   int idc = (ctr_el0 >> 28) & 1;
diff --git a/litmus/libdir/_aarch64/self.h b/litmus/libdir/_aarch64/self.h
new file mode 100644
index 0000000000..e631d0c3fe
--- /dev/null
+++ b/litmus/libdir/_aarch64/self.h
@@ -0,0 +1,34 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+
+/***********************************/
+/* Support for self-modifying code */
+/***********************************/
+#ifndef SELF_H
+#define SELF_H 1
+#include <stdint.h>
+
+
+uint32_t getcachelinesize(void);
+
+extern uint32_t cache_line_size;
+
+void selfbar(void *p);
+
+void isync(void);
+
+void check_dic_idc(int need_dic, int need_idc);
+#endif
diff --git a/litmus/libdir/_arm/instruction.h b/litmus/libdir/_arm/instruction.h
index 9284c75901..582ae6c5f4 100644
--- a/litmus/libdir/_arm/instruction.h
+++ b/litmus/libdir/_arm/instruction.h
@@ -1 +1,3 @@
+#include <stdint.h>
+
 typedef uint32_t ins_t; /* Type of instructions */
diff --git a/litmus/libdir/_find_ins.c b/litmus/libdir/_find_ins.c
index 14d14a038c..aa80eae2fe 100644
--- a/litmus/libdir/_find_ins.c
+++ b/litmus/libdir/_find_ins.c
@@ -13,8 +13,10 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
+#include <_find_ins.h>
+
 // Find index of some instruction in code, skipping 'skip' occurrences
-static size_t find_ins(ins_t opcode,ins_t *p,int skip) {
+size_t find_ins(ins_t opcode,ins_t *p,int skip) {
   ins_t *q = p;
 
   for  ( ; *q != opcode || (skip-- > 0); q++);
diff --git a/litmus/libdir/_find_ins.h b/litmus/libdir/_find_ins.h
new file mode 100644
index 0000000000..e1c1ed2c38
--- /dev/null
+++ b/litmus/libdir/_find_ins.h
@@ -0,0 +1,23 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2020-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef _FIND_INS_H
+#define _FIND_INS_H 1
+#include <instruction.h>
+#include <stddef.h>
+
+// Find index of some instruction in code, skipping 'skip' occurrences
+size_t find_ins(ins_t opcode,ins_t *p,int skip);
+#endif
diff --git a/litmus/libdir/_hash.c b/litmus/libdir/_hash.c
index 70cafc2cb2..11f163528b 100644
--- a/litmus/libdir/_hash.c
+++ b/litmus/libdir/_hash.c
@@ -16,24 +16,10 @@
 
 /* Notice: this file contains public domain code by Bob Jenkins */
 
-typedef struct {
-  log_t key ;
-#ifdef STATS
-  param_t p ;
-#endif
-  count_t c ;
-  int ok ;
-} entry_t ;
-
-static void pp_entry(FILE *out,entry_t *p, int verbose, const char **group) ;
-
-typedef struct {
-  int nhash ;
-  entry_t t[HASHSZ] ;
-} hash_t ;
+#include <_hash.h>
 
-static void pp_hash(FILE *fp,hash_t *t,int verbose,const char **group) {
-  for (int k = 0 ; k < HASHSZ ; k++) {
+void pp_hash(FILE *fp,hash_t *t,int verbose,const char **group, void (*pp_entry)(FILE *, entry_t *, int, const char **)) {
+  for (int k = 0 ; k < t->hashsz ; k++) {
     entry_t *p = t->t+k ;
     if (p->c > 0) {
       pp_entry(fp,p,verbose,group) ;
@@ -42,26 +28,28 @@ static void pp_hash(FILE *fp,hash_t *t,int verbose,const char **group) {
 }
 
 #if 0
-static void pp_hash_ok(FILE *fp,hash_t *t,char **group) {
-  for (int k = 0 ; k < HASHSZ ; k++) {
+void pp_hash_ok(FILE *fp,hash_t *t,char **group) {
+  for (int k = 0 ; k < t->hashsz ; k++) {
     entry_t *p = t->t+k ;
     if (p->c > 0 && p->ok) pp_entry(fp,p,1,group) ;
   }
 }
 #endif
 
-static void log_init(log_t *p) {
+void log_init(log_t *p, size_t log_t_size) {
   uint32_t *q = (uint32_t *)p ;
 
-  for (int k = sizeof(log_t)/sizeof(uint32_t) ; k > 0 ; k--)
+  for (int k = log_t_size/sizeof(uint32_t) ; k > 0 ; k--)
     *q++ = -1 ;
 }
 
-static void hash_init(hash_t *t) {
+void hash_init(hash_t *t, int hashsz, entry_t *hash, size_t log_t_size) {
   t->nhash = 0 ;
-  for (int k = 0 ; k < HASHSZ ; k++) {
+  t->hashsz = hashsz ;
+  t->t = hash;
+  for (int k = 0 ; k < hashsz ; k++) {
     t->t[k].c = 0 ;
-    log_init(&t->t[k].key) ;
+    log_init(t->t[k].key, log_t_size) ;
   }
 }
 
@@ -127,48 +115,38 @@ size_t          length)              /* the length of the key, in uint32_ts */
   return c;
 }
 
-static uint32_t hash_log (log_t *key) {
-  return hashword((uint32_t *)key,sizeof(log_t)/sizeof(uint32_t)) ;
+uint32_t hash_log (log_t *key, size_t log_t_size) {
+  return hashword((uint32_t *)key,log_t_size/sizeof(uint32_t)) ;
 }
 
-#ifdef STATS
-static int hash_add(hash_t *t,log_t *key, param_t *v,count_t c,int ok) {
-#else
-static int hash_add(hash_t *t,log_t *key, count_t c,int ok) {
-#endif
-  uint32_t h = hash_log(key) ;
-  h = h % HASHSZ ;
-  for (int k = 0 ; k < HASHSZ ;  k++) {
+int hash_add(hash_t *t,log_t *key, param_t *v,count_t c,int ok, int (*eq_log)(log_t *, log_t *), size_t log_t_size) {
+  uint32_t h = hash_log(key, log_t_size) ;
+  h = h % t->hashsz ;
+  for (int k = 0 ; k < t->hashsz ;  k++) {
     entry_t *p = t->t + h ;
     if (p->c == 0) { /* New entry */
-      p->key = *key ;
-#ifdef STATS
+      p->key = key ;
       p->p = *v ;
-#endif
       p->c = c ;
       p->ok = ok ;
       t->nhash++ ;
       return 1 ;
-    } else if (eq_log(key,&p->key)) {
+    } else if (eq_log(key,p->key)) {
       p->c += c ;
       return 1;
     }
     h++ ;
-    h %= HASHSZ ;
+    h %= t->hashsz ;
   }
   return 0;
 }
 
-static int hash_adds(hash_t *t, hash_t *f) {
+int hash_adds(hash_t *t, hash_t *f, int (*eq_log)(log_t *, log_t *), size_t log_t_size) {
   int r = 1;
-  for (int k = 0 ; k < HASHSZ ; k++) {
+  for (int k = 0 ; k < t->hashsz ; k++) {
     entry_t *p = f->t+k ;
     if (p->c > 0) {
-#ifdef STATS
-      int rloc = hash_add(t,&p->key,&p->p,p->c,p->ok) ;
-#else
-      int rloc = hash_add(t,&p->key,p->c,p->ok) ;
-#endif
+      int rloc = hash_add(t,p->key,&p->p,p->c,p->ok, eq_log, log_t_size) ;
       r = r && rloc;
     }
   }
diff --git a/litmus/libdir/_hash.h b/litmus/libdir/_hash.h
new file mode 100644
index 0000000000..9d7c2d79c3
--- /dev/null
+++ b/litmus/libdir/_hash.h
@@ -0,0 +1,54 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2015-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+
+/* Notice: this file contains public domain code by Bob Jenkins */
+#ifndef _HASH_H
+#define _HASH_H 1
+#include <../utils.h>
+#ifndef KVM
+#include <stdio.h>
+#endif
+#include <log.h>
+#include <param.h>
+#include <count.h>
+#include <stdint.h>
+#include <stddef.h>
+
+typedef struct {
+  log_t *key ;
+  param_t p ;
+  count_t c ;
+  int ok ;
+} entry_t ;
+
+typedef struct {
+  int nhash ;
+  int hashsz ;
+  entry_t *t ;
+} hash_t ;
+
+void pp_hash(FILE *fp,hash_t *t,int verbose,const char **group, void (*pp_entry)(FILE *, entry_t *, int, const char **));
+
+void log_init(log_t *p, size_t log_t_size);
+
+void hash_init(hash_t *t, int hashsz, entry_t *hash, size_t log_t_size);
+
+uint32_t hash_log (log_t *key, size_t log_t_size);
+
+int hash_add(hash_t *t,log_t *key, param_t *v,count_t c,int ok, int (*eq_log)(log_t *, log_t *), size_t log_t_size);
+
+int hash_adds(hash_t *t, hash_t *f, int (*eq_log)(log_t *, log_t *), size_t log_t_size);
+#endif
diff --git a/litmus/libdir/_instance.c b/litmus/libdir/_instance.h
similarity index 96%
rename from litmus/libdir/_instance.c
rename to litmus/libdir/_instance.h
index 8a768d7e79..ed96a9d73a 100644
--- a/litmus/libdir/_instance.c
+++ b/litmus/libdir/_instance.h
@@ -17,6 +17,9 @@
 /************/
 /* Instance */
 /************/
+#ifndef _INSTANCE_H
+#define _INSTANCE_H 1
+#include <_hash.h>
 
 typedef struct {
   int id ;
@@ -42,10 +45,11 @@ typedef struct {
 static void instance_init(ctx_t *p, int id, intmax_t *mem) {
   p->id = id;
   p->mem = mem;
-  hash_init(&p->t);
-  log_init(&p->out);
+  hash_init(&p->t, HASHSZ, instance_hash[id], sizeof(log_t));
+  log_init(&p->out, sizeof(log_t));
   barrier_init(&p->b,N);
   interval_init((int *)&p->ind,N);
+  p->p.tags = instance_tags[id];
   p->stop_now = 0;
 #ifdef SOME_VARS
   vars_init(&p->v,mem);
@@ -210,3 +214,4 @@ static void set_role(global_t *g,thread_ctx_t *c,int part) {
 #endif
   barrier_wait(&g->gb) ;
 }
+#endif
diff --git a/litmus/libdir/_main.c b/litmus/libdir/_main.c
index e97d88332a..bc78ab791f 100644
--- a/litmus/libdir/_main.c
+++ b/litmus/libdir/_main.c
@@ -34,6 +34,21 @@ int RUN(int argc,char **argv,FILE *out) {
   if (!feature_check()) {
     return -1;
   }
+  for (int k = 0; k < HASHSZ; k++) {
+    main_hash[k].key = &main_hash_log[k];
+#ifdef STATS
+    main_hash[k].p.tags = hash_main_tags[k];
+#endif
+  }
+
+  for (int k = 0; k < NEXE; k++) {
+    for (int j = 0; j < HASHSZ; j++) {
+       instance_hash[k][j].key = &instance_hash_log[k][j];
+#ifdef STATS
+       instance_hash[k][j].p.tags = hash_instance_tags[k][j];
+#endif
+    }
+  }
 #ifdef DYNALLOC
 #ifdef HAVE_FAULT_HANDLER
   alloc_fault_handler();
@@ -51,6 +66,7 @@ int RUN(int argc,char **argv,FILE *out) {
   global_t *glo_ptr = &global;
   glo_ptr->mem = mem;
 #endif
+  glo_ptr->hash.t = main_hash;
   init_getinstrs();
   init_global(glo_ptr);
 #ifdef OUT
@@ -113,9 +129,9 @@ int RUN(int argc,char **argv,FILE *out) {
   for (int id=0; id < AVAIL ; id++) join(&th[id]);
 #endif
   int nexe = glo_ptr->nexe ;
-  hash_init(&glo_ptr->hash) ;
+  hash_init(&glo_ptr->hash, HASHSZ, main_hash, sizeof(log_t)) ;
   for (int k=0 ; k < nexe ; k++) {
-    glo_ptr->hash_ok = hash_adds(&glo_ptr->hash,&glo_ptr->ctx[k].t) && glo_ptr->hash_ok ;
+    glo_ptr->hash_ok = hash_adds(&glo_ptr->hash,&glo_ptr->ctx[k].t, eq_log, sizeof(log_t)) && glo_ptr->hash_ok ;
   }
 #ifdef OUT
   tsc_t total = timeofday()-start;
diff --git a/litmus/libdir/_mips/instruction.h b/litmus/libdir/_mips/instruction.h
index 9284c75901..7182be28c1 100644
--- a/litmus/libdir/_mips/instruction.h
+++ b/litmus/libdir/_mips/instruction.h
@@ -1 +1,21 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef INSTRUCTION_H
+#define INSTRUCTION_H 1
+#include <stdint.h>
+
 typedef uint32_t ins_t; /* Type of instructions */
+#endif
diff --git a/litmus/libdir/_ppc/instruction.h b/litmus/libdir/_ppc/instruction.h
index 9284c75901..289bf7f416 100644
--- a/litmus/libdir/_ppc/instruction.h
+++ b/litmus/libdir/_ppc/instruction.h
@@ -1 +1,21 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2026-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+#ifndef INSTRUCTION_H
+#define INSTRUCTION_H
+#include <stdint.h>
+
 typedef uint32_t ins_t; /* Type of instructions */
+#endif
diff --git a/litmus/libdir/_prelude_size.c b/litmus/libdir/_prelude_size.c
index b0740db946..a77599628f 100644
--- a/litmus/libdir/_prelude_size.c
+++ b/litmus/libdir/_prelude_size.c
@@ -1,2 +1,5 @@
-static size_t prelude_size(ins_t *p) { return find_ins(nop,p,0); }
+#include <_find_ins.h>
+#include <_prelude_size.h>
+ins_t nop;
 
+size_t prelude_size(ins_t *p) { return find_ins(nop,p,0); }
diff --git a/litmus/libdir/_prelude_size.h b/litmus/libdir/_prelude_size.h
new file mode 100644
index 0000000000..69a383b1ae
--- /dev/null
+++ b/litmus/libdir/_prelude_size.h
@@ -0,0 +1,8 @@
+#ifndef _PRELUDE_SIZE_H
+#define _PRELUDE_SIZE_H
+#include <instruction.h>
+#include <stddef.h>
+extern ins_t nop; /* shared by ALL test cases */
+
+size_t prelude_size(ins_t *p);
+#endif
diff --git a/litmus/libdir/_x86/barrier.c b/litmus/libdir/_x86/barrier.c
index 4f7a548604..8f2ed8fb56 100644
--- a/litmus/libdir/_x86/barrier.c
+++ b/litmus/libdir/_x86/barrier.c
@@ -16,19 +16,14 @@
 /**********************/
 /* User level barrier */
 /**********************/
+#include <barrier.h>
 
-typedef struct {
-  volatile int c,sense ;
-  int n ;
-} sense_t ;
-
-
-static void barrier_init(sense_t *p, int n) {
+void barrier_init(sense_t *p, int n) {
   p->n = p->c = n ;
   p->sense = 0 ;
 }
 
-static void barrier_wait(sense_t *p) {
+void barrier_wait(sense_t *p) {
   int sense = p->sense ;
   int r1 ;
   asm __volatile__ (
diff --git a/litmus/libdir/_x86/barrier.h b/litmus/libdir/_x86/barrier.h
new file mode 100644
index 0000000000..147c389265
--- /dev/null
+++ b/litmus/libdir/_x86/barrier.h
@@ -0,0 +1,31 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2015-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+/**********************/
+/* User level barrier */
+/**********************/
+#ifndef BARRIER_H
+#define BARRIER_H 1
+
+typedef struct {
+  volatile int c,sense ;
+  int n ;
+} sense_t ;
+
+
+void barrier_init(sense_t *p, int n);
+
+void barrier_wait(sense_t *p);
+#endif
diff --git a/litmus/libdir/_x86/timebase.c b/litmus/libdir/_x86/timebase.h
similarity index 96%
rename from litmus/libdir/_x86/timebase.c
rename to litmus/libdir/_x86/timebase.h
index 2a0d17112d..e9386cfede 100644
--- a/litmus/libdir/_x86/timebase.c
+++ b/litmus/libdir/_x86/timebase.h
@@ -13,8 +13,11 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
+#ifndef TIMEBASE_H
+#define TIMEBASE_H 1
 inline static tb_t read_timebase(void) {
   uint32_t a,d; ;
   asm __volatile__ ("rdtsc" : "=a" (a), "=d" (d)) ;
   return ((tb_t)a) | (((tb_t)d)<<32);
 }
+#endif
diff --git a/litmus/libdir/_x86_64/barrier.h b/litmus/libdir/_x86_64/barrier.h
new file mode 120000
index 0000000000..fb3ca09a66
--- /dev/null
+++ b/litmus/libdir/_x86_64/barrier.h
@@ -0,0 +1 @@
+../_x86/barrier.h
\ No newline at end of file
diff --git a/litmus/libdir/_x86_64/kvm-headers.h b/litmus/libdir/_x86_64/kvm-headers.h
index c461f0a4b8..85b885216f 100644
--- a/litmus/libdir/_x86_64/kvm-headers.h
+++ b/litmus/libdir/_x86_64/kvm-headers.h
@@ -13,7 +13,8 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
-
+#ifndef KVM_HEADERS_H
+#define KVM_HEADERS_H 1
 
 #include<libcflat.h>
 #include <vmalloc.h>
@@ -54,3 +55,4 @@ static inline void litmus_flush_tlb(void *_p) {
 static inline pteval_t litmus_set_pte_safe(void *q,pteval_t *p,pteval_t x) {
   return litmus_set_pte(p,x);
 }
+#endif
diff --git a/litmus/libdir/_x86_64/kvm.c.rules b/litmus/libdir/_x86_64/kvm.c.rules
index 362b57b4ce..2fc05e4694 100644
--- a/litmus/libdir/_x86_64/kvm.c.rules
+++ b/litmus/libdir/_x86_64/kvm.c.rules
@@ -1,5 +1,5 @@
 clean:
-	/bin/rm -f *.o *.s *.t *.elf *.flat *~ *.t $(H)
+	/bin/rm -f *.o lib/*.o *.s *.t *.elf *.flat *~ *.t $(H)
 
 %.s: %.c
 	$(CC) -DASS $(GCCOPTS) -S $<
@@ -13,7 +13,7 @@ clean:
 %.h: %.t
 	sh toh.sh $< > $@
 
-run.elf: run.o $(OBJ) $(UTILS) $(FLATLIBS) $(SRCDIR)/x86/flat.lds $(cstart.o)
+run.elf: run.o $(OBJ) $(UTILS) $(UTILS_OBJ) $(FLATLIBS) $(SRCDIR)/x86/flat.lds $(cstart.o)
 	$(CC) $(GCCOPTS) -nostdlib -o $@ -Wl,-T,$(SRCDIR)/x86/flat.lds $(filter %.o, $^) $(FLATLIBS)
 	@chmod a-x $@
 
diff --git a/litmus/libdir/_x86_64/kvm.rules b/litmus/libdir/_x86_64/kvm.rules
index c0cb888eb2..dc821731bb 100644
--- a/litmus/libdir/_x86_64/kvm.rules
+++ b/litmus/libdir/_x86_64/kvm.rules
@@ -1,8 +1,8 @@
 clean:
-	/bin/rm -f *.o *.s *.t *.elf *.flat *~
+	/bin/rm -f *.o lib/*.o *.s *.t *.elf *.flat *~
 
 cleansource:
-	/bin/rm -f *.o *.c *.h *.s *~
+	/bin/rm -rf *.o *.c *.h *.s *~ lib
 
 %.s: %.c
 	$(CC) $(GCCOPTS) -S $<
@@ -12,10 +12,13 @@ cleansource:
 %.t: %.s
 	awk -f show.awk $< > $@
 
-%.elf: %.o $(UTILS) $(FLATLIBS) $(SRCDIR)/x86/flat.lds $(cstart.o)
+%.elf: %.o $(UTILS) $(UTILS_OBJ) $(FLATLIBS) $(SRCDIR)/x86/flat.lds $(cstart.o)
 	$(CC) $(GCCOPTS) -nostdlib -o $@ -Wl,-T,$(SRCDIR)/x86/flat.lds  $(filter %.o, $^) $(FLATLIBS)
 	@chmod a-x $@
 
 %.flat: %.elf
 	$(OBJCOPY) -O  elf32-i386 $^ $@
 	@chmod a-x $@
+
+$(SHARED_SRC_DIR)/%.o: $(SHARED_SRC_DIR)/%.c
+	$(CC) $(GCCOPTS) -c -o $@ $<
\ No newline at end of file
diff --git a/litmus/libdir/_x86_64/kvm_timebase.c b/litmus/libdir/_x86_64/kvm_timebase.h
similarity index 96%
rename from litmus/libdir/_x86_64/kvm_timebase.c
rename to litmus/libdir/_x86_64/kvm_timebase.h
index 79c1185d31..ca07e516e5 100644
--- a/litmus/libdir/_x86_64/kvm_timebase.c
+++ b/litmus/libdir/_x86_64/kvm_timebase.h
@@ -13,6 +13,8 @@
 /* license as circulated by CEA, CNRS and INRIA at the following URL        */
 /* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
 /****************************************************************************/
+#ifndef KVM_TIMEBASE_H
+#define KVM_TIMEBASE_H 1
 
 inline static tb_t read_timebase(void) {
   uint32_t a,d; ;
@@ -20,3 +22,4 @@ inline static tb_t read_timebase(void) {
   tb_t r = ((tb_t)a) | (((tb_t)d)<<32);
   return r ;
 }
+#endif
diff --git a/litmus/libdir/_x86_64/timebase.c b/litmus/libdir/_x86_64/timebase.c
deleted file mode 120000
index a75ca01b1e..0000000000
--- a/litmus/libdir/_x86_64/timebase.c
+++ /dev/null
@@ -1 +0,0 @@
-../_x86/timebase.c
\ No newline at end of file
diff --git a/litmus/libdir/_x86_64/timebase.h b/litmus/libdir/_x86_64/timebase.h
new file mode 120000
index 0000000000..c6dcdc770c
--- /dev/null
+++ b/litmus/libdir/_x86_64/timebase.h
@@ -0,0 +1 @@
+../_x86/timebase.h
\ No newline at end of file
diff --git a/litmus/libdir/count.h b/litmus/libdir/count.h
new file mode 100644
index 0000000000..a83e4d7302
--- /dev/null
+++ b/litmus/libdir/count.h
@@ -0,0 +1,22 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2015-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+
+/* Notice: this file contains public domain code by Bob Jenkins */
+#ifndef COUNT_H
+#define COUNT_H
+#include <stdint.h>
+typedef uint32_t count_t;
+#endif
diff --git a/litmus/libdir/kvm-aarch64.cfg b/litmus/libdir/kvm-aarch64.cfg
index 1827c8370e..204f09db9d 100644
--- a/litmus/libdir/kvm-aarch64.cfg
+++ b/litmus/libdir/kvm-aarch64.cfg
@@ -13,7 +13,7 @@ ascall = true
 mode = kvm
 delay = 32
 makevar = AUXFLAGS=0x0
-makevar = SRCDIR=$(PWD)/..
+makevar = SRCDIR=$(CURDIR)/..
 makevar = -include $(SRCDIR)/config.mak
 makevar = libcflat = $(SRCDIR)/lib/libcflat.a
 makevar = libeabi = $(SRCDIR)/lib/arm/libeabi.a
diff --git a/litmus/libdir/log.h b/litmus/libdir/log.h
new file mode 100644
index 0000000000..3bafc1f12f
--- /dev/null
+++ b/litmus/libdir/log.h
@@ -0,0 +1,21 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2015-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+
+/* Notice: this file contains public domain code by Bob Jenkins */
+#ifndef LOG_H
+#define LOG_H
+typedef struct log_t log_t;
+#endif
diff --git a/litmus/libdir/param.h b/litmus/libdir/param.h
new file mode 100644
index 0000000000..4987e6bf1d
--- /dev/null
+++ b/litmus/libdir/param.h
@@ -0,0 +1,24 @@
+/****************************************************************************/
+/*                           the diy toolsuite                              */
+/*                                                                          */
+/* Jade Alglave, University College London, UK.                             */
+/* Luc Maranget, INRIA Paris-Rocquencourt, France.                          */
+/*                                                                          */
+/* Copyright 2015-present Institut National de Recherche en Informatique et */
+/* en Automatique and the authors. All rights reserved.                     */
+/*                                                                          */
+/* This software is governed by the CeCILL-B license under French law and   */
+/* abiding by the rules of distribution of free software. You can use,      */
+/* modify and/ or redistribute the software under the terms of the CeCILL-B */
+/* license as circulated by CEA, CNRS and INRIA at the following URL        */
+/* "http://www.cecill.info". We also give a copy in LICENSE.txt.            */
+/****************************************************************************/
+
+/* Notice: this file contains public domain code by Bob Jenkins */
+#ifndef PARAM_H
+#define PARAM_H
+typedef struct {
+  int part;
+  int *tags;
+} param_t;
+#endif
diff --git a/litmus/litmus.ml b/litmus/litmus.ml
index 02c3859897..3008d52bea 100644
--- a/litmus/litmus.ml
+++ b/litmus/litmus.ml
@@ -379,7 +379,7 @@ let () =
       let asmcomment = !asmcomment
       let asmcommentaslabel = !asmcommentaslabel
     end in
-     let module T = Top_litmus.Top (Config) (Tar) in
+    let module T = Top_litmus.Top (Config) (Tar) in
     T.from_files sources ;
     if not (Option.is_out ()) then MySys.rmdir outname ;
     exit 0
diff --git a/litmus/myName.ml b/litmus/myName.ml
index 27981d1b1a..9eec9db10d 100644
--- a/litmus/myName.ml
+++ b/litmus/myName.ml
@@ -22,6 +22,8 @@
 let chop_litmus source =
   if Filename.check_suffix source ".litmus" then
     Filename.chop_extension source
+  else if Filename.check_suffix source ".litmus_def" then
+    (Filename.chop_extension source) ^ "_def"
   else
     source
 
diff --git a/litmus/objUtil.ml b/litmus/objUtil.ml
index 488b8837a3..e8a725b46f 100644
--- a/litmus/objUtil.ml
+++ b/litmus/objUtil.ml
@@ -158,6 +158,9 @@ module Make(O:Config)(Tar:Tar.S) =
       close_in in_chan ;
       fnames
 
+(* Reference to the shared library *)
+    let libdir = "lib/"
+
 (* Copy lib file *)
     let cpy ?sub ?prf fnames name ext =
       do_cpy ?sub ?prf fnames ("_" ^ name) name ext
@@ -182,6 +185,9 @@ module Make(O:Config)(Tar:Tar.S) =
     | Mac as os ->
         Warn.fatal "Affinity not implemented for %s" (TargetOS.pp os)
 
+(* Create shared library directory *)
+    let mk_libdir = MySys.mkdirp (Tar.outname libdir)
+
     let dump flags =
       let fnames = [] in
       let fnames = match O.driver with
@@ -245,7 +251,7 @@ module Make(O:Config)(Tar:Tar.S) =
           let fnames = cpy fnames "kvm_timeofday" ".h" in
           let module I = Insert(O) in
           I.copy "kvm_timeofday.c" Tar.outname ;
-          I.copy "kvm-headers.h" Tar.outname ;
+          I.copy "kvm-headers.h" Tar.outname;
           fnames in
       let fnames =
         match O.mode with
diff --git a/litmus/preSi.ml b/litmus/preSi.ml
index 7d9a8765c8..14cf3f0d09 100644
--- a/litmus/preSi.ml
+++ b/litmus/preSi.ml
@@ -63,10 +63,15 @@ module Make
      and module FaultType = A.FaultType)
     (O:Indent.S)
     (Lang:Language.S with type t = A.Out.t)
+    (OO:ObjUtil.Config)
+    (Tar:Tar.S)
        : sig
       val dump : Name.t -> T.t -> unit
     end = struct
 
+(* ObjUtil (required for copying and pasting files to the relevant directory) *)
+  module Obj = ObjUtil.Make(OO)(Tar)
+
 (* Non valid mode for presi *)
   let () =
     if Cfg.variant Variant_litmus.NoInit then
@@ -146,9 +151,9 @@ module Make
 
       let timebase_possible =
         if Cfg.is_kvm then
-          Insert.exists "kvm_timebase.c"
+          Insert.exists "kvm_timebase.h"
         else
-          Insert.exists "timebase.c"
+          Insert.exists "timebase.h"
 
       let have_timebase =
         Cfg.is_tb &&
@@ -166,7 +171,7 @@ module Make
 (* Utilities *)
 (*************)
 
-      let have_fault_handler = Cfg.is_kvm && Insert.exists "kvm_fault_handler.c"
+      let have_fault_handler = Cfg.is_kvm && Insert.exists "kvm_fault_handler.h"
 
       module UCfg = struct
         let memory = Memory.Direct
@@ -187,6 +192,17 @@ module Make
       module UD = U.Dump(O)(EPF)
       module PU = SkelUtil.PteValUtil(A.V.PteVal)
 
+      let arch_dir = 
+        match UCfg.sysarch with
+        | `AArch64 -> "_aarch64/"
+        | `ARM     -> "_arm/"
+        | `MIPS    -> "_mips/"
+        | `PPC     -> "_ppc/"
+        | `X86     -> "_x86/"
+        | `RISCV   -> "_riscv/"
+        | `X86_64  -> "_x86_64/"
+        | _        -> ""
+
       let find_addr_type a env = U.find_type (A.location_of_addr a) env
       let see_faults test = Misc.consp (U.get_faults test)
       let see_faults_with_loc test =
@@ -267,16 +283,26 @@ module Make
             end
           end
         end ;
-        Insert.insert_when_exists O.o "intrinsics.h" ;
+        if Insert.exists "intrinsics.h" then begin
+          let fname = "intrinsics" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
+          O.o ""
+        end ;
+        (* Insert.insert_when_exists O.o "intrinsics.h" ; *)
         if Cfg.variant Variant_litmus.MemTag then begin
           O.o "#include \"memtag.h\""
-        end;
+        end ;
         if Cfg.variant Variant_litmus.Pac then begin
           O.o "#include \"auth.h\""
         end;
         O.o "#include \"cache.h\"" ;
         O.o "" ;
-        O.o "typedef uint32_t count_t;" ;
+        let fname = "count" in
+        ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+        O.o ("#include <" ^ fname ^ ".h>") ;
+        O.o "" ;
+        (*O.o "typedef uint32_t count_t;" ;*)
         O.o "#define PCTR PRIu32" ;
         O.o "" ;
         begin match Cfg.timelimit with
@@ -287,6 +313,21 @@ module Make
         O.o "" ;
         ()
 
+(********************)
+(* Get Instructions *)
+(********************)
+
+
+      let dump_getinstrs test =
+        if has_instruction_ptr then begin
+          let fname = "instruction" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
+          O.o ""
+        end ;
+        UD.dump_getinstrs test
+
+
 (**********)
 (* Delays *)
 (**********)
@@ -311,10 +352,10 @@ module Make
           O.o "#define HAVE_TIMEBASE 1" ;
           O.o "typedef uint64_t tb_t ;" ;
           O.o "#define PTB PRIu64" ;
-          Insert.insert O.o
-            (if Cfg.is_kvm && Insert.exists "kvm_timebase.c" then
-              "kvm_timebase.c"
-            else "timebase.c")
+          let fname = if Cfg.is_kvm && Insert.exists "kvm_timebase.h" then "kvm_timebase" else "timebase" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
+          O.o ""
         end
 
 (* Memory barrier *)
@@ -330,20 +371,29 @@ module Make
           || do_precise
           || do_label_init in
         if dump_find_ins then begin
-          ObjUtil.insert_lib_file O.o "_find_ins.c" ;
+          let fname = "_find_ins" in
+          ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".c") ;
+          ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
           O.o ""
         end ;
         if do_self then begin
-          Insert.insert O.o "self.c" ;
+          let fname = "self" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".c") ;
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
           O.o "" ;
-          if Cfg.is_kvm then
-            Insert.insert O.o "kvm-self.c"
-          else
-            Insert.insert O.o "presi-self.c" ;
+          let fname = if Cfg.is_kvm then "kvm-self" else "presi-self" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".c") ;
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
           O.o "" ;
         end ;
         if CfgLoc.need_prelude then begin
-          ObjUtil.insert_lib_file O.o "_prelude_size.c"
+          let fname = "_prelude_size" in
+          ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".c") ;
+          ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
+          O.o "" 
         end ;
         dump_find_ins
 
@@ -388,7 +438,9 @@ module Make
                  O.o "static who_t whoami[AVAIL];"
                end ;
              O.o "" ;
-             Insert.insert O.o "instruction.h" ;
+             let fname = "instruction" in
+             ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+             O.o ("#include <" ^ fname ^ ".h>") ;
              O.o "" ;
              begin
                let open Fault.Handling in
@@ -404,7 +456,10 @@ module Make
 
              let insert_ins_ops () =
                if not find_ins_inserted then begin
-                 ObjUtil.insert_lib_file O.o "_find_ins.c" ;
+                 let fname =  "_find_ins" in
+                 ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".c") ;
+                 ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+                 O.o ("#include <" ^ fname ^ ".h>") ;
                  O.o ""
                end in
 
@@ -473,7 +528,9 @@ module Make
              O.fi "return 0;" ;
              O.o "}" ;
              O.o "" ;
-             Insert.insert O.o "kvm_fault_handler.c" ;
+             let fname = "kvm_fault_handler" in
+             ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+             O.o ("#include <" ^ fname ^ ".h>") ;
              O.o "" ;
              if not (T.has_asmhandler test) then begin
                O.o "static void pp_faults(void) {" ;
@@ -495,8 +552,10 @@ module Make
              begin match ok with
              | [] -> ()
              | _::_ ->
-                Insert.insert O.o "instruction.h";
-                O.o ""
+                let fname = "instruction" in
+                ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+                O.o ("#include <" ^ fname ^ ".h>") ;
+                O.o "" 
              end ;
           end ;
           let procs_user = ProcsUser.get test.T.info in
@@ -513,7 +572,10 @@ module Make
                     (ProcsUser.is procs_user p)
                     (sprintf "%d" p) (sprintf "asm_handler%d" p))
              no ;
-          Insert.insert O.o "asmhandler.c" ;
+          let fname = "asmhandler" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".c") ;
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
           O.o "" ;
           let no_ok,no_no =
             List.partition
@@ -555,15 +617,20 @@ module Make
       let dump_user_stacks procs_user = match procs_user with
         | [] -> ()
         | _::_ ->
-            Insert.insert O.o "kvm_user_stacks.c" ;
+            let fname = "kvm_user_stacks" in
+            ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+            O.o ("#include <" ^ fname ^ ".h>") ;
             O.o ""
 
 (* Synchronisation barrier *)
       let lab_ext = if Cfg.numeric_labels then "" else "_lab"
 
       let dump_barrier_def () =
-        let fname =  sprintf "barrier%s.c" lab_ext in
-        Insert.insert O.o fname
+        let fname =  sprintf "barrier%s" lab_ext in
+        ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".c") ;
+        ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+        O.o "#include <barrier.h>" ;
+        O.o ""
 
 (**************)
 (* Topologies *)
@@ -691,8 +758,8 @@ module Make
       let data_zero =  SkelUtil.data_symb_id pp_data_zero
 
       let dump_data_indices test =
-        O.f "#define %-25s 0" data_unknown ;
-        O.f "#define %-25s 1" data_zero ;
+        O.f "#define %-25s  0" data_unknown ;
+        O.f "#define %-25s  1" data_zero ;
         (* Define indices for data *)
         List.iteri
           (fun k (a,_) ->
@@ -741,7 +808,15 @@ module Make
         if see_faults test || U.ptr_in_outs env test then
           dump_data_indices test ;
         if see_faults test then
-          Insert.insert O.o  "kvm_fault_type.c"
+          let fname = "kvm_fault_define" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
+          O.o "static bool fault_reported[NTHREADS][MAX_FAULTS_PER_THREAD];" ;
+          let fname = "kvm_fault_type" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".c") ;
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname ^ ".h>") ;
+          O.o ""
 
 (* Collected locations *)
 
@@ -798,7 +873,11 @@ module Make
         O.o "" ;
         UD.dump_vars_types false test ;
         UD.dump_array_typedefs test ;
-        O.o "typedef struct {" ;
+        let fname = "log" in
+        ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+        O.o ("#include <" ^ fname ^ ".h>") ;
+        O.o "" ;
+        O.o "struct log_t {" ;
         let fields =
           A.RLocSet.fold
             (fun loc k -> (U.find_rloc_type loc env,loc)::k)
@@ -833,7 +912,7 @@ module Make
            O.fi "th_faults_info_t th_faults[NTHREADS];"
         end ;
         if pad  then O.oi "uint32_t _pad;" ;
-        O.o "} log_t;" ;
+        O.o "};" ;
         O.o "" ;
 (* There are some pointers in log *)
         let some_ptr_pte =  U.ptr_pte_in_outs env test in
@@ -1017,7 +1096,7 @@ module Make
                 EPF.fi ~out:"chan" (sprintf "%s%s=%s;" prf p1 p2) arg)
           fmt args ;
         if List.length faults > 0 then
-          O.fi "pp_log_faults_init();";
+          O.fi "pp_log_faults_init(NTHREADS, fault_reported);";
         List.iter (fun f ->
             let ((p, lbl), loc, ft) = f in
             let lbl = match lbl with
@@ -1030,9 +1109,10 @@ module Make
               | None -> "Unknown"
               | Some ft -> A.FaultType.pp ft
             in
-            O.fi "pp_log_faults(chan, &p->th_faults[%d], %d, %s, %s, %s);" p p
-              (SkelUtil.instr_symb_id lbl) (SkelUtil.data_symb_id loc) (SkelUtil.fault_id ft)
-          ) faults;
+            O.fi "pp_log_faults(chan, &p->th_faults[%d], %d, %s, %s, %s, %s, %s, %s);" p p
+              (SkelUtil.instr_symb_id lbl) (SkelUtil.data_symb_id loc) (SkelUtil.fault_id ft) 
+              "fault_reported" "instr_symb_name" "data_symb_name"
+          ) faults ;
         O.o "}" ;
         O.o "" ;
         let locs = A.RLocSet.elements rlocs in (* Now use lists *)
@@ -1055,7 +1135,7 @@ module Make
         | _ -> do_eq rloc suf in
         let do_eq_faults = function
           | [] -> O.oii "1;"
-          | _ -> O.oii "eq_faults(p->th_faults, q->th_faults);"
+          | _ -> O.oii "eq_faults(p->th_faults, q->th_faults, NTHREADS);"
         in
         let rec do_rec = function
           | [] -> do_eq_faults faults
@@ -1230,7 +1310,9 @@ module Make
         let v_tags = get_tag_vars test
         and d_tags = get_tag_delays test
         and c_tags = get_tag_caches test in
-        let all_tags = "part"::v_tags@d_tags@c_tags in
+        let all_tags_except_part = v_tags@d_tags@c_tags in
+        let all_tags = "part"::all_tags_except_part in
+        let all_tags_macro = List.map (fun tag -> "TAG_" ^ String.uppercase tag) all_tags_except_part in
 
         O.o "/**************/" ;
         O.o "/* Parameters */" ;
@@ -1239,19 +1321,32 @@ module Make
 (* Define *)
         O.o "typedef enum { cignore, cflush, ctouch, cmax, } dir_t;" ;
         O.o "" ;
-        O.o "typedef struct {" ;
+        let fname = "param" in
+        ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+        O.o ("#include <" ^ fname ^ ".h>") ;
+        O.o "" ;
+        O.f "#define TAG_LENGTH %d" (List.length all_tags_except_part) ;
+        List.iteri (fun i t ->
+          O.f "#define %s %d" t i) all_tags_macro ;
+        O.o "" ;
+        (*O.o "typedef struct {" ;
         O.oi "int part;" ;
-        let pp_tags t = function
+        O.oi "int *tags;" ;
+        (*let pp_tags t = function
           | [] -> ()
           | tags -> O.fi "%s %s;" t (String.concat "," tags) in
         pp_tags "int" v_tags ;
         pp_tags "int" d_tags ;
-        pp_tags "int" c_tags ;
+        pp_tags "int" c_tags ;*)
         O.o "} param_t;" ;
-        O.o "" ;
-        O.f "static param_t param = {%s};"
+        O.o "" ;*)
+        O.f "static int param_tags[] = {%s};" 
+          (String.concat " " 
+             (List.map (fun _ -> "-1,") all_tags_except_part)) ;
+        O.o "static param_t param = {-1, param_tags};" ;
+        (*O.f "static param_t param = {-1, param_tags};"
           (String.concat " "
-             (List.map (fun _ -> "-1,") all_tags)) ;
+             (List.map (fun _ -> "-1,") all_tags_except_part)) ;*)
         O.o "" ;
         O.o "static int id(int x) { return x; }" ;
         if have_timebase && T.get_nprocs test > 1 then
@@ -1262,16 +1357,16 @@ module Make
         let pp_tags f =
           List.iter (fun tag -> O.fi "%s," (f tag)) in
         pp_tags
-          (fun tag -> sprintf "{\"%s\",&param.%s,id,NVARS}" tag tag)
-          v_tags ;
+          (fun tag -> sprintf "{\"%s\",&param_tags[%s],id,NVARS}" tag tag)
+          (List.map (fun tag -> "TAG_" ^ String.uppercase tag) v_tags) ;
         pp_tags
-          (fun tag -> sprintf "{\"%s\",&param.%s,addnsteps,NSTEPS}" tag tag)
-          d_tags ;
+          (fun tag -> sprintf "{\"%s\",&param_tags[%s],addnsteps,NSTEPS}" tag tag)
+          (List.map (fun tag -> "TAG_" ^ String.uppercase tag) d_tags) ;
         pp_tags
-          (fun tag -> sprintf "{\"%s\",&param.%s,id,cmax}" tag tag)
-          c_tags ;
+          (fun tag -> sprintf "{\"%s\",&param_tags[%s],id,cmax}" tag tag)
+          (List.map (fun tag -> "TAG_" ^ String.uppercase tag) c_tags) ;
         O.o "};" ;
-        O.o "";
+        O.o "" ;
         O.o "#define PARSESZ (sizeof(parse)/sizeof(parse[0]))" ;
         O.o "";
 (* Print *)
@@ -1288,9 +1383,18 @@ module Make
             List.map
               (fun tag ->
                 sprintf
-                  (if is_delay tag then "p->%s-NSTEPS2" else "p->%s")
+                  (if is_delay tag then
+                     (if tag = "part" then 
+                       "p->%s-NSTEPS2"
+                     else 
+                       "p->tags[%s]-NSTEPS2")
+                   else 
+                     (if tag = "part" then
+                       "p->%s"
+                     else
+                       "p->tags[%s]"))
                   tag)
-              all_tags  in
+              ("part"::all_tags_macro)  in
           EPF.fi fmt params ;
           O.o "}" ;
           O.o "" ;
@@ -1340,12 +1444,25 @@ module Make
         let hashsz = 1+List.fold_left (fun k _ -> 2*k) hashsz faults in
         O.f "#define HASHSZ %i" hashsz ;
         O.o "" ;
-        ObjUtil.insert_lib_file O.o "_hash.c" ;
+        let fname = "_hash" in
+        ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".c") ;
+        ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+        O.o ("#include <" ^ fname ^ ".h>") ;
+        O.o "" ;
+        O.o "static entry_t main_hash[HASHSZ];" ;
+        O.o "static log_t main_hash_log[HASHSZ];" ;
+        O.o "static entry_t instance_hash[NEXE][HASHSZ];" ;
+        O.o "static log_t instance_hash_log[NEXE][HASHSZ];" ;
+        if do_stats then begin
+          O.o "static int hash_main_tags[HASHSZ][TAG_LENGTH];" ;
+          O.o "static int hash_instance_tags[NEXE][HASHSZ][TAG_LENGTH];" ;
+        end ;
+        O.o "static int instance_tags[NEXE][TAG_LENGTH];" ;
         O.o "" ;
         O.o "static void pp_entry(FILE *out,entry_t *p, int verbose, const char **group) {" ;
         let fmt = "%-6PCTR%c>" in
         EPF.fi fmt ["p->c";"p->ok ? '*' : ':'";] ;
-        O.oi "pp_log(out,&p->key);" ;
+        O.oi "pp_log(out,p->key);" ;
         if do_stats then begin
           O.oi "if (verbose) {" ;
           EPF.fii " # " [] ;
@@ -1551,7 +1668,9 @@ module Make
           ()
         end ;
         O.o "" ;
-        ObjUtil.insert_lib_file O.o "_instance.c" ;
+        let fname = "_instance" in
+        ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+        O.o ("#include <" ^ fname ^ ".h>") ;
         O.o "" ;
         ()
 
@@ -1728,10 +1847,10 @@ module Make
         O.oii "barrier_wait(_b);" ;
         List.iter
           (fun addr ->
-             O.fii "if (_p->%s == ctouch) cache_touch((void *)%s);"
-               (pctag (proc,addr)) addr ;
-             O.fii "else if (_p->%s == cflush) cache_flush((void *)%s);"
-               (pctag (proc,addr)) addr)
+             O.fii "if (_p->tags[%s] == ctouch) cache_touch((void *)%s);"
+               ("TAG_" ^ String.uppercase (pctag (proc,addr))) addr ;
+             O.fii "else if (_p->tags[%s] == cflush) cache_flush((void *)%s);"
+               ("TAG_" ^ String.uppercase (pctag (proc,addr))) addr)
           addrs ;
         begin match tag_init with
         | [] -> ()
@@ -1981,8 +2100,8 @@ module Make
               Indent.indent3 in
           O.ox id "int _cond = final_ok(final_cond(_log));" ;
           (* recorded outcome *)
-          O.fx id "int _added = hash_add(&_ctx->t,_log%s,1,_cond);"
-            (if do_stats then ",_p" else "") ;
+          O.fx id "int _added = hash_add(&_ctx->t,_log%s,1,_cond, eq_log, sizeof(log_t));" ",_p" ;
+            (*(if do_stats then ",_p" else "") ;*)
           O.ox id "if (!_added && _g->hash_ok) _g->hash_ok = 0; // Avoid writing too much." ;
           (* Result and stats *)
           O.ox id "if (_cond) {" ;
@@ -2014,10 +2133,10 @@ module Make
         O.o "/*************/" ;
         O.o "" ;
         if do_ascall then begin
-            List.iter
-              (dump_thread_code procs_user env)
-              test.T.code
-          end
+          List.iter
+            (dump_thread_code procs_user env)
+            test.T.code
+        end
 
       let dump_run_def  env test some_ptr stats procs_user =
         let faults = U.get_faults test in
@@ -2141,11 +2260,11 @@ module Make
                   try
                     let pos = get_param_pos a in
                     (* Must come first [raises Not_found] *)
-                    let tag = pvtag a in
+                    let tag = "TAG_" ^ String.uppercase (pvtag a) in
                     O.fiii
-                      "ctx->p.%s = comp_param(&c->seed,&q->%s,NVARS,0);"
+                      "ctx->p.tags[%s] = comp_param(&c->seed,&q->tags[%s],NVARS,0);"
                       tag tag ;
-                    O.fiii "_vars->%s = _mem + LINESZ*ctx->p.%s + %i*VOFFSZ;"
+                    O.fiii "_vars->%s = _mem + LINESZ*ctx->p.tags[%s] + %i*VOFFSZ;"
                       a tag pos
                   with Not_found ->
                     O.fiii "_vars->%s = _mem;" a)
@@ -2157,8 +2276,9 @@ module Make
 (* Standard parameters *)
             List.iter
               (fun (tag,max) ->
+                let macro_tag = "TAG_" ^ String.uppercase tag in 
                 O.fiii
-                  "ctx->p.%s = comp_param(&c->seed,&q->%s,%s,0);" tag tag max ;)
+                  "ctx->p.tags[%s] = comp_param(&c->seed,&q->tags[%s],%s,0);" macro_tag macro_tag max ;)
               ps ;
 (* Cache parameters*)
             List.iter
@@ -2168,25 +2288,25 @@ module Make
                     try
                       let prx = get_param_prefix v in
                       let tsts =
-                        sprintf " && ctx->p.%s != 0" (pvtag v)::
+                        sprintf " && ctx->p.tags[%s] != 0" ("TAG_" ^ String.uppercase (pvtag v))::
                         List.map
                           (fun w ->
-                            sprintf " && ctx->p.%s != ctx->p.%s"
-                              (pvtag v) (pvtag w))
+                            sprintf " && ctx->p.tags[%s] != ctx->p.tags[%s]"
+                              ("TAG_" ^ String.uppercase (pvtag v)) ("TAG_" ^ String.uppercase (pvtag w)))
                           prx in
                       String.concat "" tsts
                     with Not_found -> "" in
                   O.fiii "if (c->act->%s%s) {"
                     (Topology.active_tag p) more_test ;
-                  let tag = pctag p in
-                  O.fiv "ctx->p.%s = comp_param(&c->seed,&q->%s,cmax,1);"
+                  let tag = "TAG_" ^ String.uppercase (pctag p) in
+                  O.fiv "ctx->p.tags[%s] = comp_param(&c->seed,&q->tags[%s],cmax,1);"
                     tag tag ;
                   O.oiii "} else {" ;
-                  O.fiv "ctx->p.%s = cignore;" tag ;
+                  O.fiv "ctx->p.tags[%s] = cignore;" tag ;
                   O.oiii "}"
                 end else begin
-                  let tag = pctag p in
-                  O.fiii "ctx->p.%s = comp_param(&c->seed,&q->%s,cmax,1);"
+                  let tag = "TAG_" ^ String.uppercase (pctag p) in
+                  O.fiii "ctx->p.tags[%s] = comp_param(&c->seed,&q->tags[%s],cmax,1);"
                     tag tag
                 end)
               cs ;
@@ -2392,7 +2512,7 @@ module Make
         and procs_user = ProcsUser.get test.T.info in
         ObjUtil.insert_lib_file O.o "header.txt" ;
         dump_header test ;
-        UD.dump_getinstrs test ;
+        dump_getinstrs test ;
         dump_delay_def () ;
         dump_read_timebase () ;
         let find_ins_inserted = dump_mbar_def () in
diff --git a/litmus/skel.ml b/litmus/skel.ml
index e9f2bb6ac7..1924e3169d 100644
--- a/litmus/skel.ml
+++ b/litmus/skel.ml
@@ -84,7 +84,9 @@ module Make
      type instruction = A.instruction and
      type P.code = P.code and module A = A and module FaultType = A.FaultType)
     (O:Indent.S)
-    (Lang:Language.S with type t = A.Out.t) : sig
+    (Lang:Language.S with type t = A.Out.t)
+    (OO:ObjUtil.Config)
+    (Tar:Tar.S) : sig
       val dump : Name.t -> T.t -> unit
     end = struct
   module MakeLoc
@@ -99,6 +101,9 @@ module Make
       open Constant
       open CType
 
+(* ObjUtil (required for copying and pasting files to the relevant directory) *)
+      module Obj = ObjUtil.Make(OO)(Tar)
+
 (* Shared configuration *)
       module Param = SkelUtil.Param(Cfg)
 
@@ -300,7 +305,18 @@ module Make
 
       module Insert = ObjUtil.Insert(Cfg)
 
-      let have_timebase = Insert.exists "timebase.c"
+      let arch_dir = 
+        match UCfg.sysarch with
+        | `AArch64 -> "_aarch64/"
+        | `ARM     -> "_arm/"
+        | `MIPS    -> "_mips/"
+        | `PPC     -> "_ppc/"
+        | `X86     -> "_x86/"
+        | `RISCV   -> "_riscv/"
+        | `X86_64  -> "_x86_64/"
+        | _        -> ""
+
+      let have_timebase = Insert.exists "timebase.h"
 
       (* Location utilities *)
       let get_global_names t = List.map fst t.T.globals
@@ -553,12 +569,21 @@ module Make
         O.o "}" ;
         O.o ""
 
+      let dump_getinstrs test = 
+        if Insert.exists "instruction.h" then begin
+          let fname = "instruction" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname  ^ ".h>") ;
+          O.o "" ;
+        end ;
+        UD.dump_getinstrs test
+
       let dump_read_timebase () =
         if (do_verbose_barrier || do_timebase) && have_timebase then begin
           O.o "/* Read timebase */" ;
           O.o "typedef uint64_t tb_t ;" ;
           O.o "#define PTB PRIu64" ;
-          Insert.insert O.o "timebase.c"
+          Insert.insert O.o "timebase.h"
         end
 
       let lab_ext = if do_numeric_labels then "" else "_lab"
@@ -672,8 +697,11 @@ module Make
           O.o ""
         end ;
         if do_self then begin
-          Insert.insert O.o "self.c" ;
-          O.o ""
+          let fname = "self" in
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".c") ;
+          ignore(Obj.do_cpy ~sub:arch_dir [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname  ^ ".h>") ;
+          O.o "" ;
         end
 
 
@@ -1393,7 +1421,10 @@ module Make
             O.fx indent "_a->%s = %s(_a->%s,sizeof(*_a->%s));" a alg a a
         in
         if do_self || CfgLoc.need_prelude || U.label_in_outs env test then begin
-          ObjUtil.insert_lib_file O.o "_find_ins.c" ;
+          let fname = "_find_ins" in
+          ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".c") ;
+          ignore(Obj.do_cpy [] fname (Obj.libdir ^ fname) ".h") ;
+          O.o ("#include <" ^ fname  ^ ".h>") ;
           O.o "" ;
           if do_self then begin
             O.o "static size_t code_size(ins_t *p,int skip) { return find_ins(getret(),p,skip)+1; }" ;
@@ -2933,7 +2964,7 @@ module Make
         dump_header test ;
         if U.label_in_outs env test then
           UD.dump_label_defs (T.all_labels test) ;
-        UD.dump_getinstrs test ;
+        dump_getinstrs test ;
         dump_read_timebase () ;
         dump_threads test ;
         dump_topology doc test ;
diff --git a/litmus/skelUtil.ml b/litmus/skelUtil.ml
index 6c23eb015e..7697db2d1f 100644
--- a/litmus/skelUtil.ml
+++ b/litmus/skelUtil.ml
@@ -778,7 +778,7 @@ end
           end
 
         let dump_label_defs lbls =
-          O.f "#define %-25s 0" (instr_symb_id "UNKNOWN") ;
+          O.f "#define %-25s  0" (instr_symb_id "UNKNOWN") ;
           (* Define indices for labels *)
           List.iteri
             (fun i (p,lbl) ->
@@ -905,7 +905,7 @@ end
               O.oi "just_dump_outcomes(out,hist);"
           | Mode.PreSi|Mode.Kvm ->
               pp_nstates "hash->nhash" ;
-              O.oi "pp_hash(out,hash,g->verbose > 1,g->group);" ;
+              O.oi "pp_hash(out,hash,g->verbose > 1,g->group, pp_entry);" ;
               ()
           end ;
 (* Print condition and witnesses *)
@@ -1086,9 +1086,10 @@ end
        (* Dump opcode of relevant instructions *)
 
         let dump_getinstrs t =
-          let module I = ObjUtil.Insert(Cfg) in
+          (* Insertion of this code is now done by the caller and not this function. *)
+          (*let module I = ObjUtil.Insert(Cfg) in
           I.insert_when_exists O.o "instruction.h" ; (* Always insert *)
-          O.o "" ;
+          O.o "" ;*)
           let module D = A.GetInstr.Make(O) in
           let lbl2instr,is = all_instrs t in
           if
diff --git a/litmus/top_litmus.ml b/litmus/top_litmus.ml
index 7b559f8ccd..f61dd56268 100644
--- a/litmus/top_litmus.ml
+++ b/litmus/top_litmus.ml
@@ -162,6 +162,17 @@ end = struct
       module R = Run_litmus.Make(O)(Tar)(T.D)
       module H = LitmusUtils.Hash(O)
 
+      module OO = struct
+        include OT
+        let arch = A'.arch
+        let sysarch = Archs.get_sysarch A'.arch OT.carch
+        let cached =
+          match threadstyle with
+          | ThreadStyle.Cached -> true
+          | _ -> false
+        end
+      module Obj = ObjUtil.Make(OO)(Tar)
+
       let get_cycle t =
         let info = t.MiscParser.info in
         List.assoc "Cycle" info
@@ -198,7 +209,7 @@ end = struct
               let dump =
                 match OT.mode with
                 | Mode.Std ->
-                    let module S = Skel.Make(O)(Pseudo)(A')(T)(Out)(Lang) in
+                    let module S = Skel.Make(O)(Pseudo)(A')(T)(Out)(Lang)(OO)(Tar) in
                     S.dump
                 | Mode.PreSi|Mode.Kvm ->
                     let module O =
@@ -212,7 +223,7 @@ end = struct
                         | Barrier.TimeBase  -> true
                         | _ -> false
                       end  in
-                    let module S = PreSi.Make(O)(Pseudo)(A')(T)(Out)(Lang) in
+                    let module S = PreSi.Make(O)(Pseudo)(A')(T)(Out)(Lang)(OO)(Tar) in
                     S.dump in
               dump doc compiled)
             outname
@@ -272,22 +283,12 @@ end = struct
                   { Flags.pac = O.variant Variant_litmus.Pac;
                     Flags.self = O.variant Variant_litmus.Self;
                     Flags.memtag = O.variant Variant_litmus.MemTag } in
+                let () = Obj.mk_libdir in
                 dump src doc compiled;
                 if not OT.is_out then begin
-                    let _utils =
-                      let module OO = struct
-                        include OT
-                        let arch = A'.arch
-                        let sysarch = Archs.get_sysarch A'.arch OT.carch
-                        let cached =
-                          match threadstyle with
-                          | ThreadStyle.Cached -> true
-                          | _ -> false
-                      end in
-                      let module Obj = ObjUtil.Make(OO)(Tar) in
-                      Obj.dump flags in
-                    ()
-                  end ;
+                  let _utils = Obj.dump flags in
+                  ()
+                end ;
                 R.run name out_chan doc allocated src ;
                 Completed
                   { arch = A'.arch; doc; src; fullhash = hash ;