diff --git a/CHANGES.md b/CHANGES.md
index bc420dcca..8da554bcd 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -28,6 +28,9 @@ description indicates whether it is SOURCE-COMPATIBLE, BINARY-COMPATIBLE, or BRE
### Changes
+* Add `seL4_DebugGetThreadAffinity()` syscall to return the current affinity of a thread
+ in SMP configurations.
+
### Platforms
* Add support for the stm32mp2 SoC family
diff --git a/libsel4/arch_include/arm/sel4/arch/syscalls.h b/libsel4/arch_include/arm/sel4/arch/syscalls.h
index 63eaae369..3331b286b 100644
--- a/libsel4/arch_include/arm/sel4/arch/syscalls.h
+++ b/libsel4/arch_include/arm/sel4/arch/syscalls.h
@@ -645,6 +645,21 @@ LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
}
#if CONFIG_ENABLE_SMP_SUPPORT
+LIBSEL4_INLINE_FUNC seL4_Word seL4_DebugGetThreadAffinity(seL4_CPtr tcb)
+{
+ seL4_Word unused0 = 0;
+ seL4_Word unused1 = 0;
+ seL4_Word unused2 = 0;
+ seL4_Word unused3 = 0;
+ seL4_Word unused4 = 0;
+
+ seL4_Word affinity = 0;
+
+ arm_sys_send_recv(seL4_SysDebugGetThreadAffinity, tcb, &affinity, 0,
+ &unused0, &unused1, &unused2, &unused3, &unused4, 0);
+ return affinity;
+}
+
LIBSEL4_INLINE_FUNC void seL4_DebugSendIPI(seL4_Uint8 target, unsigned irq)
{
arm_sys_send(seL4_SysDebugSendIPI, target, irq, 0, 0, 0, 0);
diff --git a/libsel4/arch_include/riscv/sel4/arch/syscalls.h b/libsel4/arch_include/riscv/sel4/arch/syscalls.h
index 06042003f..351fa79ba 100644
--- a/libsel4/arch_include/riscv/sel4/arch/syscalls.h
+++ b/libsel4/arch_include/riscv/sel4/arch/syscalls.h
@@ -849,7 +849,24 @@ LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
riscv_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3,
&unused4, &unused5, 0);
}
-#endif
+
+#if CONFIG_ENABLE_SMP_SUPPORT
+LIBSEL4_INLINE_FUNC seL4_Word seL4_DebugGetThreadAffinity(seL4_CPtr tcb)
+{
+ seL4_Word unused0 = 0;
+ seL4_Word unused1 = 0;
+ seL4_Word unused2 = 0;
+ seL4_Word unused3 = 0;
+ seL4_Word unused4 = 0;
+
+ seL4_Word affinity = 0;
+
+ riscv_sys_send_recv(seL4_SysDebugGetThreadAffinity, tcb, &affinity, 0,
+ &unused0, &unused1, &unused2, &unused3, &unused4, 0);
+ return affinity;
+}
+#endif /* CONFIG_ENABLE_SMP_SUPPORT */
+#endif /* CONFIG_DEBUG_BUILD */
#ifdef CONFIG_DANGEROUS_CODE_INJECTION
LIBSEL4_INLINE_FUNC void seL4_DebugRun(void (* userfn)(void *), void *userarg)
diff --git a/libsel4/include/api/syscall.xml b/libsel4/include/api/syscall.xml
index 5b62ac24e..8174659d3 100644
--- a/libsel4/include/api/syscall.xml
+++ b/libsel4/include/api/syscall.xml
@@ -57,6 +57,7 @@
+
diff --git a/libsel4/include/sel4/syscalls.h b/libsel4/include/sel4/syscalls.h
index 1613c4f77..eea7da585 100644
--- a/libsel4/include/sel4/syscalls.h
+++ b/libsel4/include/sel4/syscalls.h
@@ -118,7 +118,22 @@ seL4_DebugCapIdentify(seL4_CPtr cap);
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugNameThread(seL4_CPtr tcb, const char *name);
-#if defined(CONFIG_ENABLE_SMP_SUPPORT) && defined(CONFIG_ARCH_ARM)
+#if defined(CONFIG_ENABLE_SMP_SUPPORT)
+/**
+ * @xmlonly @endxmlonly
+ * @brief Get the current affinity of a thread.
+ *
+ * This gets the value of the kernel's tcb_t->tcbAffinity field, which corresponds
+ * to the core (affinity) of the thread. If the thread is not running (e.g. blocked)
+ * this is the last core it ran on.
+ *
+ * @param tcb A capability to the tcb object for the thread to query.
+ *
+ */
+LIBSEL4_INLINE_FUNC seL4_Word
+seL4_DebugGetThreadAffinity(seL4_CPtr tcb);
+
+#if defined(CONFIG_ARCH_ARM)
/**
* @xmlonly @endxmlonly
* @brief Sends arbitrary SGI.
@@ -131,8 +146,9 @@ seL4_DebugNameThread(seL4_CPtr tcb, const char *name);
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugSendIPI(seL4_Uint8 target, unsigned irq);
-#endif
-#endif
+#endif /* CONFIG_ARCH_ARM */
+#endif /* CONFIG_ENABLE_SMP_SUPPORT */
+#endif /* CONFIG_DEBUG_BUILD */
#ifdef CONFIG_DANGEROUS_CODE_INJECTION
/**
diff --git a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
index 3d3a8f2db..7ead82092 100644
--- a/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/ia32/sel4/sel4_arch/syscalls.h
@@ -874,6 +874,23 @@ LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
x86_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, MCS_COND(0, &unused3));
}
+
+#if CONFIG_ENABLE_SMP_SUPPORT
+LIBSEL4_INLINE_FUNC seL4_Word seL4_DebugGetThreadAffinity(seL4_CPtr tcb)
+{
+ seL4_Word unused0 = 0;
+ seL4_Word unused1 = 0;
+ seL4_Word unused2 = 0;
+ seL4_Word unused3 = 0;
+ seL4_Word unused4 = 0;
+
+ seL4_Word affinity = 0;
+
+ x86_sys_send_recv(seL4_SysDebugGetThreadAffinity, tcb, &affinity, 0,
+ &unused0, &unused1, MCS_COND(0, &unused2));
+ return affinity;
+}
+#endif /* CONFIG_ENABLE_SMP_SUPPORT */
#endif
#if defined(CONFIG_DANGEROUS_CODE_INJECTION)
diff --git a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
index 2752cfc30..fda4aa161 100644
--- a/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
+++ b/libsel4/sel4_arch_include/x86_64/sel4/sel4_arch/syscalls.h
@@ -673,7 +673,24 @@ LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
x64_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
-#endif
+
+#if CONFIG_ENABLE_SMP_SUPPORT
+LIBSEL4_INLINE_FUNC seL4_Word seL4_DebugGetThreadAffinity(seL4_CPtr tcb)
+{
+ seL4_Word unused0 = 0;
+ seL4_Word unused1 = 0;
+ seL4_Word unused2 = 0;
+ seL4_Word unused3 = 0;
+ seL4_Word unused4 = 0;
+
+ seL4_Word affinity = 0;
+
+ x64_sys_send_recv(seL4_SysDebugGetThreadAffinity, tcb, &affinity, 0,
+ &unused0, &unused1, &unused3, &unused4, &unused5, 0);
+ return affinity;
+}
+#endif /* CONFIG_ENABLE_SMP_SUPPORT */
+#endif /* CONFIG_DEBUG_BUILD */
#if defined(CONFIG_DANGEROUS_CODE_INJECTION)
LIBSEL4_INLINE_FUNC void seL4_DebugRun(void (*userfn)(void *), void *userarg)
diff --git a/src/api/syscall.c b/src/api/syscall.c
index 1e734189c..5166f3b28 100644
--- a/src/api/syscall.c
+++ b/src/api/syscall.c
@@ -158,6 +158,19 @@ exception_t handleUnknownSyscall(word_t w)
return EXCEPTION_NONE;
}
#ifdef ENABLE_SMP_SUPPORT
+ if (w == SysDebugGetThreadAffinity) {
+ word_t cptr = getRegister(NODE_STATE(ksCurThread), capRegister);
+ lookupCapAndSlot_ret_t lu_ret = lookupCapAndSlot(NODE_STATE(ksCurThread), cptr);
+ /* ensure we got a TCB cap */
+ word_t cap_type = cap_get_capType(lu_ret.cap);
+ if (cap_type != cap_thread_cap) {
+ userError("SysDebugGetThreadAffinity: cap is not a TCB, halting");
+ halt();
+ }
+ word_t affinity = TCB_PTR(cap_thread_cap_get_capTCBPtr(lu_ret.cap))->tcbAffinity;
+ setRegister(NODE_STATE(ksCurThread), capRegister, affinity);
+ return EXCEPTION_NONE;
+ }
if (w == SysDebugSendIPI) {
return handle_SysDebugSendIPI();
}