Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
66 commits
Select commit Hold shift + click to select a range
95f264d
added provisional template C file
Jan 23, 2026
4f1f0e8
Merge remote-tracking branch 'upstream/master'
Jan 28, 2026
d3fbc28
squashed all commits to one
Feb 9, 2026
101dbcd
added header guards and moved include to find ins
Feb 23, 2026
ba2ce7c
added initial header info
Feb 26, 2026
39bb437
potential fix to instruction port problem
Mar 2, 2026
7359fa9
fixed aarch64 std and presi instruction.h error
Mar 3, 2026
00b105e
fixed merge conflict
Mar 3, 2026
4680272
fixed missing file
Mar 3, 2026
06c08a0
hashtable C code no longer static
Mar 5, 2026
4b60148
fixed kvm self mode compilation error
Mar 19, 2026
edd0ddf
Merge branch 'inlineport' into inlineport2
Mar 19, 2026
a860d81
Merge branch 'inlineport' into inlineport4
Mar 19, 2026
69b72b8
fixed kvm self mode compilation error
Mar 19, 2026
0e9b1b9
Merge branch 'inlineport' of github.com:z5146542/herdtools7 into inli…
Mar 19, 2026
03c04d9
Merge branch 'inlineport' into inlineport2
Mar 19, 2026
318e7d4
Merge branch 'inlineport' into inlineport4
Mar 19, 2026
63734c8
fixed kvm self mode compilation error
Mar 19, 2026
cf435e2
Merge branch 'inlineport2' of github.com:z5146542/herdtools7 into inl…
Mar 19, 2026
f19ef8d
fixed kvm self mode compilation error
Mar 19, 2026
382b4f8
Merge branch 'inlineport4' of github.com:z5146542/herdtools7 into inl…
Mar 19, 2026
a39c744
added missing header
Mar 19, 2026
2dd8205
added initial header info
Feb 26, 2026
4051ac5
fixed merge conflict
Mar 19, 2026
bbf2861
Merge branch 'inlineport2' into inlineport4
Mar 19, 2026
584ae91
fixed all kvm aarch64 compilation errors
Mar 20, 2026
25442e6
Merge branch 'inlineport' into inlineport2
Mar 20, 2026
c974d21
Merge branch 'inlineport2' into inlineport4
Mar 20, 2026
00d6d1d
fixed timebase not copying and make clean deleting o files
Mar 23, 2026
7d5048b
Merge branch 'inlineport' into inlineport2
Mar 23, 2026
236bf3f
Merge branch 'inlineport2' into inlineport4
Mar 23, 2026
80212cc
made header guards more consistent, removed old comments, and improve…
Mar 23, 2026
92ba376
fixed merge conflict
Mar 23, 2026
413639b
fixed merge conflict
Mar 23, 2026
97baf3e
added additional ignores
Mar 23, 2026
ff3f849
added provisional template C file
Jan 23, 2026
0ff0cde
squashed all commits to one
Feb 9, 2026
bae8890
added header guards and moved include to find ins
Feb 23, 2026
ea92038
added initial header info
Feb 26, 2026
9f579bb
fixed all kvm aarch64 compilation errors
Mar 20, 2026
a7d176c
fixed timebase not copying and make clean deleting o files
Mar 23, 2026
6316e89
made header guards more consistent, removed old comments, and improve…
Mar 23, 2026
2512069
rebased with origin master and fixed merge conflict
Mar 24, 2026
0898f16
rebased and fixed type merge conflict
Mar 24, 2026
f8cec08
Merge branch 'inlineport2' into inlineport4
Mar 24, 2026
de19e61
added provisional template C file
Jan 23, 2026
6b8e4db
squashed all commits to one
Feb 9, 2026
b5a7e77
added header guards and moved include to find ins
Feb 23, 2026
fce8c5d
added initial header info
Feb 26, 2026
e50e65a
fixed all kvm aarch64 compilation errors
Mar 20, 2026
d4ea914
fixed timebase not copying and make clean deleting o files
Mar 23, 2026
233fc54
made header guards more consistent, removed old comments, and improve…
Mar 23, 2026
d68bd31
added provisional template C file
Jan 23, 2026
785db8c
squashed all commits to one
Feb 9, 2026
6286f53
added header guards and moved include to find ins
Feb 23, 2026
8350229
added initial header info
Feb 26, 2026
2cc4318
fixed all kvm aarch64 compilation errors
Mar 20, 2026
df3a309
made header guards more consistent, removed old comments, and improve…
Mar 23, 2026
aba77f0
fixed missing header guard
Mar 24, 2026
b13f590
fixed copyright headers
Mar 24, 2026
42ba5b8
fixed merge conflict
Mar 24, 2026
ef9613a
fixed merge conflict
Mar 24, 2026
0fe4e0d
fixed std self mode error
Mar 24, 2026
f40f79c
fixed gcc warning on exit stdlib
Mar 24, 2026
a88f11d
Merge branch 'inlineport' into inlineport2
Mar 24, 2026
191c327
Merge branch 'inlineport2' into inlineport4
Mar 24, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion dirs-and-confs.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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
catalogue/aarch64-ifetch/tests catalogue/aarch64-ifetch/cfgs/new-web.cfg
37 changes: 27 additions & 10 deletions litmus/dumpRun.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 -> ()
Expand All @@ -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 =
Expand All @@ -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"
Expand All @@ -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 ;
()
;;

Expand Down Expand Up @@ -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" ;
Expand Down Expand Up @@ -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 *)
Expand Down
2 changes: 1 addition & 1 deletion litmus/libdir/_aarch64/_auth.h
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand Down
5 changes: 0 additions & 5 deletions litmus/libdir/_aarch64/_memtag.c
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down Expand Up @@ -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 */
5 changes: 4 additions & 1 deletion litmus/libdir/_aarch64/_memtag.h
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Expand All @@ -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,
Expand All @@ -22,3 +24,4 @@ typedef enum
} tag_check_key;

void mte_init(tag_check_key tag_check);
#endif
19 changes: 18 additions & 1 deletion litmus/libdir/_aarch64/asmhandler.c
Original file line number Diff line number Diff line change
@@ -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"
Expand Down
19 changes: 19 additions & 0 deletions litmus/libdir/_aarch64/asmhandler.h
Original file line number Diff line number Diff line change
@@ -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
13 changes: 4 additions & 9 deletions litmus/libdir/_aarch64/barrier.c
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down Expand Up @@ -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 (
Expand Down Expand Up @@ -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) ;
Expand Down
30 changes: 30 additions & 0 deletions litmus/libdir/_aarch64/barrier.h
Original file line number Diff line number Diff line change
@@ -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
21 changes: 21 additions & 0 deletions litmus/libdir/_aarch64/instruction.h
Original file line number Diff line number Diff line change
@@ -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
16 changes: 16 additions & 0 deletions litmus/libdir/_aarch64/intrinsics.h
Original file line number Diff line number Diff line change
@@ -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) \
Expand Down
3 changes: 3 additions & 0 deletions litmus/libdir/_aarch64/kvm-headers.h
Original file line number Diff line number Diff line change
Expand Up @@ -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>
Expand Down Expand Up @@ -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
28 changes: 24 additions & 4 deletions litmus/libdir/_aarch64/kvm-self.c
Original file line number Diff line number Diff line change
Expand Up @@ -16,20 +16,40 @@
/* 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);
vaddr += cache_line_size;
}
}

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);
Expand All @@ -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);
Expand Down
31 changes: 31 additions & 0 deletions litmus/libdir/_aarch64/kvm-self.h
Original file line number Diff line number Diff line change
@@ -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
Loading