- Devel - lists.sel4.systems

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

Camkes Build Error
by Amit Goyal 05 Sep '18

05 Sep '18

Hi All, My Camkes has been working fine since now. Suddenly, it stopped working and produce the attached error log on running ninja. I am running it on x86 system (i5 processor), ubuntu 16.04 on qemu: I am running the following commands: mkdir build cd build ../init --plat pc99 --tut hello-camkes-2 --solution ninja Can you please suggest a possible way out? -- Thanks and Regards, Amit Goyal

2 1

Does seL4 support raspberry pi 3B+
by talos 04 Sep '18

04 Sep '18

Hi I saw that seL4 supported raspberry pi 3B, did it support 3B+ now? If it did not, how can I modify it for 3B+? Thanks! Sincerely

2 1

SMC in seL4
by 冀东旭 31 Aug '18

31 Aug '18

Hello, I'm porting sel4 to imx6q sabrelite as the trusted OS in trustzone. I initialize the monitor mode directly using the functions "install_monitor_hook()" and “switch_to_mon_mode()”. Is the sp in monitor mode appropriate? After calling smc in SVC mode, it hangs(do nothing in smc_handle()). What's wrong with it? Do you have any ideas? Thank you! Dongxu Ji

2 1

seL4 benchmark configure
by 송대영 31 Aug '18

31 Aug '18

Hi, I want to change seL4 benchmark configuration in ninja build tool. First, I want to change seL4's cache use. Sencond, I want to change CPU core number. How can I change these configuration?

2 1

32 bit vs 64 bit
by Chris Rothrock 31 Aug '18

31 Aug '18

When building the x86 demo for both 32 and 64 bit builds, it looks like the kernel is still a 32 bit elf file regardless of the build and only the sel4test-driver file is what is either 32 bit or 64 bit depending on which is selected. Is this normal or should the kernel also be 64 bit on the 64 bit build? -- Thank You, Chris Rothrock Senior System Administrator (315) 308-1637

2 1