Devel March 2017

devel@sel4.systems

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

Creating process from not root process
by rad021993＠yandex.ru 02 Apr '17

02 Apr '17

Hi all, I try to create process (process2) from not root process (process1). Process1 has own cspace and vspace (fields 'create_cspace' and 'create_vspace' are set to true in process1' config). I try to create process2 like in the root process (4-th example in sel4 tutorials), but I can't obtain bootinfo to create allocman. As I understood it, this info available only from root process. Also I found function to create allocman via bootstrap function (like in example_bootstrap.c), but I also need to get process1' vspace and cspace to attach them to allocman. I do not understand, how I can get the needed info. Could you tell me how I can do it? Best regards, Rinat Dobrokhotov

2 1

Confusion with various memory address
by Daniel (Xiaolong) Wang 01 Apr '17

01 Apr '17

Hi all, I have a probably a dumb question that need some clarification. I was reading the kernel source code and I’m little bit confused with the three data type: paddr_t, pptr_t, vptr_t and the following three data struct related to them. typedef struct region { pptr_t start; pptr_t end; } region_t; typedef struct p_region { paddr_t start; paddr_t end; } p_region_t; typedef struct v_region { vptr_t start; vptr_t end; } v_region_t; Based on how those are being used I assume the paddr_t and p_region are data struct for physical address, vptr_t and v_region are for virtual address. According to the following functions seem that the translation between physical address to pptr_r is by adding/subtracting a offset. But I’m confused with the pptr_t and region I wonder what are those for? Tank you very much! static inline void* CONST ptrFromPAddr(paddr_t paddr) { return (void*)(paddr + physMappingOffset); } static inline paddr_t CONST addrFromPPtr(void* pptr) { return (paddr_t)pptr - physMappingOffset; } static inline region_t CONST paddr_to_pptr_reg(p_region_t p_reg) { return (region_t) { p_reg.start + physMappingOffset, p_reg.end + physMappingOffset }; } static inline p_region_t CONST pptr_to_paddr_reg(region_t reg) { return (p_region_t) { reg.start - physMappingOffset, reg.end - physMappingOffset }; } Thanks -Dan

2 1

Announcing seL4 5.0.0
by Kent.Mcleod＠data61.csiro.au 31 Mar '17

31 Mar '17

We are pleased to announce the release of 5.0.0 of seL4. Listed below are a few of the key changes in this release: Below are the changes to the seL4 ABI and API: Generic changes: * Add missing case to seL4_getFault (seL4_Fault_DebugException) * Explicitly pack bootinfo data structures * Modify FinalizeLog syscall - Now returns a number of entries in the log * Extend bootinfo to support potentially arbitrary additional structures * Deprecate bootinfo management in libsel4 - a replacement, platsupport_get_bootinfo can be found in libsel4platsupport x86 specific changes: * Pass VBE information from multiboot through bootinfo * Remove PAE support x86-64 specific changes: * VT-x related cap and object definitions added * seL4_VMEnter syscall added arm specific changes: * ARM-HYP: VCPU interface for manipulating banked registers added * plat: added nvidia tx1 support * ARM-HYP: Add support for save/restore of debug registers * Add aarch64 implementation = Upgrade notes = * This release breaks both API and ABI and is not source compatible with the earlier versions. = Full changelog = Use {{{git log 4.0.0..5.0.0}}} in https://github.com/seL4/seL4 = More details = See the 5.0.0 manual (http://sel4.systems/Info/Docs/seL4-manual-5.0.0.pdf) included in the release for detailed descriptions of the new features. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/5.0.0.tar.gz [9e143c75c68edcaefc5506caea341890 5.0.0.tar.gz] Contributors: Adrian Danis Hesham Almatary Amirreza Zarrabi Kent McLeod Jack Suann Kofi Doku Atuah Amirreza Zarrabi Donny Yang Anna Lyons Stephen Sherratt Partha Susarla Thomas Sewell Frank Li Jeff Waugh Berkus Decker Corey Richardson Kent Mcleod Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Kent McLeod Kernel engineer DATA61 | CSIRO E kent.mcleod at data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

errors when make camkes-tutorials-manifest
by talos 31 Mar '17

31 Mar '17

Hi, When I made this tutorials, there was an error; You are not the owner of '/home/talos/.stack/'. Aborting to protect file permissions. Retry with '--allow-different-user' to disable this precaution How can I do this, thanks!

2 1

Allocation manager and processes
by Rinat Dobrokhotov 28 Mar '17

28 Mar '17

Hi all, 1. Could you check if my thoughts are right? The allocation manager is global object and there is only one instance for whole system. If I need in creation kernel objects I should create _one_ allocman above some array of memory. 2. I have the first question because I work with processes now. In the root process I create two different processes based on the elf image via allocman. Then I try to manage (suspend, change priority, etc.) process1 by process2. But I can't get process1 object from process2 because both of them belong to root process and belong to root process' memory space. As I understand it, I should copy cap which belongs to process1 to process2, then I will be able to manage them. Could you tell me if I am right? -- Best regards, Rinat Dobrokhotov

2 1

CapDL & RT
by Richard Habeeb 23 Mar '17

23 Mar '17

Hello all, I see that the master branch of CapDL has some support for the RT kernel, but I am having some trouble building it against the current public sel4 RT branch. Which version of the RT kernel does capDL work with? Or, is it still a work in progress? Thanks, Richard -- Richard Habeeb Research Assistant, Computer Science, USF PGP: https://goo.gl/VhmGGu https://habeebr.bitbucket.io/

2 1

sel4 kernel boot problem on i.mx6q board
by shijun zhao 21 Mar '17

21 Mar '17

Hi everyone, I am running sel4 on i.mx6q sabre board. I use the sabre_debug_xml_defconfig config file. However, the image stops at "Jumping to kernel-image entry point..." when I run it on the board. Following is the printed messages: ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..2030081f] ELF-loading image 'kernel' paddr=[80000000..80032fff] vaddr=[e0000000..e0032fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[80033000..80406fff] vaddr=[10000..3e3fff] virt_entry=203d0 Enabling MMU and paging Jumping to kernel-image entry point... There are some warnings during compilation, all of which are caused by arm-none-eabi/bin/ld. And I see that the sel4 wiki shows how to solve the warnings: *To fix, do make menuconfig visit seL4 Libraries→Build musl C Library and untick libmuslc use precompiled archive then do make clean and attempt to rebuild.* However, there is no *Build musl C library* in my menuconfig, and there are only *libmuslc *and *libsel4muslcsys *options in the seL4 libraries. Can anyone tell me how to solve this problem? Thanks! Best Regards, Shijun

2 4

Help accessing physical address on zynq7000
by Brandon, Jeffrey - 0553 - MITLL 21 Mar '17

21 Mar '17

Hello, I've been getting started with seL4 on the zynq7000 and I am looking for resources on how to read/write physical memory for memory mapped io purposes. If there is a relevant tutorial or manual to reference I haven't come across it yet so I wanted to ask here. Any other guidance as to how to think about and work with capabilities would be useful at this stage. I'm working with a modified version of the sel4test repository. Looking at that I found env.simple (simple_t defined https://github.com/seL4/seL4_libs/blob/a1c031b0885dec4ddf1ee1f8866bcd23dcca6 ac3/libsel4simple/include/simple/simple.h) which seems to contain function pointers for some relevant functions to what I'm trying to do, but I am not entirely sure how to go about using them. What needs to be initialized first and how do I go about that? Any guidance greatly appreciated, Thanks. Jeff Brandon Associate Staff MIT Lincoln Laboratory 05-53 Secure Resilient Systems and Technology Ph: 781.981.9233

2 1

TK1 VMM SMMU Translation Error
by Enrique Leon 15 Mar '17

15 Mar '17

Hello All, We have recently run into an issue trying to boot the TK1 VMM on a TK1 Jetson board. The kernel tries to run but soon runs into translation errors after a couple of seconds. We are using the non-secure dtb with the initrd image. Here are some of the lines, it continues on like this and never stops. SMMU Address translation error: ID: 1 address: 0x0 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 SMMU Address translation error: ID: 1 address: 0x18fc00 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x SMMU Address translation error: ID: 1 address: 0x912c0 type: 6 direction: 0x0 We had success running the VM using the previous commit from camkes-arm-vmm repo, but the newest commit has introduced this issue. We have isolated it to line 93 in the "vmm_common.camkes" file. Removing "0x54200000:18", // Display A" from the file fixes the problem and we can boot as normal. We are also running Uboot 2010-10-rc5 as suggested by a email on the board. I am still new to working down to this level of code so any help in understanding this problem is appreciated.

3 3

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel March 2017