March 2021 - Devel - lists.sel4.systems

Stuck during invalidate local TLB in Tx2
by Muneeswaran Rajendran 16 Oct '24

16 Oct '24

Hi seL4 Dev team, Can someone explain the reason (share the reference) to invalidate the local TLB during kernel vspace activation as part CPU initialisation. The Tx2 board stuck while performing this operation. As per my understanding both Tx1 and Tx2 are using same A57 core. so the TLB initialisation and invalidation remain same for Tx2 and should not stuck during invalidation.Please correct me if anything wrong here. I understand from that instruction (tlbi vmalle1) which is invalidating stage 1 entries associated to the current VMID. Also from arm mmu code the seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as 16bit and page table setup 4k granular size. I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the state of processor but its throwing synchronous exception. Do we have any other option to dump all the register content to see the state of processor like we have one in 'sel4debug_dump_registers' which is used in sel4test code. Regards, Muneeswaran R

3 4

Questions about Memory Management in seL4
by Daniel Wang 19 May '23

19 May '23

Hi all, Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me? 1. where is the kernel’s address space? I know there are basically three methods: a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode c) privilege region in each process’s virtual address space, e.g. through page table to map kernel address into use-mode process. My question is which of this is being used by seL4 microkernel? 2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space? 3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page? The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on? Thanks -Dan

5 4

gic v2 vs gic v3
by Chris Koziarz 09 Jul '21

09 Jul '21

Hi all, I'm trying to port camkes-arm-vm to a different platform, that supports gic-v3 In the process, I hit a compilation error: Building C object kernel/CMakeFiles/kernel_all_pp_...rapper_temp_lib.dir/ kernel_all_pp_prune_wrapper_temp.c.obj FAILED: kernel/kernel_all_pp_prune_wrapper_temp.c In file included from /home/chris/camkes-tqma8xqp- vm/kernel/src/arch/arm/object/vcpu.c:15: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v2.h:23: error: "IRQ_MASK" redefined [-Werror] 23 #define IRQ_MASK MASK(10u) In file included from kernel/gen_headers/plat/platform_gen.h:23, from /home/chris/camkes-tqma8xqp-vm/kernel/include/plat/ default/plat/machine.h:8, from /home/chris/camkes-tqma8xqp- vm/kernel/include/machine.h:9, from /home/chris/camkes-tqma8xqp- vm/kernel/include/api/syscall.h:10, from /home/chris/camkes-tqma8xqp- vm/kernel/src/api/faults.c:10: /home/chris/camkes-tqma8xqp-vm/kernel/include/arch/arm/arch/machine/gic_v3.h:30: note: this is the location of the previous definition 30 #define IRQ_MASK MASK(16u) which is an indicative that both gic_v3.h & gic_v2.h headers have been included, which is an error because said headers are not compatible: kernel/include/arch/arm/arch/machine/gic_v3.h:#define IRQ_MASK MASK(16u) kernel/include/arch/arm/arch/machine/gic_v2.h:#define IRQ_MASK MASK(10u) So my question is: how can I configure the build to avoid such a conflict? I can grepp the relevant configuration option in CMakeCache.txt: build_tqma8/CMakeCache.txt:CONFIGURE_INTERRUPT_CONTROLLER:INTERNAL=arch/machine/gic_v3.h but cannot see it in ccmake gui because it's "INTERNAL" What is the solution? - replace this option somehow to use gic_v2 and have my HW use gic v.2, or - change compilation options to use gic_v3 everywhere Thanks for any help, Chris.

4 5

hello_rumprun app not worked
by MOHAMAD REZA SHAFIEI 13 Jun '21

13 Jun '21

hi. i'm recently worked on sel4 with camkes framework. when i compile rumprun_hello on x86_64 platform its compiled and build correctly but when run with qemu by ./simulate script, program crashed with this errors: simple_get_extended_bootinfo_length@simple.h:600 simple_get_extended_bootinfo_length not implemented FAULT HANDLER: data fault from hello.hello_0_control (ID 0x1) on address 0x8, pc = 0x402b7f, fsr = 0x6 FAULT HANDLER: Register dump: FAULT HANDLER: rip :0x402b7f , . . so i found that this method not implemented yet so i return 0 in this method and resolved. for second problem that cause failure if trace program and i found that in "init rumprun" process the program failed in the /projects/sel4runtime/include/sel4_arch/x86_64/sel4runtime/thread_arch.h file and sel4runtime_set_tls_base method. so i read git log and in recently commit your team use sel4runtime for thread TLS, so when we run rumprun_hello, the program failed in sel4runtime_set_tls_base method. can you help me fix this bug? thanks for your attention. -- This email was Anti Virus checked by Security Gateway.

4 4

MMC wait after second command in intialization with mmc_init
by MOHAMAD REZA SHAFIEI 13 Jun '21

13 Jun '21

hi there . i'm work on mmc storage with sel4. i wrote a simple app that use mmc an here is that : ////////////////////////////////////////////////////////////////////// static int count = 0; ps_io_ops_t io_ops = {0}; struct netif* net_if; mmc_card_t mmc_card = 0; sdio_host_dev_t sdio_host_dev; int mmc_found = 0; void mmc_irq_handle(ps_irq_t* irq) { printf("mmc irq handle .... \n"); if(!mmc_found){ mmc_irq_acknowledge(irq); // printf("mmc not found yet :)\n"); sdio_host_dev.handle_irq(&sdio_host_dev,irq->irq.number); return ; } mmc_irq_acknowledge(irq); mmc_handle_irq(mmc_card,irq->irq.number); } int run(void) { notification = timer_notification(); int err = camkes_io_ops(&io_ops); if (err != 0) { ZF_LOGF("Can not init ops : %d\n", err); }; printf("initialize sdhc1 ...\n"); err = sdio_init(SDHC1, &io_ops, &sdio_host_dev); // while card not present check while(sdio_host_dev.reset(&sdio_host_dev) == -1){ delay(1000); } printf("before mmc_init\n"); mmc_init(&sdio_host_dev, &io_ops, &mmc_card); mmc_found = 1; printf("after mmc_init\n"); if (!err) { printf("SDHC1 inited successfully.\n"); } else { printf("SDHC1 initizatino failed!: %d", err); } while (true) { printf(".\n"); delay(1000); } return 0; //////////////////////////////////////////////// its work but in mmc_init after going to mmc_reset , first command sent but in second command (ie MMC_SEND_EXT_CSD ) wait for ever... can any body help me? best regards -- This email was Anti Virus checked by Security Gateway.

2 1

Generating CAmkES glue-spec and glue-proofs
by Ben Fiedler 11 May '21

11 May '21

Hi everyone, I'm having troubles generating the CAmkES glue component specification and proofs from our source. I can and have successfully generated the ADL/CDL spec and implementations using the documented CMake parameters. Grepping around the docs I've found references to a 'camkes.sh' script, but neither the project tree nor the files generated during build contain it. One candidate reason could be that we set up our build environment strangely: We currently check out seL4/camkes-manifest and then symlink our component into the 'projects/global-components' subtree of the seL4. This works for generating bootable images, but I haven't found out how to generate the glue spec yet. Why we have set it up this way I don't know, and I suspect that there is a right way TM that we have overlooked/not found in the documentation. I appreciate any help in this regard. Thanks and have a nice day! Cheers, Ben

4 6

Reducing memory footprint - RISC-V
by porter.188＠osu.edu 19 Apr '21

19 Apr '21

I'm trying to build a low memory footprint of RISC-V based seL4. I'm using QEMU/spike for now. In seL4 12.0 I can modify spike.dts to 8.5 MB of memory 0x00880000. 42 memory@80000000 { 43 device_type = "memory"; 44 reg = <0x00000000 0x80000000 0x00000000 0x00880000>; 45 }; This is the smallest value that builds, lower than this I get the error: [0/1] Re-running CMake... -- Found GCC with prefix riscv64-unknown-linux-gnu- STATUS,KernelDTSList: tools/dts/spike.dts -- /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating... STATUS,platform_yaml: /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml -- Detecting cached version of: musllibc -- Found valid cache entry for musllibc -- Configuring done -- Generating done -- Build files have been written to: /mnt/data/femur_12.0/build [18/36] Generating gen_headers/image_start_addr.h FAILED: elfloader-tool/gen_headers/image_start_addr.h cd /mnt/data/femur_12.0/build/elfloader-tool && sh -c "/mnt/data/femur_12.0/tools/elfloader-tool/../cmake-tool/helpers/shoehorn.py /mnt/data/femur_12.0/build/kernel/gen_headers/plat/machine/platform_gen.yaml /mnt/data/femur_12.0/build/elfloader-tool/archive.o > /mnt/data/femur_12.0/build/elfloader-tool/gen_headers//image_start_addr.h" shoehorn: fatal error: ELF-loader image "/mnt/data/femur_12.0/build/elfloader-tool/archive.o" of size 0x107548 does not fit within any memory region described in "{'devices': [{'end': 2147483648, 'start': 0}, {'end': 549755809792, 'start': 2155872256}], 'memory': [{'end': 2155872256, 'start': 2149580800}]}" ninja: build stopped: subcommand failed. What do I need to modify to get to < 2 MB? Thanks!

4 8

About the BuildSystem of seL4
by Jerry Zhou 29 Mar '21

29 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

2 2

seL4 as bootloader
by Isaac Beckett 29 Mar '21

29 Mar '21

The Linux kernel has support via the EFISTUB module to be loaded directly as an EFI bootloader, which if I recall correctly, also allows it to chainload another OS and be used as a fully-fledged multiboot bootloader. Is it practical to do something similar with seL4? Obviously on non-UEFI platforms it'd be entirely different code, but still.

2 1

About the BuildSystem of seL4
by zhouchunhua＠lixiang.com 26 Mar '21

26 Mar '21

Hi guys, I am a newbie of seL4 and I am trying to get some understanding of it. So, my first question is about the build system of seL4: 1. Why cmake has been taken to build it? I think there are at least two shortcomings about current build system based on CMakeLists.txt: - Some build options were implied in the CMakeLists.txt. It's not easy to get a complete and comprehensive understanding of all the options. And some options depends on other options. Such as, ./init-build.sh -DPLATFORM=odroidc2 -DAARCH64=1 A new guys couldn't get a support list of PLATFORM option, and know AARCH64 is only for ARMv8 SoC easily. - There are too much branches of platform or SoC Architectures. Such as: if(KernelArchARM) include_directories("include/arch/arm/armv/${KernelArmArmV}/") include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") endif() if(KernelArmMach STREQUAL "exynos") include_directories("include/plat/exynos_common/") endif() if(KernelArchRiscV) include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") endif() Linux Build System places the special build options and source files into the directory related with each architectures, and will generated a configure file (.config) during building. It's very good in my opinion. In Android Build System, a given project building inherits a common build options set, and update these parts only related the given project. It's very good for integration. And I want to know if there is a plan to update the build system or accept patches from volunteer? 2. I notice that, all kernel source files have been concatenated into a kernel_all.c, and compile the kernel_all.c. Is there some special reason for this step? It's a slight strange for me? Anyway, I am a new guy. I just want to understand it and if I could provide something to change it. Any comments are appreciated. Thanks, Jerry

1 0