- Devel - lists.sel4.systems

how to debug libsel4allocman
by Vasily A. Sartakov 14 Apr '17

14 Apr '17

Greetings I am using a 4.0 compatible seL4 snapshot derived from mainline several months ago as a base for seL4/MIPS port. Currently, I am debugging sel4tests. My goal — make everything working before moving to hardware. By «everything» I mean different configurations of the system (optimization flags, syscall attributes, fast/slow path, etc). For example, most stable build uses «CONFIG_LIB_SEL4_INLINE_INVOCATIONS», less stable build, which I am debugging now, uses «CONFIG_LIB_SEL4_PUBLIC_SYMBOLS». This configuration crashes at the start when I am trying to allocate memory for the first test: Starting test suite sel4test Starting test 0: TEST_TRIVIAL0001 TEST_TRIVIAL0001 b24e68 b0cc4c b0cc2c b0cc2c sel4test-tests 0 0 * Loading segment 00400000-->005748a4 * Loading segment 00575000-->00689d84 alloc->num_cspace_slots = 30 alloc->num_cspace_slots = 29 alloc->num_cspace_slots = 28 alloc->num_cspace_slots = 27 alloc->num_cspace_slots = 26 alloc->num_cspace_slots = 25 alloc->num_cspace_slots = 24 alloc->num_cspace_slots = 23 alloc->num_cspace_slots = 22 alloc->num_cspace_slots = 21 alloc->num_cspace_slots = 20 alloc->num_cspace_slots = 19 alloc->num_cspace_slots = 18 alloc->num_cspace_slots = 17 alloc->num_cspace_slots = 16 alloc->num_cspace_slots = 15 alloc->num_cspace_slots = 14 alloc->num_cspace_slots = 13 alloc->num_cspace_slots = 12 alloc->num_cspace_slots = 11 alloc->num_cspace_slots = 10 alloc->num_cspace_slots = 9 alloc->num_cspace_slots = 8 alloc->num_cspace_slots = 7 alloc->num_cspace_slots = 6 alloc->num_cspace_slots = 5 alloc->num_cspace_slots = 4 alloc->num_cspace_slots = 3 alloc->num_cspace_slots = 2 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark alloc->num_cspace_slots == 0_refill_watermark:374 slota = 0 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark alloc->num_cspace_slots == 0_refill_watermark:374 slota = 0 alloc->num_cspace_slots = 1 _allocman_cspace_alloc@allocman.c:254 Regular cspace alloc failed, and failed from watermark I see, that: 243: error = alloc->cspace.alloc(alloc, alloc->cspace.cspace, slot); returns the error, and then we allocating memory from the watermark. In other builds (for example, with CONFIG_LIB_SEL4_INLINE_INVOCATIONS attributes), I do not see this issue - there are no errors on return. So, I need to debug function to be sure that I am receiving in the kernel proper arguments and so one, but I do not understand how this part of the code works. Do you have any documentation, or slides or just simple diagrams how this allocator work? What functions are responsible for generating error return, where exactly allocation is performed and how to debug this. Thank you.

1 0

Questions about userspace memory allocation
by Daniel (Xiaolong) Wang 10 Apr '17

10 Apr '17

Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the kernel create both idlethread and init thread and, but it only create a TCB object. 1). I wonder when the init thread's frame and PD are created, and how the thread's stack and heap is allocated? 2). I wonder is there a limit or default value for how much physical memory init thread uses at booting time? Thanks -Dan

2 1

Questions about Userspace memory allocation
by Daniel Wang 08 Apr '17

08 Apr '17

Hi all, I have a couple questions hope someone can help me clear it out. I understand that after booting up, the kernel keep tracking of all physical memory as Untyped and hand it over to the init thread. It seems like the kernel create both idlethread and init thread and, but it only create a TCB object. 1). I wonder when the init thread's frame and PD are created, and how the thread's stack and heap is allocated? 2). I wonder is there a limit or default value for how much physical memory init thread uses at booting time? Thanks -Dan

1 0

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

01 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

Re: [seL4] Devel Digest, Vol 35, Issue 1
by talos 01 Apr '17

01 Apr '17

Re: 1. Re: errors when make camkes-tutorials-manifest the output of ls -al for my .stack directory: drwxrwxr-x 4 talos talos 4096 3月 29 17:19 .stack my username is talos Thanks ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Sat, Apr 1, 2017 06:29 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 35, Issue 1 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: errors when make camkes-tutorials-manifest (Stephen.Sherratt(a)data61.csiro.au) 2. Announcing seL4 5.0.0 (Kent.Mcleod(a)data61.csiro.au) 3. Creating process from not root process (rad021993(a)yandex.ru) 4. Confusion with various memory address (Daniel (Xiaolong) Wang) ---------------------------------------------------------------------- Message: 1 Date: Fri, 31 Mar 2017 03:46:28 +0000 From: <Stephen.Sherratt(a)data61.csiro.au> To: <devel(a)sel4.systems> Subject: Re: [seL4] errors when make camkes-tutorials-manifest Message-ID: <1490931983542.96806(a)data61.csiro.au> Content-Type: text/plain; charset="iso-8859-1" Hi Talos, Are you the owner of /home/talos/.stack ? For comparison, the output of ls -al for my .stack directory: drwxr-xr-x 10 ssteve ssteve 4096 Jan 24 15:25 .stack My username is ssteve. You could also try renaming your .stack directory so stack can create a new one for you. Cheers, Stephen ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of talos <2486580938(a)qq.com> Sent: Thursday, 30 March 2017 9:28 PM To: devel Subject: [seL4] errors when make camkes-tutorials-manifest 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! -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20170331/b3b2c08e/attachmen…>

1 0

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 27 Mar '17

27 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 22 Mar '17

22 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