Devel February 2021

devel@sel4.systems

6 participants
11 discussions

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

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

Ethernet device module for odroidc2
by ogosinkem＠gmail.com 24 Feb '21

24 Feb '21

I have been trying to use the ethernet driver for the UNSW Asdvanced Operating Systems course but I still get these messages: find_compatible_driver_module@io.c:434 No suitable driver was found for path /soc/ethernet@c9410000, ignoring server_init@ethdriver.c:382 Unable to find an ethernet device I thought that I had to copy the driver to the utils lib folder and provide a preprocessor macro as someone else had suggested but I may be missing a few other things. Best, Nkem

3 6

Sporadic Server Implementation Details
by msudvarg＠wustl.edu 11 Feb '21

11 Feb '21

Hi all, I hope this is the right forum to be posting this question. I've reached out to Anna Lyons, the first author on the EuroSys 2018 "Scheduling Context Capabilities" paper (https://ts.data61.csiro.au/publications/csiro_full_text//Lyons_MAH_18.pdf), but I do not know if her listed email address is still active. I want to ask for more clarification on the sporadic server implementation in seL4. My interpretation of how the Lyons et al. paper describes the implementation is different than my understanding of the sporadic server definition as described by Sprunt et al. in 1989 (https://link.springer.com/article/10.1007/BF02341920). However, looking at the seL4 kernel source code, it seems that the actual implementation follows very closely with the improved POSIX sporadic server mechanism described by Stanovic et al. in 2010 (https://www.cs.fsu.edu/~awang/papers/rtas2010.pdf). In particular, the Lyons et al. paper states that when a thread is preempted at time t, a replenishment is scheduled for time t + T. My understanding of the sporadic server is that if a thread becomes active at time t, the replenishment is scheduled for time t + T. In other words, the replenishment is scheduled one period from when the thread begins execution, not when it ends execution. Further, a thread becomes active when it becomes unblocked (i.e. returns from a blocking system call, or is activated by the release of an aperiodic task that it handles). In other words, a thread that is preempted by a higher-priority thread is not considered to have become inactive, according to the sporadic server definition. This seems to be the case in both the Sprunt and Stanovic papers. I think the distinction is significant in a system (like seL4) where only a finite number of replenishments are tracked. Determining what number of replenishments each thread’s server must track is much easier if only voluntary yielding of the processor, and not preemption by higher-priority threads, triggers a replenishment. Can somebody explain to me in more detail how the sporadic server has been implemented in seL4? Like I said, from my reading of the kernel source, it seems that it has been implemented according to the improved POSIX sporadic server detailed by Stanovic, but I’m not certain that I’ve identified all conditions that cause a replenishment to be scheduled.

3 2

Use sel4 and mmc for storage but sdhc driver wait for SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB
by MOHAMAD REZA SHAFIEI 10 Feb '21

10 Feb '21

hi there ... i'm working on mmc in sel4 for storage memory. i port your code for i.mx7 (modify registers and all need for that). so when i init mmc with calling mmc_init, sdhc driver wait at sdhc.c@249 and in this line: while (readl(host->base + PRES_STATE) & (SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB)); indeed sdhc driver send function (sdhc_next_cmd(..)) send first command in mmc_reset (): which is : struct mmc_cmd cmd = {.data = NULL}; cmd.index = MMC_GO_IDLE_STATE; cmd.arg = 0; cmd.rsp_type = MMC_RSP_TYPE_NONE; printf("2-1\n"); host_send_command(card, &cmd, NULL, NULL); and status= 65 returned whicm means this command sent completely. so when program continue to send another command (still in mmc_reset) which is : /* TODO: review this command. */ struct mmc_cmd cmd2 = {.data = NULL}; ps_mdelay(10); cmd2.index = MMC_SEND_EXT_CSD; cmd2.arg = 0x1AA; cmd2.rsp_type = MMC_RSP_TYPE_R1; printf("2-2\n"); host_send_command(card, &cmd2, NULL, NULL); status which returned with sdhc send command in sdhc driver is 0. but this worked too. and when program execution continue to call mmc_voltage_validation(..) sdhc driver wait in while (readl(host->base + PRES_STATE) & (SDHC_PRES_STATE_CIHB | SDHC_PRES_STATE_CDIHB)); ... I don't have any idea why this happened .. can you help me? I didn't modify any code in sdhc.c or mmc.c ... my app for using mmc is here: #include <autoconf.h> #include <camkes.h> #include <camkes/io.h> #include <camkes/sync.h> #include <stdio.h> #include <utils/util.h> #include "string.h" //sdio test #include <sdhc/mmc.h> #include <sdhc/plat/sdio.h> #include <sdhc/sdio.h> #define max(x, y) (((x) >= (y)) ? (x) : (y)) //build config // #define TEST_FILESYSTEM 0 #ifdef CONFIG_64BIT #define BITS_PER_LONG 64 #else #define BITS_PER_LONG 32 #endif /* CONFIG_64BIT */ #define IMX7_GPIO1_BASE_ADDR ((uint32_t)NULL) #define IMX7_GPIO4_BASE_ADDR ((uint32_t)NULL) #define IMX7_SPI_BASE_ADDR ((uint32_t)NULL) #define IMX7_CTL_MUX_BASE_ADDR ((uint32_t)NULL) /** * we have two keyboard driver () */ bool STDKBD = true; #define IMX7_CTL_MUX_GPIO1_09 (0x18) seL4_CPtr timer_notification(void); seL4_CPtr notification; static void delay(uint64_t ms) { seL4_Word badge; /* test a relative timeout */ uint64_t t1 = timer_time(); // printf("Cur time: %"PRIu64"\n", t1); timer_oneshot_relative(0, ms * NS_IN_MS); seL4_Wait(notification, &badge); // printf("Badge: %x\n", badge); t1 = timer_time(); // printf("Cur time: %"PRIu64"\n", t1); } /* * Required for the camkes_sys_clock_gettime() in sys_clock.c of libsel4camkes. */ int clk_get_time(void) { uint64_t time_in_ms = timer_time() / NS_IN_MS; return (time_in_ms & 0xFFFFFFFF); } 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){ // printf("mmc not found yet :)\n"); // mmc_init handle this self // sdio_host_dev.handle_irq(&sdio_host_dev,irq->irq.number); mmc_irq_acknowledge(irq); return ; } // sdio_host.handle_irq(&sdio_host, irq); mmc_handle_irq(mmc_card,irq->irq.number); mmc_irq_acknowledge(irq); } 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"); // sdhc_ls(); } else { printf("SDHC1 initizatino failed!: %d", err); } // sdio_host_dev.reset(&sdio_host_dev); // mmc_init(&sdio_host_dev, &io_ops, mmc_card); // sdio_host_dev.handle_irq =mmc_handle_irq_func; while (true) { printf(".\n"); delay(1000); } return 0; } best regards.. shafie -- This email was Anti Virus checked by Security Gateway.

1 0

Public seL4 TSC meeting on Fri, 12 Feb
by Gerwin Klein 08 Feb '21

08 Feb '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: Fri 12 Feb 2021 15:30-17:00 Sydney time (5:30am in Berlin, 8:30pm in San Francisco). This is the continuation of the meeting last week. The meeting is by Zoom, and you can register here: https://unsw.zoom.us/meeting/register/tZcqf--prz8jGNdE-zpwZXIBsbdYlN3fQn1Y Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. The agenda for the meeting so far is: Discussion points - when/how should Committer/Admin role change for people who have left D61 and had the role based on org membership - endorsement process for training and products Vote on: - Platform Owner proposal Discuss, potentially vote on RFC proposals: - https://sel4.atlassian.net/browse/RFC-6 - https://sel4.atlassian.net/browse/RFC-5 - https://sel4.atlassian.net/browse/RFC-4 If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.htmld

1 0

Public TSC meeting on Fri, 29 Jan
by Gerwin Klein 08 Feb '21

08 Feb '21

The Technical Steering Committee (TSC) of the seL4 Foundation will hold its next public meting on: Fri 29 Jan 2021 15:30-17:00 Sydney time (5:30am in Berlin, 8:30pm in San Francisco). The meeting is by Zoom, and you can register here: https://unsw.zoom.us/meeting/register/tZ0ocO6hrDwiGtTYlzULbKeTK8ybYJyCC7_p Anyone interested can join the meeting and listen to the discussion and request to speak, which will be granted if time permits. Only TSC members can vote. The seL4 code of conduct applies to the meeting [1]. Sorry about the very early time for Europe, but there are no time slots that work for the US, Australia, and Europe at the same time. We are planning to swap between better times for Europe and the US for the next meetings. The TSC is the body that decides on the technical direction of seL4: https://sel4.systems/Foundation/TSC/ The agenda for the meeting so far is: - updates from the TSC chair and committees: - seL4 public Jira - Jira + GitHub sync - reviewers who have joined - more GitHub tests - discussion points: - do we have too many different forums? - bug/issue classification (Jira is now public, we shouldn't call everything a bug) - more in-tree docs - test infrastructure - extend RFC process slightly? (see https://sel4.atlassian.net/browse/RFC-6?focusedCommentId=14886& ) - when/how should Committer/Admin role change for people who have left D61 and had the role based on org membership - endorsement process for training and products - vote on: - Platform Owner proposal - discuss, potentially vote on RFC proposals: - https://sel4.atlassian.net/browse/RFC-4 - https://sel4.atlassian.net/browse/RFC-5 - https://sel4.atlassian.net/browse/RFC-6 This is probably already too much for 90min and we may have to prioritise, but we will see how far we get. If there are other items that I missed or you think should be on the agenda, please let me know. If we can't get to an item this time, we can still schedule another meeting. Cheers, Gerwin (TSC chair) [1]: https://docs.sel4.systems/processes/conduct.html

2 5

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel February 2021