Devel April 2018

devel@sel4.systems

13 participants
14 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

Questions on U-boot Verified Boot with CAmkES-ARM-VM
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to test secure boot with the CAmkES-arm-vm. I found that U-boot has its implementation of secure boot called verified boot, but it seems only support FIT image format. I’m wondering is there a way to convert the final ELF image to an FIT image? I’m studying the details of different booting image format. I’m not sure how it would work with seL4 camkes demo specifically, since there are so many binary files and cpio archives packed in the final ELF image. Would love to hear your opinions. Thank you very much! Best Regards -Daniel Wang

2 1

sel4 qemu x86 runtime error
by Thad Seeberger 10 Jul '18

10 Jul '18

Compile now no problem however I'm getting error when running. I believe its an invalid opcode exception. I think my build not matching the qemu but I've tried diff machines and they do the same. I also get this warning during build, not sure if this relevant: Warning: Installation path /home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool not found on the PATH environment variable. make: Leaving directory `/home/maddthad/camkes-tutorials-manifest/projects/capdl/capDL-tool' Qemu commanr, lines with ????? suspect: qemu-system-i386 -nographic -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 (process:98550): GLib-WARNING **: gmem.c:483: custom memory allocation vtable not supported Boot config: parsing cmdline 'images/kernel-ia32-pc99 ' Boot config: console_port = 0x3f8 Boot config: debug_port = 0x3f8 Boot config: disable_iommu = false ???? Warning: Your kernel was not compiled for the current microarchitecture. Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 1fefe000 type 1 Adding physical memory region 0x100000-0x1f800000 Physical Memory Region from 1fffe000 size 2000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 Multiboot gave us no video information Kernel loaded to: start=0x100000 end=0x160000 size=0x60000 entry=0x10005e ACPI: RSDP paddr=0xf7180 ACPI: RSDP vaddr=0xdfcf7180 ACPI: RSDT paddr=0x1ffffbc1 ACPI: RSDT vaddr=0xdffffbc1 ACPI: FADT paddr=0x1ffff1c0 ACPI: FADT vaddr=0xdffff1c0 ACPI: FADT flags=0x80a5 ACPI: 0 IOMMUs detected ACPI: MADT paddr=0x1ffffb11 ACPI: MADT vaddr=0xdffffb11 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd ACPI: 1 CPU(s) detected Detected 1 IOAPICs, but configured to use PIC instead Detected 1 boot module(s): module #0: start=0x161000 end=0x25aed0 size=0xf9ed0 name='images/capdl-loader-experimental-image-ia32-pc99' ELF-loading userland images from boot modules: size=0x189000 v_entry=0x804f544 v_start=0x8048000 v_end=0x81d1000 p_start=0x25b000 p_end=0x3e4000 Moving loaded userland images to final location: from=0x25b000 to=0x160000 size=0x189000 Starting node #0 with APIC ID 0 Booting all finished, dropped to user space Caught cap fault in send phase at address 0x0 while trying to handle: ?????? user exception 0x6 code 0x0 in thread 0xff3f5d00 "rootserver" at address 0x805130e With stack: 0x80cfda0: 0x0 0x80cfda4: 0x0 0x80cfda8: 0x0 0x80cfdac: 0x0 0x80cfdb0: 0x0 0x80cfdb4: 0x0 0x80cfdb8: 0x0 0x80cfdbc: 0x0 0x80cfdc0: 0x0 0x80cfdc4: 0x0 0x80cfdc8: 0x0 0x80cfdcc: 0x0 0x80cfdd0: 0x0 0x80cfdd4: 0x0 0x80cfdd8: 0x0 0x80cfddc: 0x0 QEMU: Terminated Have a great day.

2 1

ARM Vchan Error
by Daniel Wang 10 Jul '18

10 Jul '18

Hi all, I’m trying to make Vchan work on camkes-arm-vm in the process I encountered a couple problems. Hope you can give me some advice. I knew that Vchan is out dated and never finished on ARM. But it seems the only option for now (please correct me if I’m wrong). Here is what I did so far: 1. modified tk1_vmlinux.c by adding the virtual device and fault handler and installed it to guest linux with vm_add_device(vm, &vchan_dev); --------------------------------------------------- vchan_device_fault_handler(struct device* d UNUSED, vm_t* vm, fault_t* fault){ //uint32_t data = fault_get_data(fault); uint32_t data = fault_get_ctx(fault)->r1; vchan_entry_point(vm, data); // fflush(stdout); advance_fault(fault); return 0; } struct device vchan_dev = { .devid = DEV_CUSTOM, .name = "vchan-driver", .pstart = 0x2040000, .size = 0x1000, .handle_page_fault = &vchan_device_fault_handler, .priv = NULL, }; --------------------------------------------------- 2. compiled linux-tegra using buildroot (by the way the current linux-tegra is 4.9.0 which is not supported by buildroot-2016, the earliest version works for me is buildroot-2017-2), added a vmm-manager kernel driver similar to the one in camkes-x86-vm. But I changed the call_into_hypervisor() to the following: --------------------------------------------------- int call_into_hypervisor(int cmd, void *data, size_t sz, vmcall_args_t *vmcall) { int res = 0; int err; unsigned phys_ptr = virt_to_phys(vmcall); vmcall->data = data; vmcall->cmd = cmd; vmcall->phys_data = virt_to_phys(data); vmcall->size = sz; down(&hyp_sem); /* Set up arguments for the ARM hyp call */ asm volatile ("mov r0, %0; mov r1, %1" : : "r" (VMM_MANAGER_TOKEN), "r" (phys_ptr): "%r0", "%r1"); asm volatile (".arch_extension virt\n\t” "hvc #0"); asm volatile ("mov %0, r0" : "=r" (res) : : ); err = vargs->err; up(&hyp_sem); return err; } --------------------------------------------------- The kernel built and run correctly. But when I try to install the kernel driver. It crashed with following information. --------------------------------------------------- # modprobe driver.ko [81.826621] driver: loading out-of-tree module taints kernel Bad sys call from [Linux]: scone 0 at PC: 0xbf000214 Assertion failed” !err (/camkes-arm-vm/libs/libsel4arm-vmm/src/vm.c: vm_event: 407) ————————————————————————— I’m not sure if this error is triggered by the modified call_into_hypervisor() or by event_thread_run()->eventfd_signal(). Any help would be appreciated! Thanks in advance. Best Regards -Daniel Wang

2 1

IPC
by tj5527 04 Jul '18

04 Jul '18

Searching on the sel4 repository, I find there is a manual talking about IPC (https://github.com/seL4/seL4/blob/9dba8e67ccb54e207bbec22e25f21c65e5c6a45f/…) In addition to this material, where - particularly source code - would be a good start point to look into IPC design and implementation? Thanks

2 1

Booting seL4, MMU configuration on armv7a-ve
by Jonas Persson 30 Apr '18

30 Apr '18

Hello, I'm new to seL4 and I'm trying to get seL4 running on an Cortex-A7 with VE extensions (NXP IMX6UL). One of the experiments I wish to do is measure how fast I can get from POR to seL4 doing something meningful. To achive optimal boot speed I have a custom bootloader that does the bare minimum. The boot flow looks like this; 1. POR 2. Init HW 3. Load & verify blobs for trust zone and seL4 4. Jump to TEE init (OP-TEE) 5. Tee init code returns to bootloader with the CPU in HYP mode At this point we're back in the bootloader, there is no MMU, D cache or I cache active 6. Configure MMU 7. Jump to seL4 kernel entry I'm currently struggling with getting the MMU properly setup and I was hoping that someone here might shed some light on what I would need to do. I've looked at the elf-loader and from what I can understand it will setup a basic memory-mapping for the kernel only. Some of the questions that stand out in my head are : 1) How should the hand over work between the BL and seL4 with respect to setting up more mappings, for example IO memory. Should the PGD & PMD tables created by the bootloader be shared with the kernel? 2) What needs to be configured before calling the seL4 entry? Thanks, Jonas

1 0

Announcing seL4 9.0.1: with RISC-V support
by Kent.Mcleod＠data61.csiro.au 26 Apr '18

26 Apr '18

We are pleased to announce initial RISC-V support for the UC Berkeley Spike simulator platform. Instructions are available for building and running the seL4 test suite on RISC-V: <https://docs.sel4.systems/Hardware/RISCV> See an online copy of the release notes at: <https://docs.sel4.systems/sel4_release/seL4_9.0.1> <https://docs.sel4.systems/camkes_release/CAmkES_3.4.0> # seL4 Version 9.0.1 Release Announcing the release of `seL4 9.0.1` with the following changes: 9.0.1 2018-04-18: BINARY COMPATIBLE ## Changes * On 64-bit architectures, the `label` field of `seL4_MessageInfo` is now 52 bits wide. User-level programs which use any of the following functions may break, if the program relies on these functions to mask the `label` field to the previous width of 20 bits. - `seL4_MessageInfo_new` - `seL4_MessageInfo_get_label` - `seL4_MessageInfo_set_label` * Initial prototype RISC-V architecture port. This port currently only supports running in 64-bit mode without FPU or or multicore support on the Spike simulation platform. There is *no verification* for this platform. ## Upgrade Notes --- # Full changelog Refer to the git log in <https://github.com/seL4/seL4> using `git log 9.0.0..9.0.1` # More details See the [9.0.1 manual](http://sel4.systems/Info/Docs/seL4-manual-9.0.1.pdf) included in the release or ask on the mailing list!# CAmkES Version camkes-3.3.0 Release ---- # CAmkES Version camkes-3.4.0 Release Announcing the release of `` with the following changes: camkes-3.4.0 2018-04-18 Using seL4 version 9.0.1 ## Changes ## Upgrade Notes --- # Full changelog Use `git log camkes-3.3.0..camkes-3.4.0` in <https://github.com/seL4/camkes-tool> # More details See the [documentation](https://github.com/seL4/camkes-tool/blob/camkes-3.4.0/docs/i… or ask on the mailing list!

7 10

Further use of Device Tree?
by Jeff Waugh 23 Apr '18

23 Apr '18

Hello, Congrats on the RISC-V release! I noticed some Device Tree code snuck in, replacing some hard coded bits in the platform, and is intended to be exposed to the rootserver… Any interest or intention to bring that to the ARM code, and possibly avoid building kernels for specific platforms? Thanks, Jeff

2 1

UART1 getchar
by Wei Xiang Leow 19 Apr '18

19 Apr '18

Hello all, I'm new to seL4 and embedded systems, please bear with me. I'm trying to use Sabrelite's UART1 (PS_SERIAL0), while I can make it write data (putchar), I can't make it read (getchar). The code is as follows on sel4 7.0.0, using platsupport/sel4platsupport: ps_io_ops_t io_ops; error = sel4platsupport_new_io_ops(vspace, vka, &io_ops); printf("Initialising io_ops: %d\n",error); ps_chardevice_t serial0; ps_cdev_init(PS_SERIAL0,&io_ops,&serial0) ps_chardevice_t serial1; ps_cdev_init(PS_SERIAL1,&io_ops,&serial1); //CONSOLE int character; while (1) { character = ps_cdev_getchar(&serial0); //printf("%d\n",character); if (character != -1) { ps_cdev_putchar(&serial1,character); printf("%d\n",character); } } This runs fine on QEMU with -serial file/ttyUSB -serial mon:stdio. Next I tried to run this on the Sabrelite board: -Clone the 08-09 uboot from git, according to https://sel4.systems/Info/ Hardware/sabreLite/ -Apply patches 1 and 2 (applying 3 and 4 caused uboot to stall) -Put uboot into SPI flash -Restart, run the sel4 image on the SD card, with UART2 connected to PC's RS232 and displayed by minicom, and UART1 connected to /dev/ttyUSB0 -Have a python script writing 'A's to /dev/ttyUSB0 sel4 loads but fails to read anything from /dev/ttyUSB0, UART1 just receives EOFs (-1s). The rxd seems to always be 0. Swapping the UARTs works, at the cost of losing the console: while (1) { character = ps_cdev_getchar(&serial1); //printf("%d\n",character); if (character != -1) { ps_cdev_putchar(&serial0,character); printf("%d\n",character); } } So UART2 (default console) can read and write, while UART1 can write but not read. Has anyone encountered the same problem? Suggestions much appreciated. Regards, Leow Wei Xiang

1 0

Camkes manifest now requires cmake 3.7.2 or higher to be built
by Amit Goyal 13 Apr '18

13 Apr '18

I was running the following commands to build camkes: 1. repo init -u https://github.ls com/sel4/camkes-manifest.git 2. repo sync 3. make clean 4. make ia32_simple_defconfig; make silentoldconfig 5. make -j4 6. qemu-system-i386 -nographic -m 512 -cpu Haswell -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 Earlier it used to work perfectly fine but now it requires cmake 3.7.2 or higher which can be obviously be done by using pip install. I just wanted to convey this so that the same may be updated on prerequisites page. (https://github.com/SEL4PROJ/sel4-tutorials/blob/master/Prerequisites.md) -- Thanks and Regards, Amit Goyal

1 0

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel April 2018