smartobjectoriented · jmi-reds · Feb 13, 2026 · Jan 30, 2026 · Feb 5, 2026 · Feb 7, 2026
diff --git a/doc/source/conf.py b/doc/source/conf.py
@@ -123,7 +123,6 @@
 try:
     import sphinx_rtd_theme
     html_theme = 'sphinx_rtd_theme'
-    html_theme_path = [sphinx_rtd_theme.get_html_theme_path()]
     def setup(app):
 #        app.add_stylesheet('style.css')
         app.add_css_file('style.css')

diff --git a/doc/source/user_guide.rst b/doc/source/user_guide.rst
@@ -38,7 +38,7 @@ prevent annoying warnings:
 
    sudo apt-get install bison flex
 
-Files and directroy organisation
+Files and directory organization
 ********************************
 
 SO3 root directory (main subdirs)::
@@ -67,7 +67,7 @@ SO3 root directory (main subdirs)::
 Build of the environment
 ************************
 
-kernel toolchain
+Kernel toolchain
 ================
 
 We use the ``arm-none-eabi`` toolchain which has no dependencies on a libc.
@@ -78,22 +78,22 @@ The following package can be installed:
 
    apt install gcc-arm-none-eabi
 
-usr-space toolchain
-===================
+User space toolchain
+====================
 
-The usr-space uses MUSL as libc. The Musl toolchains can be generated with
+The user space uses MUSL as libc. The Musl toolchains can be generated with
 ``toolchains/build-toolchain.sh`` script.
 
 .. code-block:: bash
 
-   $ ./build-toolchain.sh
+   $ sudo ./build-toolchain.sh
 
 By default, it generates ``aarch64-linux-musl`` and ``arm-linux-musleabihf``
 folder in the ``toolchains`` directory
 
 .. note::
 
-   The output directory (by default ``toolchains`` floder) can be changed by setting
+   The output directory (by default ``toolchains`` folder) can be changed by setting
    the ``OUTPUT_PATH`` variable in the ``build-toolchain.sh`` script
 
 Quick setup & early test
@@ -309,4 +309,4 @@ The, starting the execution of the container:
 
 
 
-
+
diff --git a/so3/arch/arm64/domain.c b/so3/arch/arm64/domain.c
@@ -116,9 +116,9 @@ void __setup_dom_pgtable(struct domain *d, addr_t paddr_start, unsigned long map
 	__create_mapping(new_pt, memslot[slotID].ipa_addr, paddr_start, map_size, false, S2);
 
 	if (d->avz_shared->domID == DOMID_AGENCY)
-		do_ipamap(new_pt, linux_ipamap, ARRAY_SIZE(linux_ipamap));
+		do_ipamap(new_pt, agency_ipamap, ARRAY_SIZE(agency_ipamap));
 	else
-		do_ipamap(new_pt, guest_ipamap, ARRAY_SIZE(guest_ipamap));
+		do_ipamap(new_pt, capsule_ipamap, ARRAY_SIZE(capsule_ipamap));
 
 	/* Map the shared page in the IPA space; the shared page is located right after the domain area
 	 * in the IPA space, and if any, the RT shared page follows the shared page (in IPA space).

diff --git a/so3/arch/arm64/exception.S b/so3/arch/arm64/exception.S
@@ -209,17 +209,17 @@ ENTRY(__vectors)
 
 #ifdef CONFIG_CPU_SPIN_TABLE
 
-ENTRY(pre_ret_to_el1_with_spin)
+ENTRY(pre_ret_to_el1_spin)
 
-	mov	x1, x0
+	mov		x1, x0
 	str 	xzr, [x1]
 1:
 	wfe
  	ldr 	x0, [x1]
 
-    	cbz 	x0, 1b
+    cbz 	x0, 1b
 
-    	// Branch to the given address
+    // Branch to the given address
 	msr	elr_el2, x0
 
 	// Set the CPU in EL1 mode to proceed with
@@ -239,7 +239,7 @@ ENTRY(pre_ret_to_el1_with_spin)
 	mov	x2, #0
 	mov	x3, #0
 
-	// Ready to jump into the Linux domain...
+	// Ready to jump into the Agency domain...
 
 	eret
 
@@ -264,7 +264,7 @@ ENTRY(pre_ret_to_el1)
 
 	wfi
 
-	ldr 	x0, cpu_entrypoint
+	ldr x0, cpu_entrypoint
 	msr	elr_el2, x0
 
 	// Set the CPU in EL1 mode to proceed with

diff --git a/so3/arch/arm64/include/asm/processor.h b/so3/arch/arm64/include/asm/processor.h
@@ -1263,7 +1263,7 @@ void __switch_domain_to(struct domain *prev, struct domain *next);
 void ret_to_user(void);
 void pre_ret_to_user(void);
 void pre_ret_to_el1(void);
-void pre_ret_to_el1_with_spin(addr_t release_addr);
+void pre_ret_to_el1_spin(addr_t release_addr);
 
 #endif /* CONFIG_AVZ */
 

diff --git a/so3/arch/arm64/rpi4_64/include/mach/ipamap.h b/so3/arch/arm64/rpi4_64/include/mach/ipamap.h
@@ -21,51 +21,37 @@
 
 #include <asm/mmu.h>
 
-ipamap_t ipamap[] = {
+ipamap_t agency_ipamap[] = {
+
+	/* I/O Memory space*/
 	{
 		.ipa_addr = 0xf0000000,
 		.phys_addr = 0xf0000000,
 		.size = 0x10000000,
 	},
-	{
-		.ipa_addr = 0x1faf0000,
-		.phys_addr = 0x1faf0000,
-		.size = 0x1000,
-	},
-	{
-		.ipa_addr = 0x1faf1000,
-		.phys_addr = 0x1faf1000,
-		.size = 0x9000,
-	},
-	{
-		.ipa_addr = 0x1fafa000,
-		.phys_addr = 0x1fafa000,
-		.size = 0x2000,
-	},
-	{
-		.ipa_addr = 0x1fafc000,
-		.phys_addr = 0x1fafc000,
-		.size = 0x2000,
-	},
-	{
-		.ipa_addr = 0x1fafe000,
-		.phys_addr = 0x1fafe000,
-		.size = 0x2000,
-	},
+
+	/* Null pointer exception */
 	{
 		.ipa_addr = 0x0,
 		.phys_addr = 0x0,
 		.size = 0x1000,
 	},
+};
+
+/**
+ * In the guest environment, the access to the GIC distributor must lead to a data abort
+ * which will be trapped and handled by the hypervisor.
+ */
+
+ipamap_t capsule_ipamap[] = {
+
 	{
-		.ipa_addr = 0x50000000,
-		.phys_addr = 0x50000000,
-		.size = 0x10000000,
-	},
-	{
-		.ipa_addr = 0x600000000,
-		.phys_addr = 0x600000000,
-		.size = 0x1000,
+		/* Only mapping the CPU interface to the vGIC CPU interface.
+	 * Access to the distributor must lead to a trap and be handled by the hypervisor.
+	 */
+		.ipa_addr = 0x08010000,
+		.phys_addr = 0x08040000,
+		.size = 0x10000,
 	},
 };
 

diff --git a/so3/arch/arm64/virt64/include/mach/ipamap.h b/so3/arch/arm64/virt64/include/mach/ipamap.h
@@ -21,7 +21,7 @@
 
 #include <asm/mmu.h>
 
-ipamap_t linux_ipamap[] = {
+ipamap_t agency_ipamap[] = {
 	{
 		.ipa_addr = 0x08000000,
 		.phys_addr = 0x08000000,
@@ -34,7 +34,7 @@ ipamap_t linux_ipamap[] = {
  * which will be trapped and handled by the hypervisor.
  */
 
-ipamap_t guest_ipamap[] = {
+ipamap_t capsule_ipamap[] = {
 
 	{
 		/* Only mapping the CPU interface to the vGIC CPU interface.

diff --git a/so3/avz/kernel/smp.c b/so3/avz/kernel/smp.c
@@ -114,23 +114,25 @@ void secondary_start_kernel(void)
 #ifdef CONFIG_CPU_SPIN_TABLE
 	switch (cpu) {
 	case 1:
-		pre_ret_to_el1_with_spin(CPU1_RELEASE_ADDR);
+		pre_ret_to_el1_spin(CPU1_RELEASE_ADDR);
 		break;
 	case 2:
-		pre_ret_to_el1_with_spin(CPU2_RELEASE_ADDR);
+		pre_ret_to_el1_spin(CPU2_RELEASE_ADDR);
 		break;
 	case 3:
-		pre_ret_to_el1_with_spin(CPU3_RELEASE_ADDR);
+		pre_ret_to_el1_spin(CPU3_RELEASE_ADDR);
 		break;
 	default:
 		printk("%s: trying to start CPU %d that is not supported.\n", __func__, cpu);
 	}
 #endif
 
+#ifdef CONFIG_CPU_PSCI
 #ifdef CONFIG_SOO
 	if (cpu != ME_CPU)
-#endif
+#endif /* CONFIG_SOO */
 		pre_ret_to_el1();
+#endif /* CONFIG_CPU_PCSI */
 
 	secondary_timer_init();
 

diff --git a/so3/devices/fdt.c b/so3/devices/fdt.c
@@ -1,5 +1,5 @@
 /*
- * Copyright (C) 2014-2019 Daniel Rossier <daniel.rossier@heig-vd.ch>
+ * Copyright (C) 2014-2026 Daniel Rossier <daniel.rossier@heig-vd.ch>
  *
  *
  * This program is free software; you can redistribute it and/or modify
@@ -55,7 +55,13 @@ static void init_dev_info(dev_t *dev)
 	dev->fdt = 0;
 }
 
-/* Get memory informations from a device tree */
+/**
+ * @brief Get memory informations from a device tree 
+ * 
+ * @param fdt Virtual address of the device tree
+ * @param info Memory info structure which will be filled up by this function
+ * @return int Offset of the memory node in the device tree
+ */
 int get_mem_info(const void *fdt, mem_info_t *info)
 {
 	int offset;
@@ -81,14 +87,17 @@ int get_mem_info(const void *fdt, mem_info_t *info)
 
 	/* For some platform, address-cells and size-cells are set to 2 (64-bit)
 	 * even for a 32-bit platform, probably to support LPAE.
+	 * Additionally, on Raspberry Pi 4, the device tree has its memory node 
+	 * with a 64-bit address cell and a 32-bit size cell. That's why we need
+	 * to consider a 12 bytes <reg> property.
 	 */
 
 	if (prop) {
 		if (prop_len == 8) {
 			info->phys_base = fdt32_to_cpu(((const fdt32_t *) prop->data)[0]);
 			info->size = fdt32_to_cpu(((const fdt32_t *) prop->data)[1]);
 		} else {
-			BUG_ON(prop_len != 16);
+			BUG_ON((prop_len != 16) && (prop_len != 12));
 
 			/* Keep a possible conversion from 64-bit to 32-bit if the address & size are
 			 * on 64-bit for aarch32 platforms.
@@ -110,10 +119,15 @@ int get_mem_info(const void *fdt, mem_info_t *info)
 
 			info->phys_base = fdt64_to_cpu(val);
 
-			for (i = 0; i < 8; i++)
-				*(((char *) &val) + i) = *ptr++;
-
-			info->size = fdt64_to_cpu(val);
+			if (prop_len == 16) {
+				for (i = 0; i < 8; i++)
+					*(((char *) &val) + i) = *ptr++;
+				info->size = fdt64_to_cpu(val);
+			} else {
+				for (i = 0; i < 4; i++)
+					*(((char *) &val) + i) = *ptr++;
+				info->size = fdt32_to_cpu(val);
+			}
 
 #endif /* !CONFIG_ARCH_ARM32 */
 		}

diff --git a/so3/devices/irq/gic.c b/so3/devices/irq/gic.c
@@ -431,12 +431,9 @@ void gich_init(void)
 
 void gicc_init(void)
 {
-	unsigned int cpu = smp_processor_id();
 	u32 bypass = 0;
 	int i;
 
-	spin_lock_init(&per_cpu(intc_lock, cpu));
-
 	/*
          * Deal with the banked PPI and SGI interrupts - disable all
          * PPI interrupts, ensure all SGI interrupts are enabled.
@@ -659,6 +656,11 @@ static int gic_init(dev_t *dev, int fdt_offset)
 {
 	const struct fdt_property *prop;
 	int prop_len;
+	int cpu;
+
+	for (cpu = 0; cpu < CONFIG_NR_CPUS; cpu++) {
+		spin_lock_init(&per_cpu(intc_lock, cpu));
+	}
 
 	gic = (gic_t *) malloc(sizeof(gic_t));
 	BUG_ON(!gic);

diff --git a/so3/dts/Makefile b/so3/dts/Makefile
@@ -1,6 +1,6 @@
 
 dtb-$(CONFIG_RPI4) += rpi4.dtb
-dtb-$(CONFIG_RPI4_64) += rpi4_64.dtb rpi4_64_avz_vt.dtb
+dtb-$(CONFIG_RPI4_64) += rpi4_64.dtb rpi4_64_avz.dtb
 dtb-$(CONFIG_VIRT64) += virt64.dtb virt64_avz.dtb virt64_capsule.dtb virt64_lvperf.dtb
 dtb-$(CONFIG_VIRT32) += virt32.dtb virt32_lvperf.dtb
 

diff --git a/so3/dts/rpi4_64.dts b/so3/dts/rpi4_64.dts
@@ -32,11 +32,7 @@
 
 	memory@0 {
 		device_type = "memory";
-		reg = <0x0 0x01000000 0x0 0x20000000>; /* 512 MB */
-	};
-
-	agency {
-		domain-size = <0x10000000>;
+		reg = <0x0 0x10000000 0x0 0x20000000>; /* 512 MB */
 	};
 
 	mem {

diff --git a/so3/dts/rpi4_64_avz_vt.dts → so3/dts/rpi4_64_avz.dts b/so3/dts/rpi4_64_avz_vt.dts → so3/dts/rpi4_64_avz.dts
diff --git a/so3/fs/elf.c b/so3/fs/elf.c
@@ -219,8 +219,9 @@ void elf_load_segments(elf_img_info_t *elf_img_info)
 		elf_img_info->segment_end_vaddr = 0;
 	}
 
+#ifndef CONFIG_AVZ
 	LOG_DEBUG("segments use %d virtual pages\n", elf_img_info->segment_page_count);
-
+#endif
 	for (i = 0; i < elf_img_info->header->e_phnum; i++) {
 		LOG_DEBUG("[0x%08x] vaddr: 0x%08x; paddr: 0x%08x; filesize: 0x%08x; memsize: 0x%08x flags: 0x%08x\n",
 			  elf_img_info->segments[i].p_offset, elf_img_info->segments[i].p_vaddr,

diff --git a/so3/kernel/process.c b/so3/kernel/process.c
@@ -329,8 +329,9 @@ void create_root_process(void)
 
 	allocate_page(pcb, pcb->stack_top - (pcb->page_count * PAGE_SIZE), pcb->page_count, true);
 
+#ifndef CONFIG_AVZ
 	LOG_DEBUG("Stack mapped at 0x%08x (size: %d bytes)\n", pcb->stack_top - (pcb->page_count * PAGE_SIZE), PROC_STACK_SIZE);
-
+#endif
 	/* First map the code in the user space so that
          * the initial code can run normally in user mode.
          */
@@ -589,8 +590,9 @@ int setup_proc_image_replace(elf_img_info_t *elf_img_info, pcb_t *pcb, int argc,
 
 	allocate_page(pcb, pcb->stack_top - (pcb->page_count * PAGE_SIZE), pcb->page_count, true);
 
+#ifndef CONFIG_AVZ
 	LOG_DEBUG("stack mapped at 0x%08x (size: %d bytes)\n", pcb->stack_top - (pcb->page_count * PAGE_SIZE), PROC_STACK_SIZE);
-
+#endif
 	/* Initialize the pc register */
 	pcb->bin_image_entry = (uint32_t) elf_img_info->header->e_entry;
 

diff --git a/so3/soo/include/soo/uapi/soo.h b/so3/soo/include/soo/uapi/soo.h
@@ -175,7 +175,7 @@ extern atomic_t dc_incoming_domID[DC_EVENT_MAX];
  */
 typedef struct {
 	unsigned int slotID;
-	unsigned int capsuleID;
+	unsigned int capsuleID; /* ID handled by emiso engine */
 	uint64_t spid;
 
 	ME_state_t state;