diff --git a/so3/arch/arm64/Kconfig b/so3/arch/arm64/Kconfig
index 47ebeda15..283fd926c 100644
--- a/so3/arch/arm64/Kconfig
+++ b/so3/arch/arm64/Kconfig
@@ -3,12 +3,6 @@ if ARCH_ARM64
 
 menu "Platform"
 
-	config ARM64VT
-		depends on AVZ
-		bool "Virtualization support (ARM64 VT)"
-		help
-	  	  Enabling support of CPU virtualization extensions.
-  
 	choice
   		prompt "Target"
 	
diff --git a/so3/arch/arm64/Makefile b/so3/arch/arm64/Makefile
index ad63cc0cd..273b8a92a 100644
--- a/so3/arch/arm64/Makefile
+++ b/so3/arch/arm64/Makefile
@@ -1,5 +1,5 @@
 
-ifneq ($(CONFIG_ARM64VT),y)
+ifneq ($(CONFIG_AVZ),y)
 obj-y += hyp-stub.o
 endif
 
@@ -10,7 +10,7 @@ obj-y += backtrace.o backtrace_asm.o
 obj-y += cache_v8.o cache.o context.o
 obj-y += semihosting.o semicall.o
 
-obj-$(CONFIG_AVZ) += domain.o mmio.o
+obj-$(CONFIG_AVZ) += domain.o mmio.o #smmu.o
 
 obj-y += smccc-call.o
 
@@ -18,8 +18,6 @@ obj-y += thread.o
 
 obj-$(CONFIG_MMU) += mmu.o
 
-obj-$(CONFIG_ARM64VT) += #smmu.o
-
 obj-y += lib/
 
 obj-y += $(TARGET)/
diff --git a/so3/arch/arm64/cache_v8.c b/so3/arch/arm64/cache_v8.c
index c155d8752..41cdae414 100644
--- a/so3/arch/arm64/cache_v8.c
+++ b/so3/arch/arm64/cache_v8.c
@@ -101,7 +101,7 @@ void mmu_setup(void *pgtable)
 	invalidate_dcache_all();
 	__asm_invalidate_tlb_all();
 
-#endif /* !CONFIG_ARM64VT */
+#endif /* !CONFIG_AVZ */
 }
 
 /*
diff --git a/so3/arch/arm64/domain.c b/so3/arch/arm64/domain.c
index 0e5c0d2d9..39632777d 100644
--- a/so3/arch/arm64/domain.c
+++ b/so3/arch/arm64/domain.c
@@ -26,7 +26,7 @@
 #include <asm/mmu.h>
 #include <asm/processor.h>
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 #include <mach/ipamap.h>
 #endif
 
@@ -123,7 +123,7 @@ void __setup_dom_pgtable(struct domain *d, addr_t paddr_start, unsigned long map
 	/* 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).
 	 */
-	__create_mapping(new_pt, memslot[slotID].ipa_addr + map_size, __pa(d->avz_shared), PAGE_SIZE, true, S2);
+	__create_mapping(new_pt, memslot[slotID].ipa_addr + map_size, __pa(d->avz_shared), PAGE_SIZE, false, S2);
 
 #ifdef CONFIG_SOO
 	/* Initialize the grant pfn (ipa address) area */
diff --git a/so3/arch/arm64/include/asm/arm_timer.h b/so3/arch/arm64/include/asm/arm_timer.h
index a57d38d7d..a6b990a96 100644
--- a/so3/arch/arm64/include/asm/arm_timer.h
+++ b/so3/arch/arm64/include/asm/arm_timer.h
@@ -24,7 +24,7 @@
 #include <asm/processor.h>
 
 /**
- * In AVZ and ARM64VT we are using the ARM physical timer. The guest domains will
+ * In AVZ we are using the ARM physical timer. The guest domains will
  * rely on virtual timer where an offset can be added.
  */
 
@@ -53,7 +53,7 @@
  * nicely work out which register we want, and chuck away the rest of
  * the code. At least it does so with a recent GCC (4.6.3).
  */
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 
 static inline void arch_timer_reg_write_el2(enum arch_timer_reg reg, u32 val)
 {
@@ -161,7 +161,7 @@ static inline u32 arch_timer_reg_read_cp15(int access, enum arch_timer_reg reg)
 	return 0;
 }
 
-#endif /* CONFIG_ARM64VT */
+#endif /* CONFIG_AVZ */
 
 /**
  * Get the timer frequency
@@ -183,7 +183,7 @@ static inline u64 arch_counter_get_cntvct(void)
 	u64 cnt;
 
 	isb();
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 	cnt = read_sysreg(cntpct_el0);
 #else
 	cnt = read_sysreg(cntvct_el0);
diff --git a/so3/arch/arm64/include/asm/mmu.h b/so3/arch/arm64/include/asm/mmu.h
index 34c913043..e5963f767 100644
--- a/so3/arch/arm64/include/asm/mmu.h
+++ b/so3/arch/arm64/include/asm/mmu.h
@@ -523,7 +523,7 @@ typedef enum { S1, S2 } mmu_stage_t;
 #define VA2PA_WR "w"
 #define va2pa_at(stage, el, rw, va) asm volatile("at " stage el rw ", %0" : : "r"(va) : "memory", "cc");
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 
 typedef struct {
 	addr_t ipa_addr;
@@ -556,7 +556,7 @@ static inline void set_pte_page_S2(u64 *pte, enum dcache_option option)
 		*pte |= S2_PTE_FLAG_NORMAL;
 }
 
-#endif /* CONFIG_ARM64_VT */
+#endif /* CONFIG_AVZ */
 
 static inline void set_pte_table(u64 *pte, enum dcache_option option)
 {
@@ -620,7 +620,7 @@ static inline bool user_space_vaddr(addr_t addr)
 		return true;
 }
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 
 static inline unsigned int get_sctlr(void)
 {
@@ -637,7 +637,7 @@ static inline void set_sctlr(unsigned int val)
 	asm volatile("isb");
 }
 
-#else
+#else /* CONFIG_AVZ */
 
 static inline unsigned int get_sctlr(void)
 {
@@ -654,7 +654,7 @@ static inline void set_sctlr(unsigned int val)
 	asm volatile("isb");
 }
 
-#endif
+#endif /* !CONFIG_AVZ */
 
 extern addr_t __sys_root_pgtable[], __sys_idmap_l1pgtable[], __sys_linearmap_l1pgtable[], __sys_linearmap_l2pgtable[];
 
@@ -678,7 +678,7 @@ extern void __mmu_switch_vttbr(void *root_pgtable_phys);
 
 void __mmu_setup(void *pgtable);
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 void do_ipamap(void *pgtable, ipamap_t ipamap[], int nbelement);
 #endif
 
diff --git a/so3/arch/arm64/include/asm/processor.h b/so3/arch/arm64/include/asm/processor.h
index 1b8ca3d1a..d136b2330 100644
--- a/so3/arch/arm64/include/asm/processor.h
+++ b/so3/arch/arm64/include/asm/processor.h
@@ -648,7 +648,7 @@
 #define SCTLR_ELx_FLAGS	(SCTLR_ELx_M  | SCTLR_ELx_A | SCTLR_ELx_C | \
 			 SCTLR_ELx_SA | SCTLR_ELx_I | SCTLR_ELx_IESB)
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 #define SCTLR_EL2_RES1  (SCTLR_UCI_BIT | SCTLR_nTWE | SCTLR_nTWI \
 		        | SCTLR_UCT_BIT | SCTLR_DZE_BIT)
 #else
diff --git a/so3/arch/arm64/mmu.c b/so3/arch/arm64/mmu.c
index 7322bbc1f..dfe4821a6 100644
--- a/so3/arch/arm64/mmu.c
+++ b/so3/arch/arm64/mmu.c
@@ -88,7 +88,7 @@ static void alloc_init_l3(u64 *l0pgtable, addr_t addr, addr_t end, addr_t phys,
 			/* Attach the L2 PTE to this L3 page table */
 			*l2pte = __pa((addr_t) l3pgtable) & TTB_L2_TABLE_ADDR_MASK;
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 			if (stage == S1)
 				set_pte_table(l2pte, (nocache ? DCACHE_OFF : DCACHE_WRITEALLOC));
 			else
@@ -105,7 +105,7 @@ static void alloc_init_l3(u64 *l0pgtable, addr_t addr, addr_t end, addr_t phys,
 
 		*l3pte = phys & TTB_L3_PAGE_ADDR_MASK;
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 		if (stage == S1)
 			set_pte_page(l3pte, (nocache ? DCACHE_OFF : DCACHE_WRITEALLOC));
 		else
@@ -161,7 +161,7 @@ static void alloc_init_l2(u64 *l0pgtable, addr_t addr, addr_t end, addr_t phys,
 			/* Attach the L1 PTE to this L2 page table */
 			*l1pte = __pa((addr_t) l2pgtable) & TTB_L1_TABLE_ADDR_MASK;
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 			if (stage == S1)
 				set_pte_table(l1pte, (nocache ? DCACHE_OFF : DCACHE_WRITEALLOC));
 			else
@@ -183,7 +183,7 @@ static void alloc_init_l2(u64 *l0pgtable, addr_t addr, addr_t end, addr_t phys,
 		if (((addr | next | phys) & ~BLOCK_2M_MASK) == 0) {
 			*l2pte = phys & TTB_L2_BLOCK_ADDR_MASK;
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 			if (stage == S1)
 				set_pte_block(l2pte, (nocache ? DCACHE_OFF : DCACHE_WRITEALLOC));
 			else
@@ -239,7 +239,7 @@ static void alloc_init_l1(u64 *l0pgtable, addr_t addr, addr_t end, addr_t phys,
 
 			/* Attach the L0 PTE to this L1 page table */
 			*l0pte = __pa((addr_t) l1pgtable) & TTB_L0_TABLE_ADDR_MASK;
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 			if (stage == S1)
 				set_pte_table(l0pte, (nocache ? DCACHE_OFF : DCACHE_WRITEALLOC));
 			else
@@ -260,7 +260,7 @@ static void alloc_init_l1(u64 *l0pgtable, addr_t addr, addr_t end, addr_t phys,
 
 		if (((addr | next | phys) & ~BLOCK_1G_MASK) == 0) {
 			*l1pte = phys & TTB_L1_BLOCK_ADDR_MASK;
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 			if (stage == S1)
 				set_pte_block(l1pte, (nocache ? DCACHE_OFF : DCACHE_WRITEALLOC));
 			else
@@ -712,9 +712,6 @@ void __mmu_switch_kernel(void *pgtable_paddr, bool vttbr)
 	if (vttbr)
 		__mmu_switch_vttbr(pgtable_paddr);
 	else
-#endif
-
-#ifdef CONFIG_ARM64VT
 		__mmu_switch_ttbr0(pgtable_paddr);
 #else
 	__mmu_switch_ttbr1(pgtable_paddr);
@@ -968,6 +965,7 @@ addr_t virt_to_phys_pt(addr_t vaddr)
 
 	l1pte = l1pte_offset(l0pte, vaddr);
 	BUG_ON(!*l1pte);
+	
 #elif CONFIG_VA_BITS_39
 	if (user_space_vaddr(vaddr))
 		l1pte = l1pte_offset((u64 *) current_pgtable(), vaddr);
@@ -1000,7 +998,6 @@ addr_t virt_to_phys_pt(addr_t vaddr)
 
 #ifdef CONFIG_AVZ
 
-#ifdef CONFIG_ARM64VT
 /**
  * Perform a mapping of IPA regions to physical regions
  *
@@ -1017,4 +1014,3 @@ void do_ipamap(void *pgtable, ipamap_t ipamap[], int nbelement)
 
 #endif /* CONFIG_AVZ */
 
-#endif
diff --git a/so3/arch/arm64/rpi4_64/include/mach/ipamap.h b/so3/arch/arm64/rpi4_64/include/mach/ipamap.h
index d7d67ca3e..e7b44c57a 100644
--- a/so3/arch/arm64/rpi4_64/include/mach/ipamap.h
+++ b/so3/arch/arm64/rpi4_64/include/mach/ipamap.h
@@ -25,9 +25,9 @@ ipamap_t agency_ipamap[] = {
 
 	/* I/O Memory space*/
 	{
-		.ipa_addr = 0xf0000000,
-		.phys_addr = 0xf0000000,
-		.size = 0x10000000,
+		.ipa_addr = 0xfc000000,
+		.phys_addr = 0xfc000000,
+		.size = 0x04000000,
 	},
 
 	/* Null pointer exception */
@@ -46,12 +46,13 @@ ipamap_t agency_ipamap[] = {
 ipamap_t capsule_ipamap[] = {
 
 	{
-		/* Only mapping the CPU interface to the vGIC CPU interface.
+	/* Only mapping the CPU interface to the vGIC CPU interface (GICV).
 	 * Access to the distributor must lead to a trap and be handled by the hypervisor.
+	 * BCM2711 GIC-400: GICV (virtual CPU interface) at 0xFF846000.
 	 */
-		.ipa_addr = 0x08010000,
-		.phys_addr = 0x08040000,
-		.size = 0x10000,
+		.ipa_addr = 0xff842000,
+		.phys_addr = 0xff846000,
+		.size = 0x2000,
 	},
 };
 
diff --git a/so3/arch/arm64/traps.c b/so3/arch/arm64/traps.c
index ca7019b5d..3ed751883 100644
--- a/so3/arch/arm64/traps.c
+++ b/so3/arch/arm64/traps.c
@@ -78,10 +78,19 @@ void trap_handle_error(addr_t lr)
 {
 #ifdef CONFIG_AVZ
 	unsigned long esr = read_sysreg(esr_el2);
+	unsigned long far = read_sysreg(far_el2);
+	unsigned long elr = read_sysreg(elr_el2);
+	unsigned long hpfar = read_sysreg(hpfar_el2);
 #else
 	unsigned long esr = read_sysreg(esr_el1);
+	unsigned long far = read_sysreg(far_el1);
+	unsigned long elr = 0;
+	unsigned long hpfar = 0;
 #endif
 
+	printk("  FAR:   %lx\n", far);
+	printk("  ELR:   %lx\n", elr);
+	printk("  HPFAR: %lx (IPA: %lx)\n", hpfar, (hpfar >> 4) << 12);
 	show_invalid_entry_message(ESR_ELx_EC(esr), esr, lr);
 }
 
@@ -123,7 +132,7 @@ void trap_handle(cpu_regs_t *regs)
 	syscall_args_t sys_args;
 #endif
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 
 	unsigned long esr = read_sysreg(esr_el2);
 	unsigned long hvc_code;
@@ -137,7 +146,7 @@ void trap_handle(cpu_regs_t *regs)
 
 #else
 	unsigned long esr = read_sysreg(esr_el1);
-#endif /* CONFIG_ARM64VT */
+#endif /* CONFIG_AVZ */
 
 	switch (ESR_ELx_EC(esr)) {
 	case ESR_ELx_EC_DABT_LOW:
diff --git a/so3/avz/kernel/domain_utils.c b/so3/avz/kernel/domain_utils.c
index e7d610d3a..64b747f58 100644
--- a/so3/avz/kernel/domain_utils.c
+++ b/so3/avz/kernel/domain_utils.c
@@ -259,7 +259,6 @@ void loadAgency(void)
 
 /**
  * The ITB image will be parsed and the components placed in their target memory location.
- * This work only with ARM64VT support.
  *
  * @param slotID
  * @param itb	ITB image
diff --git a/so3/avz/kernel/gnttab.c b/so3/avz/kernel/gnttab.c
index 599e4a164..333694cbf 100644
--- a/so3/avz/kernel/gnttab.c
+++ b/so3/avz/kernel/gnttab.c
@@ -165,7 +165,14 @@ addr_t map_vbstore_pfn(int target_domid, int pfn)
 			else
 				grant_paddr = pfn_to_phys(pfn);
 
-			__create_mapping((addr_t *) d->pagetable_vaddr, grant_paddr, pfn_to_phys(cur->pfn), PAGE_SIZE, true,
+			/*
+			 * The vbstore ring buffer is shared Normal memory between agency
+			 * and ME. Map it Normal cacheable (nocache=false) so that both
+			 * sides see coherent writes via the inner-shareable cache domain.
+			 * Using Device attributes here would break ring-buffer coherency
+			 * with the agency which maps the same page as Normal cacheable.
+			 */
+			__create_mapping((addr_t *) d->pagetable_vaddr, grant_paddr, pfn_to_phys(cur->pfn), PAGE_SIZE, false,
 					 S2);
 
 			return phys_to_pfn(grant_paddr);
diff --git a/so3/avz/kernel/hypercalls.c b/so3/avz/kernel/hypercalls.c
index 072ed76c4..5d626f528 100644
--- a/so3/avz/kernel/hypercalls.c
+++ b/so3/avz/kernel/hypercalls.c
@@ -209,5 +209,6 @@ void do_avz_hypercall(void *__args)
 		break;
 	}
 
-	flush_dcache_all();
+	dsb(ish);   /* inner shareable */
+    	isb();
 }
diff --git a/so3/avz/kernel/setup.c b/so3/avz/kernel/setup.c
index cf7c6eaba..bacac4ef3 100644
--- a/so3/avz/kernel/setup.c
+++ b/so3/avz/kernel/setup.c
@@ -1,5 +1,5 @@
 /*
- * Copyright (C) 2014-2018 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
  * it under the terms of the GNU General Public License version 2 as
diff --git a/so3/avz/kernel/smp.c b/so3/avz/kernel/smp.c
index 283b4e96d..217b38b44 100644
--- a/so3/avz/kernel/smp.c
+++ b/so3/avz/kernel/smp.c
@@ -1,5 +1,5 @@
 /*
- * Copyright (C) 2014-2022 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
  * it under the terms of the GNU General Public License version 2 as
@@ -105,13 +105,21 @@ void secondary_start_kernel(void)
 
 	printk("CPU%u: Booted secondary processor\n", cpu);
 
-#ifndef CONFIG_SOO
+#ifdef CONFIG_SOO
+	if (cpu != ME_CPU)
+#endif /* CONFIG_SOO */
 	__mmu_switch_kernel((void *) domains[DOMID_AGENCY]->pagetable_paddr, true);
-#endif /* !CONFIG_SOO */
-
+ 
 	booted[cpu] = 1;
 
 #ifdef CONFIG_CPU_SPIN_TABLE
+#ifdef CONFIG_SOO
+	/* Agency secondary CPUs are handed directly to Linux via spin-table.
+	 * Set current_domain to agency so HVC calls from EL1 are correctly dispatched.
+	 */
+	if (cpu != ME_CPU)
+		set_current_domain(agency);
+#endif /* CONFIG_SOO */
 	switch (cpu) {
 	case 1:
 		pre_ret_to_el1_spin(CPU1_RELEASE_ADDR);
@@ -119,9 +127,13 @@ void secondary_start_kernel(void)
 	case 2:
 		pre_ret_to_el1_spin(CPU2_RELEASE_ADDR);
 		break;
+	/* CPU #3 is dedicated to capsules in case of CONFIG_SOO */
+#ifndef CONFIG_SOO
 	case 3:
 		pre_ret_to_el1_spin(CPU3_RELEASE_ADDR);
 		break;
+#endif /* !CONFIG_SOO*/
+
 	default:
 		printk("%s: trying to start CPU %d that is not supported.\n", __func__, cpu);
 	}
@@ -213,6 +225,10 @@ void smp_init(void)
 
 #ifdef CONFIG_SOO
 
+	/* Boot agency secondary CPUs so they enter spin-table wait for Linux */
+	for (i = 1; i < ME_CPU; i++)
+		cpu_up(i);
+
 	printk("Starting ME CPU...\n");
 
 	cpu_up(ME_CPU);
@@ -221,7 +237,7 @@ void smp_init(void)
 
 #else /* CONFIG_SOO */
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 	/* With VT support, we prepare the CPU to be started through a HVC call
 	 * from the domain.
 	 */
diff --git a/so3/configs/rpi4_64_avz_soo_defconfig b/so3/configs/rpi4_64_avz_soo_defconfig
new file mode 100644
index 000000000..56a2c6692
--- /dev/null
+++ b/so3/configs/rpi4_64_avz_soo_defconfig
@@ -0,0 +1,90 @@
+#
+# Automatically generated make config: don't edit
+# SO3 Polymorphic OS Configuration
+#
+# CONFIG_ARCH_ARM32 is not set
+CONFIG_ARCH_ARM64=y
+CONFIG_ARCH="arm64"
+CONFIG_CROSS_COMPILE="aarch64-none-elf-"
+# CONFIG_ARM_TRUSTZONE is not set
+CONFIG_KERNEL_VADDR=0x0000100000000000
+
+#
+# Platform
+#
+CONFIG_ARM64VT=y
+# CONFIG_VIRT64 is not set
+CONFIG_RPI4_64=y
+# CONFIG_VA_BITS_39 is not set
+CONFIG_VA_BITS_48=y
+CONFIG_THREAD_ENV=y
+
+#
+# Kernel & CPU features
+#
+CONFIG_MAX_THREADS=32
+CONFIG_SMP=y
+CONFIG_NR_CPUS=4
+# CONFIG_CPU_PSCI is not set
+CONFIG_CPU_SPIN_TABLE=y
+CONFIG_HZ=100
+CONFIG_SCHED_FLIP_SCHEDFREQ=30
+
+#
+# SO3 Scheduling configuration
+#
+CONFIG_SCHED_RR=y
+# CONFIG_SCHED_PRIO is not set
+CONFIG_SCHED_FREQ_PREEMPTION=y
+
+#
+# Drivers
+#
+CONFIG_UART=y
+CONFIG_IO_MAPPING_BASE=0x0000200000000000
+# CONFIG_I2C is not set
+# CONFIG_NET is not set
+# CONFIG_FB is not set
+# CONFIG_INPUT is not set
+# CONFIG_NS16550 is not set
+CONFIG_BCM283x_MU_UART=y
+CONFIG_UART_LL_PADDR=0xfe215040
+# CONFIG_MMC is not set
+# CONFIG_RAMDEV is not set
+CONFIG_ARM_TIMER=y
+CONFIG_GIC=y
+
+#
+# SO3 Applications
+#
+# CONFIG_APP_SAMPLE is not set
+# CONFIG_APP_REFSO3 is not set
+
+#
+# Filesystems
+#
+CONFIG_ROOTFS_NONE=y
+# CONFIG_ROOTFS_MMC is not set
+# CONFIG_ROOTFS_RAMDEV is not set
+
+#
+# IPC
+#
+# CONFIG_IPC_SIGNAL is not set
+# CONFIG_IPC_PIPE is not set
+CONFIG_HEAP_SIZE_MB=8
+CONFIG_SYS_STACK_SIZE_KB=64
+CONFIG_THREAD_STACK_SIZE_KB=64
+# CONFIG_RTOS is not set
+CONFIG_AVZ=y
+CONFIG_USER_INIT_PROGRAM="init.elf"
+# CONFIG_LOG_LEVEL_CRITICAL is not set
+# CONFIG_LOG_LEVEL_ERROR is not set
+# CONFIG_LOG_LEVEL_WARNING is not set
+CONFIG_LOG_LEVEL_INFO=y
+# CONFIG_LOG_LEVEL_DEBUG is not set
+# CONFIG_LOG_LEVEL_TRACE is not set
+# CONFIG_LOG_LEVEL_NONE is not set
+CONFIG_LOG_LEVEL=4
+CONFIG_SOO=y
+CONFIG_MMU=y
diff --git a/so3/devices/irq/gic.c b/so3/devices/irq/gic.c
index 6eb54bf16..2b5654e81 100644
--- a/so3/devices/irq/gic.c
+++ b/so3/devices/irq/gic.c
@@ -71,7 +71,7 @@ gic_t *gic;
 
 DEFINE_PER_CPU(spinlock_t, intc_lock);
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 
 #define MAX_PENDING_IRQS 256
 
@@ -112,7 +112,7 @@ void display_lr(unsigned int n)
 	printk("  - hw: %x\n", lr & GICH_LR_HW_BIT);
 }
 
-#endif /* CONFIG_ARM64VT */
+#endif /* CONFIG_AVZ */
 
 /**
  * Retrieve the information related to an interrupt entry from the DT.
@@ -218,7 +218,7 @@ int irq_set_affinity(unsigned int irq, int cpu)
 	return 0;
 }
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 
 static void gic_enable_maint_irq(bool enable)
 {
@@ -298,7 +298,7 @@ void gic_inject_pending(void)
                  */
 		dmb(ish);
 
-		pending_irqs.head = (pending_irqs.head + -1) % MAX_PENDING_IRQS;
+		pending_irqs.head = (pending_irqs.head + 1) % MAX_PENDING_IRQS;
 	}
 
 	/*
@@ -359,9 +359,6 @@ void gic_clear_pending_irqs(void)
 	iowrite32(&gic->gich->apr, 0);
 }
 
-#endif /* CONFIG_ARM64VT */
-
-#ifdef CONFIG_AVZ
 void gich_init(void)
 {
 	u32 gicc_ctlr, gicc_pmr;
diff --git a/so3/devices/timer/arm_timer.c b/so3/devices/timer/arm_timer.c
index 40b0ee4ee..4486ad9d2 100644
--- a/so3/devices/timer/arm_timer.c
+++ b/so3/devices/timer/arm_timer.c
@@ -38,7 +38,7 @@ static void next_event(u32 next)
 {
 	unsigned long ctrl;
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 	ctrl = arch_timer_reg_read_el2(ARCH_TIMER_REG_CTRL);
 #else
 	ctrl = arch_timer_reg_read_cp15(ARCH_TIMER_VIRT_ACCESS, ARCH_TIMER_REG_CTRL);
@@ -47,7 +47,7 @@ static void next_event(u32 next)
 	ctrl |= ARCH_TIMER_CTRL_ENABLE;
 	ctrl &= ~ARCH_TIMER_CTRL_IT_MASK;
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 	arch_timer_reg_write_el2(ARCH_TIMER_REG_TVAL, next);
 	arch_timer_reg_write_el2(ARCH_TIMER_REG_CTRL, ctrl);
 #else
@@ -65,7 +65,7 @@ static irq_return_t timer_isr(int irq, void *dev)
 
 	/* Clear the interrupt */
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 	ctrl = arch_timer_reg_read_el2(ARCH_TIMER_REG_CTRL);
 #else
 	ctrl = arch_timer_reg_read_cp15(ARCH_TIMER_VIRT_ACCESS, ARCH_TIMER_REG_CTRL);
@@ -74,7 +74,7 @@ static irq_return_t timer_isr(int irq, void *dev)
 	if (ctrl & ARCH_TIMER_CTRL_IT_STAT) {
 		ctrl |= ARCH_TIMER_CTRL_IT_MASK;
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 		arch_timer_reg_write_el2(ARCH_TIMER_REG_CTRL, ctrl);
 #else
 		arch_timer_reg_write_cp15(ARCH_TIMER_VIRT_ACCESS, ARCH_TIMER_REG_CTRL, ctrl);
@@ -116,13 +116,13 @@ void secondary_timer_init(void)
 {
 	arm_timer_t *arm_timer = (arm_timer_t *) dev_get_drvdata(periodic_timer.dev);
 
-#ifndef CONFIG_ARM64VT
+#ifndef CONFIG_AVZ
 	unsigned long ctrl;
 #endif
 
 	/* Shutdown the timer */
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 	arch_timer_reg_write_el2(ARCH_TIMER_REG_CTRL, 0);
 #else
 
@@ -140,7 +140,7 @@ void secondary_timer_init(void)
  */
 static int periodic_timer_init(dev_t *dev, int fdt_offset)
 {
-#ifndef CONFIG_ARM64VT
+#ifndef CONFIG_AVZ
 	unsigned long ctrl;
 #endif
 	arm_timer_t *arm_timer;
@@ -167,7 +167,7 @@ static int periodic_timer_init(dev_t *dev, int fdt_offset)
 
 	/* Shutdown the timer */
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 	arch_timer_reg_write_el2(ARCH_TIMER_REG_CTRL, 0);
 #else
 
diff --git a/so3/dts/Makefile b/so3/dts/Makefile
index e0acd87d9..d577cdfc6 100644
--- a/so3/dts/Makefile
+++ b/so3/dts/Makefile
@@ -1,12 +1,16 @@
 
 dtb-$(CONFIG_RPI4) += rpi4.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_VIRT64) += virt64.dtb virt64_avz.dtb virt64_lvperf.dtb
 dtb-$(CONFIG_VIRT32) += virt32.dtb virt32_lvperf.dtb
 
 ifeq ($(CONFIG_SOO),y)
+
 ifeq ($(CONFIG_AVZ),)
 
+dtb-$(CONFIG_VIRT64) += virt64_capsule.dtb
+dtb-$(CONFIG_RPI4_64) += rpi4_64_capsule.dtb
+
 ifeq ($(CONFIG_SOO_REFSO3),y)
 ifeq ($(CONFIG_RAMDEV),y)
 dtb-y += refso3_ramfs.dtb  
diff --git a/so3/dts/rpi4_64_avz.dts b/so3/dts/rpi4_64_avz.dts
index ede720f3f..3c6ce229d 100644
--- a/so3/dts/rpi4_64_avz.dts
+++ b/so3/dts/rpi4_64_avz.dts
@@ -47,10 +47,9 @@
 		#interrupt-cells = <3>;
 		
 		/* GIC dist, cpu, hyp */
-		reg = <0x0 0x08000000 0x0 0x10000 
-		       0x0 0x08010000 0x0 0x10000
-		       0x0 0x08030000 0x0 0x10000>;
-		       
+		reg =	<0x0 0xff841000 0x0 0x1000>,
+			<0x0 0xff842000 0x0 0x2000>,
+			<0x0 0xff844000 0x0 0x2000>;
 		status = "ok";
 	};
 	
diff --git a/so3/dts/rpi4_64_capsule.dts b/so3/dts/rpi4_64_capsule.dts
new file mode 100644
index 000000000..02b672ecf
--- /dev/null
+++ b/so3/dts/rpi4_64_capsule.dts
@@ -0,0 +1,125 @@
+/*
+ * Copyright (C) 2014-2019 Daniel Rossier <daniel.rossier@heig-vd.ch>
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License version 2 as
+ * published by the Free Software Foundation.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
+ *
+ */
+
+/dts-v1/;
+
+/ {
+	model = "SO3 RPi4 64-bit capsule machine";
+	compatible = "arm,virt64";
+
+	#address-cells = <2>;
+	#size-cells = <2>;
+
+	cpus {
+		device_type = "cpu";
+		compatible = "arm,virt64";
+	};
+
+	memory {
+		device_type = "memory";
+		reg = <0x0 0x41000000 0x0 0x4000000>; /* 64 MB */
+	};
+
+	mem {
+		compatible = "mem";
+		status = "ok";
+	};
+
+	soo-serial {
+		compatible = "soo-serial";
+		status = "ok";
+	};
+
+	/* SO3 virtual timer managed by AVZ */
+
+	soo-timer {
+		compatible = "soo-timer,periodic-timer";
+		status = "ok";
+	};
+
+	/* Free-running clocksource */
+	clocksource-timer {
+		compatible = "soo-timer,clocksource-timer";
+		status = "ok";
+	};
+
+	oneshot-timer {
+		compatible = "soo-timer,oneshot-timer";
+		status = "ok";
+	};
+
+	/*
+	 * GIC interrupt controller - BCM2711 GIC-400 addresses.
+	 * GICD at 0xFF841000: stage-2 fault -> AVZ MMIO emulation.
+	 * GICC at 0xFF842000: stage-2 mapped to GICV at 0xFF846000.
+	 */
+	gic: interrupt-controller@0xff841000 {
+		compatible = "intc,gic";
+		interrupt-controller;
+		#interrupt-cells = <3>;
+
+		/* GIC dist, cpu */
+		reg = <0x0 0xff841000 0x0 0x1000
+		       0x0 0xff842000 0x0 0x2000>;
+
+		status = "ok";
+	};
+
+	mydev {
+		compatible = "arm,mydev";
+		status = "ok";
+	};
+
+	ME {
+   		/* SPID on 64-bit encoding */
+        	spid = /bits/ 64 <0x0030000000000003>;
+
+		 /* Name of this ME */
+		me_name = "SOO.refso3";
+
+		/* Short description */
+		me_shortdesc =
+
+		"This is the standard reference ME that can be used as template or simply to \n \
+		perform various tests. This variant includes a rootfs with some user space \n \
+		applications.";
+
+		frontends {
+
+			/* Enabling vdummy for testing purposes */
+			vdummy {
+				compatible = "vdummy,frontend";
+				status = "disabled";
+			};
+
+			/* Enabling the console */
+			vuart {
+				compatible = "vuart,frontend";
+				status = "ok";
+			};
+
+			/* Enabling vlogs - logging supports */
+			vlogs {
+				compatible = "vlogs,frontend";
+				status = "ok";
+			};
+		};
+	};
+
+
+};
diff --git a/so3/kernel/psci_smp.c b/so3/kernel/psci_smp.c
index 76232a9e4..75de8c2de 100644
--- a/so3/kernel/psci_smp.c
+++ b/so3/kernel/psci_smp.c
@@ -69,7 +69,7 @@ void cpu_on(unsigned long cpuid, addr_t entry_point)
 {
 	int ret;
 
-#ifdef CONFIG_ARM64VT
+#ifdef CONFIG_AVZ
 	ret = __invoke_psci_fn_smc(PSCI_0_2_FN_CPU_ON, cpuid, entry_point, 0);
 #else
 	ret = __invoke_psci_fn_hvc(PSCI_0_2_FN_CPU_ON, cpuid, entry_point, 0);
diff --git a/so3/mm/Kconfig b/so3/mm/Kconfig
index eeb64c18f..a252c6849 100644
--- a/so3/mm/Kconfig
+++ b/so3/mm/Kconfig
@@ -3,7 +3,7 @@ config KERNEL_VADDR
 	hex "Virtual base address of the SO3 kernel or hypervisor"
 	default 0xff000000 if ARM32
 	default 0xffff700000000000 if ARM64 
-	default 0x100000000000 if ARM64VT
+	default 0x100000000000 if AVZ
 	
 config HEAP_SIZE_MB
 	int "Size of the heap (MB)"
diff --git a/so3/soo/kernel/hypervisor.c b/so3/soo/kernel/hypervisor.c
index 8f21d3621..94f984fc4 100644
--- a/so3/soo/kernel/hypervisor.c
+++ b/so3/soo/kernel/hypervisor.c
@@ -20,6 +20,8 @@
 #include <bitops.h>
 #include <heap.h>
 
+#include <asm/mmu.h>
+
 #include <avz/uapi/avz.h>
 
 #include <soo/console.h>
@@ -45,6 +47,16 @@ void avz_get_shared(void)
 
 	avz_shared = (avz_shared_t *) io_map(args.u.avz_domctl_args.domctl.avz_shared_paddr, PAGE_SIZE);
 	BUG_ON(!avz_shared);
+
+	/*
+	 * io_map() uses Device-nGnRnE memory attributes. The AVZ shared page
+	 * must be Normal (cacheable) memory: exclusive/atomic operations (xchg)
+	 * on Device memory are CONSTRAINED UNPREDICTABLE on Cortex-A72 and
+	 * generate a deferred SError (ESR: bf000002).
+	 * Override the PTE with Normal cacheable attributes.
+	 */
+	create_mapping(NULL, (addr_t) avz_shared,
+		       args.u.avz_domctl_args.domctl.avz_shared_paddr, PAGE_SIZE, false);
 }
 
 void avz_printch(char c)
diff --git a/so3/soo/kernel/setup.c b/so3/soo/kernel/setup.c
index 45d8a5708..86a7e4ab7 100644
--- a/so3/soo/kernel/setup.c
+++ b/so3/soo/kernel/setup.c
@@ -97,6 +97,17 @@ void post_init_setup(void)
 	__intf = (void *) io_map(pfn_to_phys(avz_shared->dom_desc.u.ME.vbstore_pfn), PAGE_SIZE);
 	BUG_ON(!__intf);
 
+	/*
+	 * io_map() uses Device-nGnRnE memory attributes (Stage-1). The vbstore
+	 * ring buffer is shared with the agency which maps it as Normal cacheable.
+	 * Both Stage-1 and Stage-2 must be Normal so the combined effective
+	 * memory type is Normal cacheable, enabling hardware cache coherency
+	 * (inner-shareable) for the ring buffer protocol.
+	 * Override the Stage-1 PTE with Normal cacheable attributes.
+	 */
+	create_mapping(NULL, (addr_t) __intf,
+		       pfn_to_phys(avz_shared->dom_desc.u.ME.vbstore_pfn), PAGE_SIZE, false);
+
 	LOG_INFO("SOO Mobile Entity booting ...\n");
 
 	soo_guest_activity_init();
diff --git a/target/rpi4_64.its b/target/rpi4_64.its
index b4f32f965..01a633d1f 120000
--- a/target/rpi4_64.its
+++ b/target/rpi4_64.its
@@ -1 +1 @@
-rpi4_64_so3.its
\ No newline at end of file
+rpi4_64_avz_so3.its
\ No newline at end of file
diff --git a/target/rpi4_64_capsule.its b/target/rpi4_64_capsule.its
new file mode 100644
index 000000000..9ebff9b61
--- /dev/null
+++ b/target/rpi4_64_capsule.its
@@ -0,0 +1,75 @@
+/*
+ * Copyright (C) 2020 Daniel Rossier <daniel.rossier@heig-vd.ch>
+ *
+ * This program is free software; you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License version 2 as
+ * published by the Free Software Foundation.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA
+ *
+ */
+
+/dts-v1/;
+
+/ {
+	description = "Kernel and rootfs components for rpi4_64 (armv8) environment";
+
+	images {
+
+	so3 {
+			description = "SO3 OS kernel";
+			data = /incbin/("../so3/so3.bin");
+			type = "guest";
+			arch = "arm64";
+			os = "linux";
+			compression = "none";
+            		load = <0x41080000>;
+			entry = <0x41080000>;
+		};
+
+        fdt {
+			description = "Flattened Device Tree blob";
+			data = /incbin/("../so3/dts/rpi4_64_capsule.dtb");
+			type = "flat_dt";
+			arch = "arm64";
+			compression = "none";
+			load = <0x43000000>;
+		};
+
+        ramfs {
+        	description = "SO3 environment minimal rootfs";
+			data = /incbin/("../rootfs/rootfs.fat");
+			type = "ramdisk";
+			arch = "arm64";
+			os = "linux";
+			compression = "none";
+			load = <0x43500000>;
+    	};
+
+};
+
+	configurations {
+		default = "so3_ramfs";
+
+		so3_ramfs {
+			description = "SO3 kernel image including device tree";
+			kernel = "so3";
+			fdt = "fdt";
+            ramdisk = "ramfs";
+		};
+
+        so3_mmc {
+			description = "SO3 kernel image including device tree";
+			kernel = "so3";
+			fdt = "fdt";
+		};
+	};
+
+};