- Devel - lists.sel4.systems

Re: [seL4] Memory protections within userspace and hardware/driver support
by Devin Harper 03 May '17

03 May '17

Hi, I read the whole FAQ. Does the "bug-free" protections for privacy apply to within each app of the same Linux virtual machine (overcoming memory bugs built in apps), between apps of the same Linux virtual machine (overcoming memory bugs built in the Linux kernel/GNU distro), or merely between different virtual machines (allowing any Linux kernel/GNU distro to be compromised, just not allowing them to compromise each other)? Furthermore, do I understand correctly that sel4 will only work on a few pieces of computer hardware, or will it work on everything the Linux kernel supports (has drivers for)? If sel4 will work on everything the Linux kernel supports (has drivers for), then do the same bug-free promises hold true on those hardwares in addition to the hardwares sel4 has already been tested on? Thanks!

2 1

Can I running camkes-arm-vm on HiKey board
by li94575 02 May '17

02 May '17

Hi all, Now, only exynos5 and tk1 are supported for running virtualised Linux on seL4. If I want to port it to HiKey board, is this possible?

3 2

questions about TK1 VM
by PX 01 May '17

01 May '17

Hi, all I have some questions about TK1 VM. I want to save the execution status of the TK1 VM. First, I stop the VM, then I use the function, seL4_TCB_ReadRegisters() to read the VM's registers into a buffer. Here are my questions: 1. Before I call the function, seL4_TCB_ReadRegisters(), do I need to flush TLB of CPU? If so, where is the library I need to check for this function? 2. The register values in the structure, seL4_UserContext, are VMM's physical addresses or virtual addresses? Best wishes Peng

2 1

sel4test failing TEST_SCHED0004 on iMX6
by Robert Kaiser 19 Apr '17

19 Apr '17

Hi all, I just tried to run the test suite on iMX6. Using the current version from github, I got this result: ---------------------------- ..... Test suite failed. 200/202 tests passed. 200/202 tests passed. *** FAILURES DETECTED *** ---------------------------- Further checking into the log shows this: ---------------------------- ..... Starting test 51: TEST_SCHED0004 TEST_SCHED0004 Running test SCHED0004 (Test threads at all priorities) _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark vka_alloc_object_at_maybe_dev@object.h:46 Failed to allocate cslot: error 1 new_pages_at_vaddr@vspace.c:331 Failed to allocate page sel4utils_configure_thread_config@thread.c:77 ipc buffer allocation failed Assertion failed: error == 0 ([.....]/seL4test/apps/sel4test-tests/src/helpers.c: create_helper_thread: 346) Failure: result == SUCCESS at line 343 of file [.....]/seL4test/apps/sel4test-driver/src/main.c Failure: Test check failure (see log). at line 0 of file ..... ---------------------------- The same test is run a second time further down below the log, giving the same result. I tested this on two different IMX6 platforms (SabreLite and Wandboard). Both showed identical results. Is this a known problem? Cheers Robert -- Robert Kaiser Technische Informatik Hochschule RheinMain Wiesbaden Rüsselsheim Computer Engineering RheinMain University of Applied Sciences robert.kaiser(a)hs-rm.de http://www.cs.hs-rm.de/~kaiser tel:(+49)611-9495-1292 fax:(+49)611-9495-1210 Postanschrift/Postal Address: Robert Kaiser, Hochschule RheinMain, FB DCSM/Informatik Unter den Eichen 5, 65195 Wiesbaden, Germany

2 2

smaccm/sel4arm-vmm-manifest complie problem
by 高文博 19 Apr '17

19 Apr '17

hi everyone! i am doing research about sel4.i used https://github.com/smaccm/sel4arm-vmm-manifest code. and complie it.than it build out kernel.elf only. but where is linux? expecting your answers. thanks very much! gao. -- 高文博数据通信科学技术研究所

2 1

smaccm/sel4arm-vmm-manifest compile problem
by 高文博 15 Apr '17

15 Apr '17

hi everyone! i am doing research about sel4.i used https://github.com/smaccm/sel4arm-vmm-manifest code. and compile it.than it build out kernel.elf only. but where is linux? expecting your answers. thanks very much! gao.

1 0

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 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 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 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