- Devel - lists.sel4.systems

Questions about Vchan
by Daniel Wang 14 Mar '18

14 Mar '18

Hi all, I’m trying to figure out how to use the Vchan library to setup communication between guest OS and native components. I got couple questions how you can give me some advices. 1. I saw the camkes_vchan_con_t structure in the helloworld components (camkes-arm-vm), but I could not find the implementation for vchan_con_new_connection(), vchan_con_rem_connection(), etc. Are those autogenerated by camkes? If so how it is generated? static camkes_vchan_con_t con = { .connect = &vchan_con_new_connection, .disconnect = &vchan_con_rem_connection, .get_buf = &vchan_con_get_buf, .status = &vchan_con_status, .alert = &vchan_con_ping, .wait = &vevent_wait, .poll = &vevent_poll, .dest_dom_number = 0, .source_dom_number = 50, }; 2. I tried to compile the Vchan support and demo helloworld components for odroid-xu. But the compile shows error due to the VM.h file (camkes-arm-vm/projects/vm/components/VM/src/cmks_vchan_vm.c:23) cannot be found. How can I generate the VM.h file? Thanks a lot! Best Regards -Daniel Wang

4 5

seL4 developer review of RISC-V privileged ISA spec?
by Kelly Dean 14 Mar '18

14 Mar '18

The RISC-V privileged ISA is not yet finalized. Have the seL4 developers reviewed the draft [1], in case they might have any recommendations for improvement? For example, just last year a blunder (H-mode) was removed from the draft per a proposal [2] on the mailing list. Finalization is planned for this year. Speak now or forever hold your peace. The first public draft of the memory consistency model [3] was also released just last December. And platform standardization, especially the IOMMU, is in progress. [1] https://content.riscv.org/wp-content/uploads/2017/05/riscv-privileged-v1.10… [2] https://groups.google.com/a/groups.riscv.org/forum/#!msg/isa-dev/SfEDPLU0NU… [3] https://groups.google.com/a/groups.riscv.org/forum/#!topic/isa-dev/hKywNHBk…

6 5

Questions about Allocman
by Daniel Wang 12 Mar '18

12 Mar '18

Hi all, I’m trying to understand the code a little bit more. This is kind of a random question. I’m wondering that in a case where we call to allocate a frame using allocman library, where is the physical address of a certain region is stored? In allocman_t there are multiple fields: size_t num_utspace_chunks; struct allocman_utspace_chunk *utspace_chunk; size_t *utspace_chunk_count; struct allocman_utspace_allocation **utspace_chunks; struct allocman_utspace_chunk { size_t size_bits; seL4_Word type; size_t count; }; struct allocman_utspace_allocation { seL4_Word cookie; cspacepath_t slot; }; I didn’t find struct that hold the paddr, also after we create a frame where is that paddr stored? It is stored in slot.capPtr? Also What does the field cookie for? Best Regards -Daniel Wang

3 3

Share UART with Guest Linux
by Daniel Wang 10 Mar '18

10 Mar '18

Hi all, For experiment, I created a simple app along with the vmm using CamKES-ARM-VM repository. Currently the simple app only prints strings periodically using printf(). However as soon as the guest Linux starting running. I cannot print anything and also receives error as following: I assumes it is due to the iommu capability got assigned to Linux by VMM. Is there a way to allow native app also prints information on the screen using printf()? ------------------ libsel4muslcsys: Error attempting syscall 162 FAULT HANDLER: data fault from hello.control (ID 0x1) on address 0xffffff80, pc = 0x135ac, fsr = 0x3840046 FAULT HANDLER: pc = 0x135ac FAULT HANDLER: sp = 0x142d20 FAULT HANDLER: lr = 0x135ac FAULT HANDLER: r0 = 0xffffff80 FAULT HANDLER: r1 = 0 FAULT HANDLER: r2 = 0 FAULT HANDLER: r3 = 0 FAULT HANDLER: r4 = 0x26 FAULT HANDLER: r5 = 0 FAULT HANDLER: r6 = 0 FAULT HANDLER: r7 = 0xfffffff2 FAULT HANDLER: r8 = 0x1 FAULT HANDLER: r9 = 0 FAULT HANDLER: r10 = 0 FAULT HANDLER: r12 = 0x142caa FAULT HANDLER: r14 = 0x135ac FAULT HANDLER: cpsr = 0x20000050 FAULT HANDLER: memory map: FAULT HANDLER: +-- 0x00143fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00143000 -- FAULT HANDLER: | stack FAULT HANDLER: +-- 0x0013f000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x0013e000 -- FAULT HANDLER: | <undescribed> FAULT HANDLER: +-- 0x00137fff -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00137000 -- FAULT HANDLER: | IPC buffer FAULT HANDLER: +-- 0x00136000 -- FAULT HANDLER: | guard page FAULT HANDLER: +-- 0x00135000 -- FAULT HANDLER: | <undescribed> FAULT HANDLER: +-- 0x00131fff -- FAULT HANDLER: | code and data FAULT HANDLER: +-- 0x00010000 -- CPIO: 2 files found. 0) linux 0x00059c70, 16302080 bytes 1) linux-dtb 0x00fe5ce8, 29415 bytes Best Regards -Daniel Wang

1 1

Compilation Error with version
by Thad Seeberger 08 Mar '18

08 Mar '18

Good day. I am getting hung up compiling the CAmkES compiles. I'm getting following error which I believe is because the version.h.d does not exist. Where is the version set? thx [camkes-accelerator] building... -- Configuring done -- Generating done -- Build files have been written to: /home/xxxx/seL4_camkes_x86_64/stage/x86/pc99/accelerator ninja: error: '/home/xxxx/seL4_camkes_x86_64/tools/camkes/tools/accelerator/DEPFILE', needed by '.', missing and no known rule to make it make: *** [/home/xxxx/seL4_camkes_x86_64/stage/x86/pc99/accelerator/camkes-accelerator] Error 1 ive traced it down I think to this block in the Cmakeadd_custom_command( OUTPUT ${CMAKE_CURRENT_BINARY_DIR} OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/include/version.h OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/version.h.d # Build a valid dependency file from the print-deps script, this is a little awkward COMMAND echo "include/version.h: " > "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/print-deps.py" >> "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND sed -i "s/$$/\\/" "${CMAKE_CURRENT_BINARY_DIR}/version.h.d" COMMAND COMMAND "${CMAKE_CURRENT_SOURCE_DIR}/mkversion.py" >"${CMAKE_CURRENT_BINARY_DIR}/include/version.h" DEPENDS mkversion.py DEPENDS print-deps.py DEPFILE ${CMAKE_CURRENT_BINARY_DIR}/version.h.d )

4 8

CapDL spec for Camkes-ARM-VM
by Daniel Wang 08 Mar '18

08 Mar '18

Hi all, I’m trying build a PoC system based on the camkes-arm-vm repository. I saw the init process is created using CapDL, but I’m having trouble to find the the CapDL spec file. Could you please point it out for me? Also for the first step, I’m trying to build another app side-by-side with the VMM and guest Linux. I assume I need to modify the CapDL. I’m not exactly the work flow with CapDL can you give me a hint? Thanks. Best Regards -Daniel Wang

2 2

ARM-VM with Linux Distribution
by Daniel Wang 06 Mar '18

06 Mar '18

Hi all, I was able to compile the camkes-arm-vm and run it on a TK1-SOM board. I wonder if it is possible to run a Linux distribution as the guest OS, such as Ubuntu, Fedora, etc.? If so how can we do that? Best Regards -Daniel Wang

2 1

Re: [seL4] seL4 VMM Hangs during loading time
by Daniel Wang 02 Mar '18

02 Mar '18

Hi Kent and Peter, Thank you so much for your response. I do not know what exactly caused the issue. But I upgraded my toolchain and recompiled the image again and it loaded this time. The GCC version is version 7.2.1 (before it was 4.6). Although I still see the misaligned information like this: CACHE: Misaligned operation at range [90000000, 90000014] CACHE: Misaligned operation at range [90001000, 900091c4] CACHE: Misaligned operation at range [900091c4, 900098d8] CACHE: Misaligned operation at range [900198d8, 900198e0] CACHE: Misaligned operation at range [900198e0, 91392ae0] CACHE: Misaligned operation at range [91394000, 913a4820] CACHE: Misaligned operation at range [913a4820, 913a8000] Another thing I found is that U-boot for TK1-SOM cannot detect ethernet, but I was able to copy the image into MMC and load from there. There are two things I want to do with the seL4 ARM VMM platform. First, I want to incorporate the secure boot from U-boot to seL4 and then using seL4 to verified signed Linux. Second, I want to build a PoC native application and allow the communication between the native app to communication with App running in Linux. I’m wondering if anyone did those two things before that can give me some advice? I implemented the the second scenario before using L4re with a paravirtualized L4Linux. But I’m exactly sure how to do it with seL4 yet. Best Regards -Daniel Wang > On Mar 1, 2018, at 8:00 PM, <Kent.Mcleod(a)data61.csiro.au> <Kent.Mcleod(a)data61.csiro.au> wrote: > > Hi Daniel, > > Two things to try: > > First is to confirm that CONFIG_PRINTING is enabled to distinguish if the kernel is successfully starting its init process. > > Second is to check what ${loadaddr} is set to. Yours seems correct, ours seems to be 0x81000000, but that is for the tk1 jetson dev board. > > You could also try editing the elfloader to print out the contents of the kernel entrypoint before it jumps there to confirm that it is the correct instructions in the stage/arm/tk1/kernel.elf binary. > > Below is what I see when I boot the project on our devboard. > > Kind regards, > Kent. > > ---- > U-Boot SPL 2015.10-rc5-00002-gf861f51-dirty (Oct 13 2015 - 13:44:41) > > > U-Boot 2015.10-rc5-00002-gf861f51-dirty (Oct 13 2015 - 13:44:41 +1100) > > TEGRA124 > Model: NVIDIA Jetson TK1 > Board: NVIDIA Jetson TK1 > DRAM: 2 GiB > MMC: Tegra SD/MMC: 0, Tegra SD/MMC: 1 > tegra-pcie: PCI regions: > tegra-pcie: I/O: 0x12000000-0x12010000 > tegra-pcie: non-prefetchable memory: 0x13000000-0x20000000 > tegra-pcie: prefetchable memory: 0x20000000-0x40000000 > tegra-pcie: 2x1, 1x1 configur��K��Ʌ�pcie: probing port 0, using 2 lanes > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, retrying > tegra-pcie: link 0 down, ignoring > tegra-pcie: probing port 1, using 1 lanes > In: serial > Out: serial > Err: serial > Net: RTL8169#0 > Hit any key to stop autoboot: 2 > 0 > Tegra124 (Jetson TK1) # setenv autoload no && dhcp && tftpboot 0x81000000 jetson1/sel4-image > setenv autoload no && dhcp && tftpboot 0x81000000 jetson1/sel4-image > BOOTP broadcast 1 > BOOTP broadcast 2 > BOOTP broadcast 3 > BOOTP broadcast 4 > DHCP client bound to address 10.13.1.172 (2929 ms) > Using RTL8169#0 device > TFTP from server 10.13.0.130; our IP address is 10.13.1.172 > Filename 'jetson1/sel4-image'. > Load address: 0x81000000 > Loading: ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################################################# > ################################ > 3.8 MiB/s > done > Bytes transferred = 20493516 (138b4cc hex) > Tegra124 (Jetson TK1) # bootelf 0x81000000 > bootelf 0x81000000 > ## Starting application at 0x90000000 ... > ELF loader: monitor mode init done > Copy monitor mode vector from 90001000 to a7f00000 size 50 > Number of IRQs: 192 > Load seL4 in nonsecure HYP mode 600001da > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 > paddr=[90000000..9139ffff] > ELF-loading image 'kernel' > paddr=[80000000..8003cfff] > vaddr=[e0000000..e003cfff] > virt_entry=e0000000 > ELF-loading image 'capdl-loader-experimental' > paddr=[8003d000..8158dfff] > vaddr=[10000..1560fff] > virt_entry=18484 > Enabling hypervisor MMU and paging > Jumping to kernel-image entry point... > > Bootstrapping kernel > Total 28 IOASID set up > Region [c to 28) for SMMU caps > Booting all finished, dropped to user space > > > > From: Devel <devel-bounces(a)sel4.systems> on behalf of Daniel Wang <danielwang.ksu(a)gmail.com> > Sent: Friday, March 2, 2018 7:47 AM > To: devel(a)sel4.systems > Subject: [seL4] seL4 VMM Hangs during loading time > > Hi all, > > I’m trying to run seL as a microvisor following the CAMKES-ARM-VM. My development board is TK1-SOM from ColoradoEngineering. I was able to flash the U-boot to to load seL4 HYP mode. However when I try to load the kernel. The system just hangs. I got stuck here any help would be appreciated thank you! > > I built the capdl-loader-experimental-image-arm-tk1 > and can copied it to the TK1 MMC storage, then I followed the wiki to setup env bootm_boot_mode to nonsec. Attachment is the printout: > > ------------------------------------------------------------------------------------------- > U-Boot 2018.03-rc3-00090-g3990c9d (Mar 01 2018 - 14:33:40 -0500) > > TEGRA124 > Model: Colorado Engineering TK1-SOM > Board: CEI tk1-som > DRAM: 2 GiB > MMC: sdhci@700b0400: 1, sdhci@700b0600: 0 > Loading Environment from MMC... OK > In: > serial > Out: serial > Err: serial > Net: No ethernet found. > Hit any key to stop autoboot: 0 > Tegra124 (TK1-SOM) # setenv bootm_boot_mode nonsec > Tegra124 (TK1-SOM) # saveenv > Saving Environment to MMC... Writing to MMC(0)... OK > Tegra124 (TK1-SOM) # ext2ls mmc 0 > <DIR> > 4096 . > <DIR> > 4096 .. > <DIR> > 16384 lost+found > <DIR> > 4096 boot > <DIR> > 4096 bin > <DIR> > 4096 dev > <DIR> > 12288 etc > <DIR> > 4096 home > <DIR> > 4096 lib > <DIR> > 4096 media > <DIR> > 4096 mnt > <DIR> > 4096 opt > <DIR> > 4096 proc > > 62 README.txt > <DIR> > 4096 root > <DIR> > 4096 run > <DIR> > 12288 sbin > <DIR> > 4096 srv > <DIR> > 4096 sys > <DIR> > 4096 tmp > <DIR> > 4096 usr > <DIR> > 4096 var > > 150994944 testfile > > 20524388 capdl-loader-experimental-image-arm-tk1 > Tegra124 (TK1-SOM) # ext2load mmc 0 ${loadaddr} capdl-loader-experimental-image-arm-tk1 > 20524388 bytes read in 593 ms (33 MiB/s) > Tegra124 (TK1-SOM) # bootelf ${loadaddr} > CACHE: Misaligned operation at range [90000000, 90000014] > CACHE: Misaligned operation at range [90001000, 900091c4] > CACHE: Misaligned operation at range [900091c4, 900098d8] > CACHE: Misaligned operation at range [900198d8, 900198e0] > CACHE: Misaligned operation at range [900198e0, 91392ae0] > CACHE: Misaligned operation at range [91394000, 913a4820] > CACHE: Misaligned operation at range [913a4820, 913a8000] > ## Starting application at 0x90000000 ... > ELF loader: monitor mode init done > Copy monitor mode vector from 90001000 to a7f00000 size 50 > Number of IRQs: 192 > Load seL4 in nonsecure HYP mode 600001da > ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 > paddr=[90000000..913a7fff] > ELF-loading image 'kernel' > paddr=[60000000..6003cfff] > vaddr=[e0000000..e003cfff] > virt_entry=e0000000 > > ------------------------------------------------------------------------------------------- > > Best Regards > -Daniel Wang > > > >

1 0

seL4 VMM Hangs during loading time
by Daniel Wang 02 Mar '18

02 Mar '18

Hi all, I’m trying to run seL as a microvisor following the CAMKES-ARM-VM. My development board is TK1-SOM from ColoradoEngineering. I was able to flash the U-boot to to load seL4 HYP mode. However when I try to load the kernel. The system just hangs. I got stuck here any help would be appreciated thank you! I built the capdl-loader-experimental-image-arm-tk1 and can copied it to the TK1 MMC storage, then I followed the wiki to setup env bootm_boot_mode to nonsec. Attachment is the printout: ------------------------------------------------------------------------------------------- U-Boot 2018.03-rc3-00090-g3990c9d (Mar 01 2018 - 14:33:40 -0500) TEGRA124 Model: Colorado Engineering TK1-SOM Board: CEI tk1-som DRAM: 2 GiB MMC: sdhci@700b0400: 1, sdhci@700b0600: 0 Loading Environment from MMC... OK In: serial Out: serial Err: serial Net: No ethernet found. Hit any key to stop autoboot: 0 Tegra124 (TK1-SOM) # setenv bootm_boot_mode nonsec Tegra124 (TK1-SOM) # saveenv Saving Environment to MMC... Writing to MMC(0)... OK Tegra124 (TK1-SOM) # ext2ls mmc 0 <DIR> 4096 . <DIR> 4096 .. <DIR> 16384 lost+found <DIR> 4096 boot <DIR> 4096 bin <DIR> 4096 dev <DIR> 12288 etc <DIR> 4096 home <DIR> 4096 lib <DIR> 4096 media <DIR> 4096 mnt <DIR> 4096 opt <DIR> 4096 proc 62 README.txt <DIR> 4096 root <DIR> 4096 run <DIR> 12288 sbin <DIR> 4096 srv <DIR> 4096 sys <DIR> 4096 tmp <DIR> 4096 usr <DIR> 4096 var 150994944 testfile 20524388 capdl-loader-experimental-image-arm-tk1 Tegra124 (TK1-SOM) # ext2load mmc 0 ${loadaddr} capdl-loader-experimental-image-arm-tk1 20524388 bytes read in 593 ms (33 MiB/s) Tegra124 (TK1-SOM) # bootelf ${loadaddr} CACHE: Misaligned operation at range [90000000, 90000014] CACHE: Misaligned operation at range [90001000, 900091c4] CACHE: Misaligned operation at range [900091c4, 900098d8] CACHE: Misaligned operation at range [900198d8, 900198e0] CACHE: Misaligned operation at range [900198e0, 91392ae0] CACHE: Misaligned operation at range [91394000, 913a4820] CACHE: Misaligned operation at range [913a4820, 913a8000] ## Starting application at 0x90000000 ... ELF loader: monitor mode init done Copy monitor mode vector from 90001000 to a7f00000 size 50 Number of IRQs: 192 Load seL4 in nonsecure HYP mode 600001da ELF-loader started on CPU: ARM Ltd. Cortex-A15 r3p3 paddr=[90000000..913a7fff] ELF-loading image 'kernel' paddr=[60000000..6003cfff] vaddr=[e0000000..e003cfff] virt_entry=e0000000 ------------------------------------------------------------------------------------------- Best Regards -Daniel Wang

3 2

How to avoid timeout exceptions in non-buggy server code
by Kelly Dean 02 Mar '18

02 Mar '18

The article “Mixed-criticality support in seL4” at https://lwn.net/Articles/745946/ says seL4's solution to the problem of CPU budget exhaustion while in a non-reentrant shared data-structure server is timeout exceptions. The server might time out by chance, through no fault of its own. A more robust solution is to simply disallow calling any such server that advertises a WCET longer than the client's per-period CPU budget, and when a call is made, have the kernel check whether the client's remaining CPU budget ≥ server's WCET. If it is, then proceed with the call as normal. If it isn't, then verify that the client's per-period CPU budget ≥ server's WCET. If that verification succeeds, then terminate the budget for the client's current period early, and actually enter the server at the beginning of the client's _next_ period. (If the verification fails, then the kernel tells the client that the call is disallowed.) If the server fails to return before exhausting the client's CPU budget, then the server has violated its own WCET, which is a bug. Thus, a non-buggy server will never time out, so timeout exception handlers handle only bugs, not routine system operation. If the server's actual WCET is W, then from the client's point of view, the server's apparent WCET is almost 2W, because the client might make the call with remaining CPU budget X such that X is just barely less than W, in which case the kernel will terminate the client's current budget early (so the client loses X) and enter the server at the beginning of the next period, and the server might then take W to return, making the client wait X+W altogether (plus, of course, the remainder of the period, during which other VMs run). But with seL4's current solution, the server's apparent WCET is even longer than 2W, because the server could run for X, time out, be restarted (taking time R), then run for W, making the client wait X+R+W altogether.

2 5