- 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 «… [View More]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. [View Less]

1 0

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

11 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 … [View More]

2 1

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

09 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 … [View More]

1 0

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 … [View More]

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 … [View More]

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 … [View More]

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,… [View More]

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 … [View More]

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