September 2018 - Devel - lists.sel4.systems

create a new thread in sel4
by Dongxu Ji 25 Sep '18

25 Sep '18

Hello, My platform is imx6q sabrelite and I have run sel4-test successfully. Now I'm trying to create a new thread in the initial thread according to sel4 tutorial2. But it didn't run. The code is shown below: struct driver_env env; allocman_t *allocman; /* function to run in the new thread */ void thread_2(void) { printf("thread_2: hallo wereld\n"); while (1); } int main(void) { int error; reservation_t virtual_reservation; seL4_BootInfo *info = platsupport_get_bootinfo(); seL4_DebugNameThread(seL4_CapInitThreadTCB, "sel4test-driver"); /* initialise libsel4simple */ simple_default_init_bootinfo(&env.simple, info); /* create an allocator */ allocman = bootstrap_use_current_simple(&env.simple, ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); /* create a vka */ allocman_make_vka(&env.vka, allocman); /* create a vspace */ error = sel4utils_bootstrap_vspace_with_bootinfo_leaky(&env.vspace, &data, simple_get_pd(&env.simple), &env.vka, platsupport_get_bootinfo()); /* fill the allocator with virtual memory */ void *vaddr; virtual_reservation = vspace_reserve_range(&env.vspace, ALLOCATOR_VIRTUAL_POOL_SIZE, seL4_AllRights, 1, &vaddr); if (virtual_reservation.res == 0) { ZF_LOGF("Failed to provide virtual memory for allocator"); } bootstrap_configure_virtual_pool(allocman, vaddr, ALLOCATOR_VIRTUAL_POOL_SIZE, simple_get_pd(&env.simple)); /* Allocate slots for, and obtain the caps for, the hardware we will be * using, in the same function. */ sel4platsupport_init_default_serial_caps(&env.vka, &env.vspace, &env.simple, &env.serial_objects); vka_t serial_vka = env.vka; serial_vka.utspace_alloc_at = arch_get_serial_utspace_alloc_at(&env); /* Construct a simple wrapper for returning the I/O ports. */ simple_t serial_simple = env.simple; /* enable serial driver */ platsupport_serial_setup_simple(&env.vspace, &serial_simple, &serial_vka); simple_print(&env.simple); /* get our cspace root cnode */ seL4_CPtr cspace_cap; cspace_cap = simple_get_cnode(&env.simple); /* get our vspace root page diretory */ seL4_CPtr pd_cap; pd_cap = simple_get_pd(&env.simple); /* create a new TCB */ vka_object_t tcb_object = {0}; error = vka_alloc_tcb(&env.vka, &tcb_object); /* initialise the new TCB */ error = seL4_TCB_Configure(tcb_object.cptr, seL4_CapNull, cspace_cap, seL4_NilData, pd_cap, seL4_NilData, 0, 0); /* give the new thread a name */ name_thread(tcb_object.cptr, "hello-2: thread_2"); UNUSED seL4_UserContext regs = {0}; /* set instruction pointer where the thread shoud start running */ sel4utils_set_instruction_pointer(&regs, (seL4_Word)thread_2); error=sel4utils_get_instruction_pointer(regs); /* check that stack is aligned correctly */ const int stack_alignment_requirement = sizeof(seL4_Word) * 2; uintptr_t thread_2_stack_top = (uintptr_t)thread_2_stack + sizeof(thread_2_stack); /* set stack pointer for the new thread */ sel4utils_set_stack_pointer(&regs, thread_2_stack_top); error=sel4utils_get_sp(regs); /* actually write the TCB registers. */ error = seL4_TCB_WriteRegisters(tcb_object.cptr, 0, 0, 2, &regs); /* start the new thread running */ error = seL4_TCB_Resume(tcb_object.cptr); /* we are done, say hello */ printf("main: hello world \n"); return 0; } And I can get some output: cspace_cap is 2 pd_cap is 3 tcb_object.cptr is 5f7 tcb_object.ut is 10000208 tcb_object.type is 1 tcb_object.size_bits is a regs.pc is 9640 regs.sp is 3f24f0 Any advice about the issue? Thank you, Dongxu Ji

2 2

seL4 and rump kernel synchronization primitives limitations
by Jason Wenger 20 Sep '18

20 Sep '18

I think I've uncovered an interesting problem involving IPC between rump kernels and seL4, and I'm curious if anyone has any thoughts on mitigating it. My use case is that I want a CAmkES component to be able to notify the rump component to send a network packet. However, as far as I can see: CAmkES connector, mutex, and semaphore threads that run in a rump component • can wait on their seL4 synchronization primitives • ... but they can't call rump function calls because they're not rump threads. You can try to call, becuase you're running in the same address space as the rump kernel, but if you call a rumpkernel function, the CAmkES thread crashes when it reaches curlwp() becuase the calling thread is unknown to the NetBSD kernel. Therefore you can't call sendto() inside, for example, a notification callback or an seL4RPCCall handler, unless you can work out a way to signal to the NetBSD kernel that you're calling into the kernel from a foreign thread. Is this somehow possible through use of rump_schedule() and rump_unschedule()? ... and the other possible path I can see also has problems: rumpkernel created userspace threads (pthreads) • can wait on seL4 synchronization primitives • ... but if they do wait, they also unschedule the* entire rest of the rump kernel and userspace* because every single rump thread (both kernel and user) all run in one seL4 thread. Therefore you can't do while(true) { semaphore_wait(); sendto(...); } without unscheduling the entire rump component when you hit the wait(). For this to work, there would need to be a way to have multiple seL4 threads for rump kernel execution so that one could block while the others continue. That *is* done for interrupt and timer handling, but there's no way I can see to set it up from a rump userspace program. The only other possible path appears to be busy-wait polling which is obviously very inefficient. Any thoughts? --Jason C. Wenger

2 1

genode-sel4-arm -- Genode OS with seL4 on ARM hardware
by Adam Wiethuechter 19 Sep '18

19 Sep '18

Webite -- http://genodl4arm.critical.com/ Github -- https://github.com/CriticalTechnologiesInc/genode-sel4-arm Hello everyone, I have something rather exciting to share with you all today that we here at Critical Technologies Inc (CTI) have been working on for sometime now - the marriage of Genode OS and seL4 on native ARM hardware. We currently are supporting the Wandboard Quad (from Wandboard) and the SabreLite (from Boundary Devices). We are hoping to continue development targeting ARMv8a boards of interest; mainly the Raspberry Pi 3B and/or the Xilinx Zynq UltraScale+ ZCU102. This is obviously a work in progress with only the first step but we wished to share our documentation to the community for others to contribute and see what we are doing. I am happy to answer any questions you may have. -- 73's, Adam Wiethuechter, Jr Software Engineer Critical Technologies Inc. <adam.wiethuechter(a)critical.com>

2 1

Building/Running https://github.com/SEL4PROJ/docs with docker
by Axel Heider 18 Sep '18

18 Sep '18

Hi, I'm trying to build and run https://github.com/SEL4PROJ/docs with docker. Following the instrucitons: git clone https://github.com/SEL4PROJ/docs cd docs git submodule init git submodule update docker run --network=host -v $PWD:/host -w /host -it ruby bash -c 'bundle install && bundle exec jekyll serve' things fails with: ... Bundle complete! 8 Gemfile dependencies, 29 gems now installed. Bundled gems are installed into `/usr/local/bundle` Configuration file: /host/_config.yml Source: /host Destination: /host/_site Incremental build: disabled. Enable with --incremental Generating... Liquid Exception: No such file or directory @ rb_sysopen - /host/_repos/sel4/manual/generated_markdown/GeneralSystemCalls.md in ApiDoc.md jekyll 3.6.2 | Error: No such file or directory @ rb_sysopen - /host/_repos/sel4/manual/generated_markdown/GeneralSystemCalls.md Any hint what's failing here? I don't even see a folder "_repo", but I assume the build should create one? Thanks, Axel

2 1

Getting Started
by Dave Richards 14 Sep '18

14 Sep '18

I am in the process of reading the Getting Started documentation and building a development environment on Debian Linux. I thought RefOS would be the best example project to start with. When I execute the command: repo init -u ssh://git@github.com/seL4/refos-manifest -b master I get the response: Please make sure you have the correct access rights and the repository exists. Permission denied (publickey). fatal: Could not read from remote repository. Please make sure you have the correct access rights and the repository exists. fatal: cannot obtain manifest ssh://git@github.com/seL4/refos-manifest Apparently something has changed since the instructions were written. Dave

2 1

Notion of a User in seL4
by Amit Goyal 11 Sep '18

11 Sep '18

Hi All, As far as I understand, in seL4, the notion of a subject is similar to a thread (process). Each process has a different cspace and thus has different capabilities. Correct me, if I am wrong. Currently, we can make different components say server and client which run on the same seL4 kernel. They can interact with each other by creating endpoint and adding capability for that endpoint, in others cspace. Now, I want to extend it and run client and server on different host machines which run seL4. The threads (client and server) thus generated will be different users as per the standard linux convention. a) How does the communication happen in such a scenario in seL4? The problem which I see is how the capabilities for endpoint on one machine will be minted into other machine's process cspace. b) I also want to understand the notion of a user in seL4. -- Thanks and Regards, Amit Goyal

2 1

seL4 - getting the execution time of different threads
by Mr. Peace 11 Sep '18

11 Sep '18

Hello together, I was wondering how you do get the execution time in seL4 if you are using multiple threads. In the initial thread I can use the timer as it is shown in the tutorial about timers since I do have the bootinfo, vka, allocman and so on. But how do I use the timer to measure the execution time of the other threads without stopping their execution to "pull" the time from the initial thread? Is it possible to share the timer or create new ones in the other threads? Or is there another way to measure the execution time? Some background information: The threads have different VSpace's and CSpace's. Used tutorials: seL4-tutorial 4, seL4-tutorial timer. The other threads do not have a bootinfo in their environment. Kind regards, Chris

4 5

Strange behavior when writing to memory mapped to a custom device in the VMM.
by Dan DaCosta 09 Sep '18

09 Sep '18

To Whom It May Concern: I am observing seL4+VM+ARM behavior on the TK1-SOM that I find very puzzling. Consider the following code: #define idx(i) (i%16) for(i = 0; i < buf->capacity() && buf->capacity() > 16; i++, pArray++){ mem[idx(i)] = *pArray; } where 'pArray' is the array representation of 'buf' and 'mem' is a memory mapped page set that corresponds to a page set of memory that is managed by a fault handler in the VMM (something I have installed myself using a 'DEV_CUSTOM' device). This code runs as I would expect. However, the follow code results in an assertion failure in the VMM: #define idx(i) (i%16) for(i = 0; i < 16; i++, pArray++){ mem[idx(i)] = *pArray; } The error report follows: 32 bit ARM insts not decoded -------- Pagefault from [Linux]: write fault @ PC: 0xbd7499a8 IPA: 0xe0001000, FSR: 0x2000046 Context: r0: 0xb6d2a050 r1: 0x0 r2: 0xb6ac76b8 r3: 0x4c r4: 0xb6d2a050 r5: 0xb6d2a8ec r6: 0x1 r7: 0xb6d2a050 r8: 0x7fb73000 r9: 0xad13cfff r10: 0xabe31310 r11: 0x19 r12: 0xb6d285d8 pc: 0x7f68f9a8 r14: 0x7f68f99c sp: 0xaf1c3c20 cpsr: 0x80000010 -------- Assertion failed: rt >= 0 (../projects/seL4_projects_libs/libsel4arm-vmm/src/fault.c: get_rt: 357) Some added information that may be helpful; if the strange modulo operation I am performing on the index is removed I receive a similar crash for both code snippets. Any thoughts on where I might look to get to the bottom of this problem would be helpful. Thanks! Dan DaCosta

2 1

CAmkES VMM platform support
by Grant Jurgensen 07 Sep '18

07 Sep '18

Hi all, I was hoping someone could clarify for me a couple of points regarding the CAmkES VMMs. First off, I have a program I want to run under a linux VM within CAmkES. However, it is written in a language which can be compiled to x86-64 but not IA-32. The impression I have gotten from the documentation and the examples is that the x86 CAmkES VMM only supports the 32-bit variant. Is that correct? My attempt to build the project targeting x86_64 has been met with errors (qemu complains "Huge page not supported by the processor"). Alternatively, said program can be compiled to ARMv6. In fact, the ultimate goal is for this project to run on an Odroid XU4, but as that platform is not currently supported by the CAmkES ARM VMM, I was hoping to build up the infrastructure as much as possible by testing it on any platform I could. The two platforms that are supported for the ARM VMM do not seem to have support on the qemu end though, so unfortunately I have no way of testing there either. Is it fair to assume that porting the Odroid implementation to the Odroid XU4 would be a non-trivial undertaking, or are they perhaps more similar than I am imagining? Thanks, Grant Jurgensen

2 4

issues in running sel4test on RISC-V rocket-chip FPGA
by Tuo Li 06 Sep '18

06 Sep '18

Hi guys, I have ported rocket chip (github.com/ucb-bar/fpga-zynq) on a ZCU102 FPGA board and it successfully runs riscv-linux. It's RV64G RISC-V. I am trying to run sel4test on the same hardware system. So far, the system gives no output after "Jumping to kernel-image entry point..." and seems to be stuck there. The same code has been tested on qemu simulator targeting spike 1.10 with the same device tree, following the online guide ( https://docs.sel4.systems/Hardware/RISCV.html) No problem. I have seen this thread ( http://sel4.systems/pipermail/devel/2018-August/002069.html) and used the solution provided for modifying the paddr range. I tried to add a few printf statements and even a fail statement in the boot.c file in kernel/src/arch/riscv/kernel/, which I guess is the first function executed after head.S. Same problem happens. Any suggestions? Thanks. Best regards, Tuo

2 2