From 64c5982a1e922817bee194be460cb0f9ffba3165 Mon Sep 17 00:00:00 2001 From: yimingzhou2002 Date: Wed, 1 Apr 2026 03:51:20 +0000 Subject: [PATCH] feat: support on 3 set of shmem blocks Signed-off-by: yimingzhou2002 --- kernel/include/kernel/boot.h | 4 +- kernel/src/arch/arm/kernel/boot.c | 81 +++++++++++++++++-------------- 2 files changed, 47 insertions(+), 38 deletions(-) diff --git a/kernel/include/kernel/boot.h b/kernel/include/kernel/boot.h index 97b5e11..f52e3f5 100755 --- a/kernel/include/kernel/boot.h +++ b/kernel/include/kernel/boot.h @@ -106,8 +106,8 @@ typedef struct { pptr_t vspace; pptr_t asid_pool; pptr_t ipc_buf; - pptr_t shm_root_queue; - pptr_t shm_sel4_queue; + pptr_t shm_root_queue[5]; + pptr_t shm_sel4_queue[5]; pptr_t shm_data; pptr_t boot_info; pptr_t extra_bi; diff --git a/kernel/src/arch/arm/kernel/boot.c b/kernel/src/arch/arm/kernel/boot.c index e5c2842..d8c0d0d 100755 --- a/kernel/src/arch/arm/kernel/boot.c +++ b/kernel/src/arch/arm/kernel/boot.c @@ -573,38 +573,42 @@ static BOOT_CODE bool_t try_init_kernel( cap_t shm_tx_queue_cap, shm_rx_queue_cap; // 计算虚拟地址 (页面对齐) - 使用原始计算方式 - vptr_t shm_tx_queue_vaddr = ((extra_bi_frame_vptr + extra_bi_size_bits + BIT(PAGE_BITS) * 2) >> PAGE_BITS) << PAGE_BITS; + vptr_t shm_tx_queue_vaddr = extra_bi_frame_vptr + extra_bi_size_bits + BIT(PAGE_BITS) * 2; + assert(!(shm_tx_queue_vaddr%BIT(PAGE_BITS))); vptr_t shm_rx_queue_vaddr = shm_tx_queue_vaddr + BIT(PAGE_BITS); // TX 队列后 4KB (1页) - vptr_t shm_data_vaddr = shm_rx_queue_vaddr + BIT(PAGE_BITS); // RX 队列后 4KB (1页) + vptr_t shm_data_vaddr = shm_tx_queue_vaddr + 6*BIT(PAGE_BITS); // RX 队列后 4KB (1页) // HyperAMP 4KB 队列布局 (HYPERAMP_MAX_MAP_TABLE_ENTRIES=125): // TX Queue (Linux → seL4): phys 0xDE000000, virt shm_tx_queue_vaddr, size 4KB // RX Queue (seL4 → Linux): phys 0xDE001000, virt shm_rx_queue_vaddr, size 4KB // Data Region: phys 0xDE002000, virt shm_data_vaddr, size 4MB - - rootserver.shm_root_queue = (pptr_t)paddr_to_pptr(SHM_TX_QUEUE_PADDR); // TX Queue - rootserver.shm_sel4_queue = (pptr_t)paddr_to_pptr(SHM_RX_QUEUE_PADDR); // RX Queue + + for (int i = 0; i < 3; i++) + { + rootserver.shm_root_queue[i] = (pptr_t)paddr_to_pptr(SHM_TX_QUEUE_PADDR+i*BIT(PAGE_BITS)); // TX Queue + rootserver.shm_sel4_queue[i] = (pptr_t)paddr_to_pptr(SHM_RX_QUEUE_PADDR+i*BIT(PAGE_BITS)); // RX Queue + // 创建 TX Queue 映射 (Linux → seL4, 4KB) + shm_tx_queue_cap = create_ShmemCommbuf_frame_cap(root_cnode_cap, it_pd_cap, + shm_tx_queue_vaddr, + rootserver.shm_root_queue[i], + seL4_CapInitThreadShm_root_q); - // 创建 TX Queue 映射 (Linux → seL4, 4KB) - shm_tx_queue_cap = create_ShmemCommbuf_frame_cap(root_cnode_cap, it_pd_cap, - shm_tx_queue_vaddr, - rootserver.shm_root_queue, - seL4_CapInitThreadShm_root_q); - if (cap_get_capType(shm_tx_queue_cap) == cap_null_cap) { - printf("ERROR: could not create TX queue (4KB) for initial thread\n"); - return false; - } - - // 创建 RX Queue 映射 (seL4 → Linux, 4KB) - shm_rx_queue_cap = create_ShmemCommbuf_frame_cap(root_cnode_cap, it_pd_cap, - shm_rx_queue_vaddr, - rootserver.shm_sel4_queue, - seL4_CapInitThreadShm_sel4_q); - if (cap_get_capType(shm_rx_queue_cap) == cap_null_cap) { - printf("ERROR: could not create RX queue (4KB) for initial thread\n"); - return false; + // 创建 RX Queue 映射 (seL4 → Linux, 4KB) + shm_rx_queue_cap = create_ShmemCommbuf_frame_cap(root_cnode_cap, it_pd_cap, + shm_rx_queue_vaddr, + rootserver.shm_sel4_queue[i], + seL4_CapInitThreadShm_sel4_q); + + if ((cap_get_capType(shm_rx_queue_cap) == cap_null_cap) + ||(cap_get_capType(shm_tx_queue_cap) == cap_null_cap)) { + printf("ERROR: could not create TX/RX queue (4KB) for initial thread\n"); + return false; + } + //renew tx rx vaddr + shm_tx_queue_vaddr+=2*BIT(PAGE_BITS); + shm_rx_queue_vaddr+=2*BIT(PAGE_BITS); } - + printf("boot.c HyperAMP 4KB Queue Layout:\n"); printf(" extra_bi_frame_vptr: 0x%lx\n", extra_bi_frame_vptr); printf(" extra_bi_size_bits: %lu (0x%lx)\n", extra_bi_size_bits, extra_bi_size_bits); @@ -621,20 +625,24 @@ static BOOT_CODE bool_t try_init_kernel( printf("TX and RX queue mapped, mapping 4MB data region\n"); // 映射 4MB 数据区 (保持原有实现) - p_region_t shm_data_p_reg = (p_region_t) { - SHM_DATA_PADDR, SHM_DATA_PADDR + SHM_DATA_SIZE - }; - region_t shm_data_reg = paddr_to_pptr_reg(shm_data_p_reg); + // p_region_t shm_data_p_reg = (p_region_t) { + // SHM_DATA_PADDR, SHM_DATA_PADDR + SHM_DATA_SIZE + // }; + // region_t shm_data_reg = paddr_to_pptr_reg(shm_data_p_reg); - v_region_t shm_data_v_reg = { - .start = shm_data_vaddr, - .end = shm_data_vaddr + SHM_DATA_SIZE - }; + // v_region_t shm_data_v_reg = { + // .start = shm_data_vaddr, + // .end = shm_data_vaddr + SHM_DATA_SIZE + // }; - printf("data pptr 0x%lx vaddr 0x%lx\n", shm_data_reg.start, shm_data_v_reg.start); - map_4MB_phys_to_vaddr((vspace_root_t *)rootserver.vspace, SHM_DATA_PADDR, shm_data_vaddr, 0); - printf("data pptr 0x%lx vaddr 0x%lx\n", shm_data_reg.start, shm_data_v_reg.start); - + for (int i = 0; i < 3; i++) + { + paddr_t phys_start=SHM_DATA_PADDR + i*BIT(22); + vptr_t vaddr_start=shm_data_vaddr + i*BIT(22); + map_4MB_phys_to_vaddr((vspace_root_t *)rootserver.vspace,phys_start,vaddr_start, 0); + printf("%dth 4MB data block",i); + printf("data pptr 0x%lx vaddr 0x%lx\n", phys_start, vaddr_start); + } // 注意: 不要在内核中直接写入共享内存! // 内核直接映射区使用 cacheable 属性,会导致缓存不一致问题 // 应该由用户空间程序通过 uncached 映射进行初始化 @@ -704,6 +712,7 @@ static BOOT_CODE bool_t try_init_kernel( ipcBuf[3] = shm_tx_queue_vaddr; // msg[2] ipcBuf[4] = shm_rx_queue_vaddr; // msg[3] ipcBuf[5] = shm_data_vaddr; // msg[4] + //TODO: renew this section to accomodate latest 3*3 vaddr parmas revision printf("kernel: IPC buffer msg[2..4] = 0x%lx, 0x%lx, 0x%lx\n", ipcBuf[3], ipcBuf[4], ipcBuf[5]); } -- Gitee