- Devel - lists.sel4.systems

SDHC drivers (cont.)
by Norrathep Rattanavipanon 19 Jan '17

19 Jan '17

My apology that I have to continue the discussion from the old thread: ( http://sel4.systems/pipermail/devel/2016-October/001056.html) My goal is to read and write data from/to micro sd in SabreLite platform. I tried both Adrain and Anna's suggestions in that thread and they dont seem to fix the problem. Nothing returns error and I also changed cacheable parameter in sel4utils_new_pages_at_vaddr to 0 (I believe this is what Anna meant instead of setting 3rd argument of vspace_new_pages). The code's still stuck inside mmc_block_read function. I tracked it down and it seems like BRR and BWR interrupt statuses are never set to 1 I add my code below, please let me know if anything is wrong with my code. ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); assert(error == 0); ps_io_ops_t io_ops = { .io_mapper = io_mapper }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev, 0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); // return id=3 error = sdio_init(id, &io_ops, dev); assert(error == 0); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); assert(error == 0 && mmc_card != NULL); void *vaddr = vspace_new_pages(&vspace, seL4_AllRights, 5, seL4_PageBits); assert(vaddr != NULL); uintptr_t paddr = 0; printf("mmc card capacity %llu bytes\n", mmc_card_capacity(*mmc_card)); long read_len = mmc_block_read(*mmc_card, 0x50000, 1, vaddr, paddr, NULL, NULL); // Stuck here printf("read %lu bytes\n", read_len); Thanks Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 3

CAmkES Templates
by Chris Guikema 18 Jan '17

18 Jan '17

Hello, I am working on a CAmkES application attempting to build a seL4 Network Stack. I am basing this on the CAmkES-VM and utilizing UDP Protocol with the lwIP library. During my build process, I get quite a few linking errors like this: undefined reference to `pbuf_alloc' This is odd, because in the templates, the proper header files are being linked in. There are also warnings like this: Warning: no template for ethdriver_1.to.source Even though the connection does exist: connection seL4Ethdriver eth_driver(from router.ethdriver, to ethdriver.client); Is there something obvious I am doing wrong? Thanks Chris

2 2

questions about SMMU on TK1 VMM
by PX 18 Jan '17

18 Jan '17

Hi, I have some questions about the SMMU on the new version of TK1 VMM as follows: 1. In the source code, smmu.c, the IO ASID 1 is assigned to hardware engine, AFI, which is supposed to connect with PCIE devices. However, when I add 1 to vm.smmu in vm.camkes, the VM can not access Ethernet and cause a SMMU translation error. But it works if I add 0 to vm.smmu as suggested by Kent. whats the reason to do so? 2. Each IO device is assigned with an IO space mapping. However, there is no IO ASID associated with these mappings. Does that means these mappings are associated with an IO ASID in the order given in vm.smmu? 3. Is it possible for the VMM to change the IO mapping for a specific device? say, invalidate old mapping and load a new mapping? what's the rough idea to do so? thanks Peng

2 1

questions about PCIE SMMU for tk1 vmm
by PX 16 Jan '17

16 Jan '17

Hi, I am confused by the SMMU management for PCIE device in the updated TK1 VMM. The IO ASID for PCIE device is 0. However, the start IO ASID is from 1 as defined in smmu.h. When initialized, the lookup table, smmu_ioasid_to_pd, has no entry for IO asid 0 at all. I don't understand how the page table for PCIE device is generated and used by SMMU? which part source code should I check ? thanks Peng

2 1

Re: [seL4] quesitons about TK1 VMM
by Kent.Mcleod＠data61.csiro.au 13 Jan '17

13 Jan '17

Hi Peng, Adding the ethernet card requires adding the 0 ASID in the vm.camkes file that I mentioned in the previous email. vm.smmu = [0, 10, 24]; This gives permission for PCIE devices to read and write to memory. I confirmed that on the TK1 Jetson the ethernet port works after this change. You may need to run "ifconfig eth0 up" to enable the device once the image boots. Regards, Kent. ? ________________________________ From: PX <seawolf.peng(a)gmail.com> Sent: Friday, January 13, 2017 12:13 PM To: Mcleod, Kent (Data61, Kensington NSW) Subject: Re: quesitons about TK1 VMM Kent, I am using NVIDIA Jetson TK1 board. The reason I want to use insecure config is to enable VM Linux to use Ethernet port. I do not care about the SD card. How can I just add Ethernet card? is there a way for me to avoid adding SD card to The VM linux as you just suggest in your email? Thanks Peng On Thursday,January 12, 2017, <Kent.Mcleod(a)data61.csiro.au<mailto:Kent.Mcleod@data61.csiro.au>> wrote: Hi Peng, Which hardware are you using to run the image? This project has only been tested on the TK1-SOM made by Colorado Engineering. The ethernet port doesn't work as the version of Linux that we use doesn't support it. As for your second question, we configure the IOMMU to only let Linux use the emmc device and USB device on the TK1-SOM. The error is caused because Linux is trying to access a SD card device that it isn't authorized to access. The TK1-SOM doesn't have any SD card hardware so camkes doesn't set up access. If you want to use the Insecure config then you will need to modify apps/vm/vm.camkes and add the right ID to vm.smmu on line 443. To find out which ID to add we take the ID:98 from your Address translation error and look it up in the TK1 technical reference manual. In the memory controller section of the manual there is a "Error Data Capture: Status" section that starts on page 716. Using the table there you can look up ID:98 to see that it belongs to the SWGROUP sdmmc3a. We can now take this and look in seL4 ("kernel/include/plat/tk1/plat/machine/smmu.h?") to find the relevant ASID. From the list of ASIDs we see that SMMU_SDMMC3A_ASID is defined as 23. This is the ID that needs to be added to the vm.smmu array in vm.camkes. Hope this helps, Regards, Kent. ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of PX <seawolf.peng(a)gmail.com> Sent: Friday, January 13, 2017 9:03 AM To: devel(a)sel4.systems Subject: [seL4] quesitons about TK1 VMM Hi, I built a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. I have some quesitons about the tk1_vmlinux. Question 1: If I use the original tk1_vm_defconfig, the eth0 does not work in vm. Is the tk1_vm_linux in default not supposed to access Ethernet card? Hpw do I access Ethernet card in this case? Question 2: If I change the VM conifg into insecure, CONFIG_TK1_INSECURE=y, the VM can not get booted, I get "SMMU address translation error". The error message is appended as follows: " [ 10.503932] mmc1: Invalid maximum block size, assuming 512 bytes [ 10.566465] mmc1: SDHCI controller on 700b0400.sdhci [700b0400.sdhci] using ADMA 64-bit SMMU Address translation error: ID: 98 address: 0xae609000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.617123] mmc1: ADMA error" Is this error caused by bugs in source code or my wrong config? if the later case, what's the correct config? thanks Peng

2 1

quesitons about TK1 VMM
by PX 12 Jan '17

12 Jan '17

Hi, I built a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. I have some quesitons about the tk1_vmlinux. Question 1: If I use the original tk1_vm_defconfig, the eth0 does not work in vm. Is the tk1_vm_linux in default not supposed to access Ethernet card? Hpw do I access Ethernet card in this case? Question 2: If I change the VM conifg into insecure, CONFIG_TK1_INSECURE=y, the VM can not get booted, I get "SMMU address translation error". The error message is appended as follows: " [ 10.503932] mmc1: Invalid maximum block size, assuming 512 bytes [ 10.566465] mmc1: SDHCI controller on 700b0400.sdhci [700b0400.sdhci] using ADMA 64-bit SMMU Address translation error: ID: 98 address: 0xae609000 type: 6 direction: 0x0 IOPT permission: read 0x0 write 0x0 nonsecure 0x0 [ 10.617123] mmc1: ADMA error" Is this error caused by bugs in source code or my wrong config? if the later case, what's the correct config? thanks Peng

1 0

question about SEL4PROJ /camkes-arm-vm-manifest
by PX 12 Jan '17

12 Jan '17

Hi, all I try to build a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. However, I can not compile it. I get errors when the compiler tries to build "camkes-accelerator" . I don't put any new code yet. I just: 1) repo init the url ; 2) repo sync; 3) make tk1_vm_defconfig; and 4) make. Did I do something wrong here? thanks Peng

2 5

Overly eager xsave size rejection
by Corey Richardson 12 Jan '17

12 Jan '17

in src/arch/x86/machine/fpu.c:140 on 4.0.0, there is > if (x86_cpuid_ebx(0x0d, 0x0) != CONFIG_XSAVE_SIZE) { > printf("XSAVE buffer set set to %d, but should be %d\n", CONFIG_XSAVE_SIZE, x86_cpuid_ebx(0x0d, 0x0)); > return false; > } I want to force a large(r than 576) xsave region so that TCBBits is always 11, to help my userspace be vaguely more kernel-config-independent. I don't think it's a problem if the xsave buffer in the TCB is larger than the hardware will actually use? I also think this is buggy. Shouldn't it be querying ecx, since things like AVX aren't enabled in the kernel? To be clear, this is my suggested change: > if (x86_cpuid_ecx(0x0d, 0x0) > CONFIG_XSAVE_SIZE) { > printf("XSAVE buffer set set to %d, but should be at least %d\n", CONFIG_XSAVE_SIZE, x86_cpuid_ecx(0x0d, 0x0)); > return false; > } -- cmr http://octayn.net/ +16038524272

2 5

question about SEL4PROJ /camkes-arm-vm-manifest
by PX 12 Jan '17

12 Jan '17

Hi, all I posted this question yesterday, and get no answer. Let me to be more specific this time. I try to build a TK1 ARM VMM image from the source code SEL4PROJ/camkes-vm-manifest in GitHub. However, I can not compile it. I get errors when the compiler tries to parse capDL. The errors are appended as follows: " make: Entering directory '/home/dev/Documents/new_vmm/projects/capd /capDL-tool' stack setup make: stack: Command not found Makefile:37: recipe for target 'sandbox' failed make: *** [sandbox] Error 127 make: Leaving directory '/home/dev/Documents/new_vmm/projects/capdl/capDL-tool' Makefile:51: recipe for target '/home/dev/Documents/new_vmm/stage/arm/tk1/parse-capDL/parse-capDL' failed " I checked that there is a file called stack.ymal in the directory: ~/capdl/capDL-tool. My system is also installed latest ghc and ghc-prof. Anybody can help me on this problem? Thanks Peng

3 3

Using the seL4 Benchmark Tool
by Chris Guikema 12 Jan '17

12 Jan '17

Hello, I am currently attempting to use the seL4 Benchmark tool. After going through the menuconfig (kernel -> build options -> Enable Benchmarks -> Track threads and kernel utilization time), I attempt to rebuild, and get a host of errors: In file included from /home/chrisguikema/gdbtest/kernel/include/compound_types.h:16:0, from /home/chrisguikema/gdbtest/kernel/include/types.h:15, from /home/chrisguikema/gdbtest/kernel/src/api/faults.c:14: /home/chrisguikema/gdbtest/kernel/include/object/structures.h:249:5: error: unknown type name 'benchmark_util_t' benchmark_util_t benchmark; And a lot more, but all along the "not a structure or union" line, which makes me think that either the header file isn't being linked properly, or the #ifdefs aren't working for everything. Did I do something improperly in my setup? Thanks, Chris Guikema

2 1

Workshop debrief?
by Jeff Waugh 10 Jan '17

10 Jan '17

Hey there, I might be hoping a little too much for video, but will there be slides and notes from the Workshop? (Particularly interested in the gaps discussion.) Would be handy content on the wiki. :-) Thanks, Jeff

3 4

config-independent object type numbers
by Corey Richardson 10 Jan '17

10 Jan '17

Right now, object type numbers vary based on the kernel config (eg, CONFIG_VTX) etc. This is a huge source of pain for the Rust userspace libraries which don't integrate with seL4's build system. Is it possible for those enums to explicitly label every potential object type for a given architecture with a fixed number? -- cmr http://octayn.net/ +16038524272

2 2

seL4 as Xen guest / AWS
by Tony Arcieri 09 Jan '17

09 Jan '17

Has anyone managed to run seL4 as a Xen HVM guest? I was more specifically curious about running seL4 on an EC2 instance. I was curious about the possibility of using seL4 as the host OS for a "unikernel"-like deployment of a Rust application split into a small set of services living in different capability spaces (e.g. network, key storage / crypto) -- Tony Arcieri

3 3

sel4test 4.0.x.xml broken?
by Corey Richardson 09 Jan '17

09 Jan '17

It seems that the line <project name="seL4.git" path="kernel" revision="4.0.x-compatible"/> should be <project name="seL4.git" path="kernel" revision="4.0.0"/> Either that, or a tag is missing from the kernel repo. -- cmr http://octayn.net/ +16038524272

2 1

questions about the vgic maintenance for sel4 TK1 ARM VMM
by PX 09 Jan '17

09 Jan '17

Hi, all I have questions about the vgic maintenance for sel4 tk1 ARM VMM. When the VM acknowledges an IRQ, an exception is raised and is delivered to the VMM. Could someone explain how seL4 intercepts the VM ack? How is this exception is raised ? I am confused because the VM is supposed to totally control the MMIO of the device and can write any thing to the device. How can seL4 be triggered in this case? Which part of source code allows seL4 to intercept the VM ack? Thanks Peng

2 1

Interest in 32-bit x86 Rust userspace?
by Corey Richardson 07 Jan '17

07 Jan '17

Is anyone interested at all in the 32-bit x86 Rust userspace libraries? I'm considering dropping support for them, as I don't personally plan to have any support for them in Robigalia, instead focusing on x86_64. Note that this wouldn't impact any Rust CAmkES components using the support in the sel4 buildsystem, just the sel4-sys, rust-sel4, etc crates. -- cmr http://octayn.net/ +16038524272

1 0

DMA driver in VM
by PX 07 Jan '17

07 Jan '17

Hi, I have a generic question about DMA driver in the VM on sel4. How does the device driver in the vm put physical address in the DMA controller given that there is no emulation in sel4? I worked on TK1 sel4 hypervisor extention version, but cannot find any address translation from vmm. Thanks Peng

1 0

pic/no-pic and some other questions
by Vasily A. Sartakov 06 Jan '17

06 Jan '17

Greetings. I have merged MIPS port with 4.0.0 release. Now I would like to clean up my code and need to remove many small issues that I did not fix during the porting before making the code public. In fact, most of the current problems are related to toolchains: 1. The first problem is a position independent code. Could you please describe me seL4' vision about it? muclibs is building with -fPIC, but everything else doesn't, right? I have a very tricky set of GCC’ flags, related to MIPS’ GOT, small data, abicalls, pic/non-pic, etc, and many of them are not working together. 2. MIPS assembler has several features, one of them is that the -O0 code requires having an addition space above the top of the stack for 4 registers: > 43b610: 27bdffe8 addiu sp,sp,-24 <— start of the function > 43b614: afbf0014 sw ra,20(sp) > 43b618: afbe0010 sw s8,16(sp) > 43b61c: afb0000c sw s0,12(sp) > 43b620: 03a0f021 move s8,sp <— frame stack > 43b624: afc40018 sw a0,24(s8) <— save 1st arg for a subroutine call > 43b628: afc5001c sw a1,28(s8) <— save 2nd arg for the subroutine > 43b62c: afc60020 sw a2,32(s8) <— save 3rd arg for the subroutine So, each time when I am allocating new stack I should return not top of the stack, but top_of_the_stack - 4*sizeof(seL4_Word). As result, sel4utils_configure_thread_config becomes platform specific. Could you please consider a possibility to put it into the «arch» as sel4utils_arch_init_context, or add something like «sel4utils_arch_configure». Also, it is important: this is an issue only for -O0 code, as far I see, -O2 uses different methods for arguments passing. I am trying to build toolchains which do not use frame pointer this style for -O0 code, but I am not sure about the result. 3. I really like how you redesigned declaration syscalls. Now I have a freedom to modify syscalls and do not care about the mainline declarations because now there are syscall wrappers. However, my toolchain generates very poor code for CONFIG_LIB_SEL4_PUBLIC_SYMBOLS and «DEFAULT» — I have proper working code only for CONFIG_LIB_SEL4_INLINE_INVOCATIONS. What is the conceptual difference of these declaration attributes, what they affect? 4. Could you please tell me what was the C equivalent of this asm code: .global __syscall .type __syscall,%function __syscall: sub sp, sp, #4 push {r5,r6} adr r5, 1f ldr r6, 1f ldr r5, [r5,r6] str r5, [sp, #8] pop {r5, r6} pop {pc} .hidden __sysinfo 1: .word __sysinfo-1b something similar to __syscall6 from libmuslc/arch/<arch>_sel4/syscall_arch.h, right? Thank you. P/s Happy new year/merry xmass/happy holidays! -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

xsave region size for haswell/broadwell?
by Corey Richardson 06 Jan '17

06 Jan '17

Does anyone have a "maximal" xsave region size big enough for all the xsave-supporting features seL4 enables on Broadwell or Haswell? I don't have access to a machine with these features, so I can't run a program to get them with cpuid. -- cmr http://octayn.net/ +16038524272

2 1

questions about the address translation for a DMA driver in the ARM VM
by PX 05 Jan '17

05 Jan '17

Hi, all Happy new year! I have some urgent questions about address translation for a DMA driver in the ARM seL4-based VM. Your quick response is highly appreciated! 1. In the ARM sel4-based VM, the MMIO of a device is directly exposed to the device driver in the VM. When the DMA device driver allocates a DMA buffer to a device controller, the device driver can directly tell the real controller the IPA of the buffer starting address, instead of the real physical address. In other words, the device controller can only get the IPA of the buffer starting address. How can this device controller perform DMA without knowing the real PA of the buffer? Does seL4 perform some emulation here? How? 2. A closely related question to 1: when we develop a DMA driver in the VMM space, we put the real physical address of the device descriptor and real physical address of the DMA buffer in the controller registers through its MMIO. We found that the controller cannot find the correct place for the descriptor and the buffer. Do the seL4 hypervisor perform the address translation? If so, which source code does that? Thanks Peng

2 3

Build Error
by Daniel Romero 05 Jan '17

05 Jan '17

Hi, I am currently on a BeagleBone running Ubuntu 14.04 using gcc-arm-none-eabi. However I am getting the following error running 'make' after 'make menuconfig'. I am wondering if someone can guide me in the right direction [libs/libsel4] building... [GEN] include/sel4/types_gen.h Traceback (most recent call last): File "/home/ubuntu/seL4test/libs/libsel4/tools/bitfield_gen.py", line 26, in <module> from six.moves import range ImportError: No module named six.moves make[1]: *** [include/sel4/types_gen.h] Error 1 make: *** [libsel4] Error 2 Thank you, Hector Daniel Romero hdromero93(a)gmail.com

2 1

seL4test on Odroid-XU4
by Yevgeny Lavrov 05 Jan '17

05 Jan '17

Hello I ran into the following issue while running seL4test suite on Odroid-XU4: Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5 there are pending interrupts 0x00000001 reading sel4test-driver-image-arm-exynos5 3149364 bytes read Exynos5422 # bootelf 0x48000000 ## Starting application at 0x41000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p3 Switching CPU... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p3 paddr=[41000000..4130441f] ELF-loading image 'kernel' paddr=[60000000..60037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[60038000..60411fff] vaddr=[10000..3e9fff] virt_entry=1e74c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info .... 1 untypeds of size 10 1 untypeds of size 11 126 untypeds of size 12 2 untypeds of size 13 3 untypeds of size 14 3 untypeds of size 15 5 untypeds of size 16 3 untypeds of size 17 3 untypeds of size 18 3 untypeds of size 19 3 untypeds of size 20 2 untypeds of size 21 2 untypeds of size 22 1 untypeds of size 23 2 untypeds of size 24 2 untypeds of size 25 2 untypeds of size 26 2 untypeds of size 27 1 untypeds of size 29 Switching to a safer, bigger stack... seL4 Test ========= _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 31 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 2147483648, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 30 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 1073741824, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 29 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 536870912, error 1 ..... _utspace_split_alloc@split.c:247 Failed to find any untyped capable of creating an object at address 0x12dd0000 vka_alloc_object_at@object.h:64 Failed to allocate object of size 4096 at paddr 0x12dd0000, error 1 init_timer_caps@main.c:348 [Cond failed: error] Failed to get untyped at paddr 0x12dd0000 for timer Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid sys_tkill assuming self kill HYP mode is enabled, and seL4test suite is compiled in Debug Mode. Prior to running seL4test, I ran code from seL4 tutorials and those ran w/o any problems. Any suggestions on what I might have done wrong? Thanks

3 4

Exposing TSD on x86
by Corey Richardson 03 Jan '17

03 Jan '17

How do people feel about exposing the TSD (time-stamp disable) bit as a piece of state on the TCB? Ideally it'd be lazily switched. I vaguely want this in Robigalia for disabling access to real time in non-sufficiently-privileged processes. Best, -- cmr http://octayn.net/ +16038524272

2 2

Re: [seL4] Workshop debrief?
by Corey Richardson 19 Dec '16

19 Dec '16

I really ought to stop using my phone for email. Sent back to list. On Mon, Dec 19, 2016, at 05:25, Jeff Waugh wrote: > On Mon, Dec 19, 2016 at 8:19 PM, Corey Richardson > <corey(a)octayn.net> wrote: > > > I'm writing up my notes and will be publishing them on the > > Robigalia blog. > > Will send a link here when it's up. Ihor said he'd be collecting > > slides, > > not sure what the availability of those will be. > > > > Cool -- maybe let the list know too? -- cmr http://octayn.net/

1 0

RELEASE: Announcing CAmkES 2.3.0
by Stephen.Sherratt＠data61.csiro.au 15 Dec '16

15 Dec '16

Announcing the release of CAmkES 2.3.0 Changes in this release: * support for seL4 4.0.0 * new dependency: Haskell Stack (http://haskellstack.org) + Haskell Stack is a haskell version and package manager. It takes care of installing an appropriate version of ghc and cabal for building the capDL translator - part of CAmkES' build system. Check out an example CAmkES system with: repo init -u https://github.com/seL4/camkes-manifest.git -m default-2.3.x.xml repo sync For more information about CAmkES, see: https://wiki.sel4.systems/CAmkES Cheers, Stephen

1 0

ARM bootloaders that matter
by Jeff Waugh 14 Dec '16

14 Dec '16

Hi all, Out of interest, are there any ARM targets the seL4 development team / community care about that do not boot via u-boot or UEFI (whatever the implementation, be it u-boot, vendor-supplied, etc)? Thanks, Jeff

4 5

RELEASE: Announcing seL4 4.0.0
by Parthasarathi.Susarlaajay＠data61.csiro.au 13 Dec '16

13 Dec '16

We are pleased to announce the release of 4.0.0 of seL4. Listed below are a few of the key changes in this release: * Reorder bootinfo structure. * Add missing seL4_AllRights macro in libsel4. * Disallow kernel from using a device frame as an IPC buffer. * Syscall docs in manual now generated by doxygen. * Changes to make verification easier. * Various documentation fixes. * Benchmarks refactoring. * Coding style fixes. * Support for TLB and Cache management. * Preemptible backwards memzero for Retype. * Support for TCB operations in X86 multicore. * Support for raspberry-pi 3. ARM specific changes: * ARM Hyp refactoring. * Update VCPU fault definitions. * Add userspace invocations for hardware debugging. * Enable PMU export for V8. * Support ARM MPCore registers * Fix config dependency for 'IPC Buffer location'. * Use new cap rights structures in iospace. * Move initial setting of TPIDRURW register. * Add seL4_BenchmarkFlushCaches() for arm and ia32. * Support for prefetcher on Cortex-A9. * Fix fastpath_restore on ARM Hyp and implement slowpath and restore in C. * am335x: Prevent out of bounds array access. * TK1 + Remove temporary SMMU memory mapping support. + Correct SMMU PD and PT indexing. + Split the mux controller from the misc region. * OMAP: + Fix issues with OMAP IRQ Code. X86 specific changes: * Add userspace invocations for hardware debugging. * Avoid writing the fs/gs base unless necessary. * Explicitly declare adress of .phys.bss. * Add BSS regions for BOOT and PHYS code. * Write FS and GS base when restoring user context. * Initialize store area when using XSAVE variant instructions. * Efficiently pack objects for fastpath. * Increase IPI words to 3. * Support for x2APIC. * Support larger XSAVE region sizes. * Change ia32 to use fs register for IPC buffer. * Update the bootinfo for number of cores. * Initial support for SMP vt-x. * Split CPU ID management into mode and general. * Fix cpuid family/model composition. * Add X86_64 support. Please note that this release is not source compatible with earlier releases of seL4, please read https://research.csiro.au/tsblog/introduc ing-device-untyped-memory-sel4/ for more information regarding the changes. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/4.0.0.tar.gz [259d9eadaddef579c2b98b91cf40d13a 4.0.0.tar.gz] The manual for this release can be downloaded here: http://sel4.systems/Info/Docs/seL4-manual-4.0.0.pdf Contributors: * Adrian Danis * Alexander Boettcher * Amirreza Zarrabi * Anna Lyons * Christian Helmuth * Corey Richardson * Donny Yang * Hesham Almatary * Jeff Waugh * Joel Beeren * Kent McLeod * Kofi Doku Atuah * Matthew Brecknell * Matthew Fernandez * Matt Rice * Rafal Kolanski * Stephen Sherratt * Thomas Sewell * Xin,Gao Please let us know of any issues that you run into by creating an issue in the issue tracker: https://github.com/seL4/seL4/issues -- Partha Susarla Kernel engineer DATA61 | CSIRO E parthasarathi.susarla(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

seL4 on Zinq7000 on QEMU
by Andrew Gacek 09 Dec '16

09 Dec '16

I'm trying to build and emulate a version of seL4 for the zinq7000 platform, but it crashes immediately. I've started by taking the camkes tutorial and building it for zinq7000: repo init -u https://github.com/seL4/camkes-manifest.git repo sync make arm_simple_defconfig make menuconfig # change seL4 platform to zinq7000 make When I try to emulate it, it crashes right away: qemu-system-arm -M xilinx-zynq-a9 -nographic -kernel images/capdl-loader-experimental-image-arm-zynq7000 qemu: fatal: Trying to execute code outside RAM or ROM at 0x10000000 R00=00000000 R01=00000000 R02=00000000 R03=00000000 R04=00000000 R05=00000000 R06=00000000 R07=00000000 R08=00000000 R09=00000000 R10=00000000 R11=00000000 R12=00000000 R13=00000000 R14=00000000 R15=10000000 PSR=400001d3 -Z-- A svc32 s00=00000000 s01=00000000 d00=0000000000000000 s02=00000000 s03=00000000 d01=0000000000000000 s04=00000000 s05=00000000 d02=0000000000000000 s06=00000000 s07=00000000 d03=0000000000000000 s08=00000000 s09=00000000 d04=0000000000000000 s10=00000000 s11=00000000 d05=0000000000000000 s12=00000000 s13=00000000 d06=0000000000000000 s14=00000000 s15=00000000 d07=0000000000000000 s16=00000000 s17=00000000 d08=0000000000000000 s18=00000000 s19=00000000 d09=0000000000000000 s20=00000000 s21=00000000 d10=0000000000000000 s22=00000000 s23=00000000 d11=0000000000000000 s24=00000000 s25=00000000 d12=0000000000000000 s26=00000000 s27=00000000 d13=0000000000000000 s28=00000000 s29=00000000 d14=0000000000000000 s30=00000000 s31=00000000 d15=0000000000000000 s32=00000000 s33=00000000 d16=0000000000000000 s34=00000000 s35=00000000 d17=0000000000000000 s36=00000000 s37=00000000 d18=0000000000000000 s38=00000000 s39=00000000 d19=0000000000000000 s40=00000000 s41=00000000 d20=0000000000000000 s42=00000000 s43=00000000 d21=0000000000000000 s44=00000000 s45=00000000 d22=0000000000000000 s46=00000000 s47=00000000 d23=0000000000000000 s48=00000000 s49=00000000 d24=0000000000000000 s50=00000000 s51=00000000 d25=0000000000000000 s52=00000000 s53=00000000 d26=0000000000000000 s54=00000000 s55=00000000 d27=0000000000000000 s56=00000000 s57=00000000 d28=0000000000000000 s58=00000000 s59=00000000 d29=0000000000000000 s60=00000000 s61=00000000 d30=0000000000000000 s62=00000000 s63=00000000 d31=0000000000000000 FPSCR: 00000000 Aborted Is there something I'm doing wrong? Thanks, Andrew

2 9

Virtio on camkes-vm
by Robert VanVossen 08 Dec '16

08 Dec '16

Hello, We are looking to add another virtio device to camkes-vm for guests to use. I have been looking through the code at how virtio_net works and I have a pretty decent understanding of how it is configured and used. I have a few design/philosophical questions though. 1. Was any of this (libethdriver, libpci, Ethdriver component, virtio_net.c, virtio_emul.c) ported from somewhere else, or was it all written from scratch? 2. Why is components/Init/src/virtio_net.c used in conjunction with vm0_config.init_cons instead of just using the VMNet templates? 3. Looks like pci handling was decoupled from drivers like libethdriver and it is left up to the VM Init component to configure PCI. What is the reason for that? 4. Virtio_emul.c appears to be the layer that actually provides the virtio interface to the VM. Would it make more sense to make this more generic to cover more devices, or should new emulation files be created for each device? Thanks, Robbie VanVossen

2 1

Huge kernel images no more
by Jeff Waugh 06 Dec '16

06 Dec '16

Hurrah, I was curious about the huge kernel images, and had it on my list to poke at. Adrian's changes merged last night sorted it: x86: Explicitly declare adress of .phys.bss x86: Add BSS regions for BOOT and PHYS code Simulation debug x86_64 image is down from 7.1M to 1.1M. That's more like it! Nice! :-) Thanks, Jeff

2 1

Bitcoin on seL4?
by Carl Dong 02 Dec '16

02 Dec '16

Hi all, I recently acquired a BD-SL-I.MX6 and will be tinkering with it to install seL4. A major use case for me is if I could run [bitcoind](https://en.bitcoin.it/wiki/Bitcoind) or at least [vanitygen](https://en.bitcoin.it/wiki/Vanitygen) on seL4. I'm very new to the system, but is there a relatively easy way of cross-compiling said software for seL4? Would love to spend some time learning. Cheers, Carl Dong accounts(a)carldong.me

4 3

seL4 Memory Management
by Mark Reus 01 Dec '16

01 Dec '16

Hi I have been going through some of the research papers about seL4. I wanted to understand the security features in the memory management. I am a little confused, hope someone can I help me. Quote from the paper "Finally, the kernel ensures that each physical frame mapped by the MMU at a useraccessible address is of the Frame object type. These Frame objects contain no kernel data and since they cannot overlap with other typed objects, direct user access to kernel data is not possible" I understand that seL4 promotes isolation between processes and no allocation is done by the kernel itself rather it is done by user level manager. Since we use untyped memory and we retype them, there is no overlap of objects. The user level resource managers can access both the kernel memory and other memory as well because they have capabilities to both. What exactly in the above quote causes the isolation of user level memory with kernel memory. I am of the notion that the kernel allocated objects are still accessible and can be modified to point to some other memory? Am I misunderstanding something? Regards Mark

4 4

Good C, bad C, verifiable C
by Jeff Waugh 30 Nov '16

30 Nov '16

Howdy, Is there a guide to the dos and don'ts of C according to the seL4 verification process? I kinda remember reading a quick summary somewhere, but can't find it on the wiki. Maybe I read it in one of the papers? I certainly remember reading the moral equivalent of "lol no strings". ;-) Thanks, Jeff

2 1

contiguous physical memory allocation for seL4
by PX 30 Nov '16

30 Nov '16

Hi, all I want to allocate a contiguous physical memory block (larger than a physical page) and map it to contiguous virtual addresses in the vspace, what's the best way to do it? Are there existing libraries allowing me to do that? thanks Peng

3 2

First International seL4 Workshop
by Gernot.Heiser＠data61.csiro.au 29 Nov '16

29 Nov '16

Hey seL4 community! We’d like to invite you to participate in the inaugural seL4 Workshop. Given the growth in the community we are starting an annual seL4 workshop where we can come together to share and learn what is being done with seL4. Unlike the previous developers days, the focus is much more on what is happening with seL4 and what interesting things are being done using seL4 rather than a learning or tutorial event. We’d like participants to join and: - present what they are doing with seL4 - demonstrate seL4-based projects - give tutorials on aspects of seL4 or tools, libraries, environments for working with seL4 - show results or progress of verification work involving seL4 - discuss interesting challenges (and possible solutions) they’ve encountered when using seL4 - discuss visions for the future of seL4 and high-assurance systems This workshop will take place on Thursday December 15, 2016 (and may be extended to December 16th if there is enough demand) in Malibu, CA, USA. Note that you are welcome to attend even if you do not present anything. Please register participation at: https://sel4.systems/Community/Devdays/ Participation is free, and we may be able to provide students with financial assistance for travel. This workshop is sponsored by the Center for Secure and Resilient Systems at HRL Laboratories, LLC, and by Data61. Gernot for the Data61 Trustworthy Systems Team

2 1

Re: [seL4] Timer for Performance Measurement
by Kofidoku.Atuah＠data61.csiro.au 29 Nov '16

29 Nov '16

?Hey Andrew, Sorry I took so long to get back to you: we have a benchmarking suite, seL4Bench (https://github.com/seL4/sel4bench/blob/master/apps/ipc/src/main.c) which should have userspace timers and precise timestamps available for most platforms. As I understand, you will just have to write a new microbenchmark of your own, and import your library, and then insert calls to the relevant timestamp counter functions (https://wiki.sel4.systems/Benchmarking%20guide)? Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of Andrew Mine <secondmine(a)gmail.com> Sent: 04 November 2016 16:30 To: devel(a)sel4.systems Subject: [seL4] Timer for Performance Measurement Hi Is there any inbuilt library to get the time like get_time in seL4? I want to measure IPC performance and overheads for my tasks. Regards Andrew

1 0

Re: [seL4] how to get timing information on seL4 user space
by Kofidoku.Atuah＠data61.csiro.au 29 Nov '16

29 Nov '16

??Hi Peng, Well, an atomic counter would suffice, and if you need to secure the counter, you could wrap it around with a server. You either need a hardware upcounter, or else a periodic event-timer that you can use to emulate a hardware upcounter; from there, you just use your upcounter for your jiffies. Libplatsupport has userspace timer drivers for most platforms we support: https://github.com/seL4/util_libs/tree/master/libplatsupport? Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ From: Devel <devel-bounces(a)sel4.systems> on behalf of PX <seawolf.peng(a)gmail.com> Sent: 29 November 2016 08:27 To: devel(a)sel4.systems Subject: [seL4] how to get timing information on seL4 user space Hi, all I want to get number of ticks, similar to jiffies in Linux, in the ARM seL4 user space. How can I do it? Are there existing libraries I can use? If not, what's the best way to implement it? thanks Peng

1 0

how to get timing information on seL4 user space
by PX 28 Nov '16

28 Nov '16

Hi, all I want to get number of ticks, similar to jiffies in Linux, in the ARM seL4 user space. How can I do it? Are there existing libraries I can use? If not, what's the best way to implement it? thanks Peng

1 0

IPC measurements
by Neelesh Vemula 28 Nov '16

28 Nov '16

Hi I have been measuring the performance of my application and doing some comparisons with other kernels. I had a couple of queries. I am running seL4 on zynq device. I am using the given timer driver in libplatsupport to measure the clock cycles. Queries: 1) I have found the sample benchmark numbers for seL4 IPC from http://l4hq.org/docs/performance.php. Since I am running on Armv7 Cortex A9 , the time for one half way trip is 316 ns. Is this measured from system call to system call or from process to process? 2) I am trying to compare the performance on FreeRTOS and Linux, is there any such comparison on where seL4 stands? 3) Does the IPC time vary with the different api of ReplyRecv, Reply, seL4_NBRecv? I have this question because I am seeing that Reply is taking about twice the amount of clock cycles compared to Recv. In terms of my application, I am majorly looking at measuring one whole cycle which includes: 1) 1st Process sends message to 2nd Process 2) 2nd Process Reads from AXI device space 3) 2nd Process replies with Reply and waits for another command from 1st process 4) 1st process sends another message to 2nd Process 5) 2nd Process writes to the hardware 6) Time from step 1 to step 5 is measured. Results for this on seL4 : 3180 clock cycles FreeRTOS: 2414 clock cycles I am sure there is possibility of unnecessary overheads involved in my measurement, but I expected seL4 to be faster. Can someone help me in this regard. Regards Neelesh Vemula

2 1

Reading executable of the first process in kernel
by Norrathep Rattanavipanon 22 Nov '16

22 Nov '16

Hi, I want to modify the sel4 kernel to compute a checksum over the executable of the first process before executing it. The goal is to ensure that we execute the correct first process. What I'm doing right now is modify try_init_kernel() in kernel/src/archarm/kernel/boot.c by adding the following lines: for(i=ui_p_reg_start, i<ui_p_reg_end; i++) { checksum += *((char*) (i)); } My questions are the following: (1) Is this a right place to perform the checksum (inside try_init_kernel())? I assume in this function, seL4 kernel already takes over and thus this should do the job. (2) Based on my understanding, what I did was computing the checksum over the entire image (which may includes executable of other processes as well). Is there a way to just read the executable of the first process and ignore the rest in seL4 kernel? (3) I'm also curious: where/when does the seL4 kernel start the root process? I see the end of the same file (boot.c) that it just calls try_init_kernel() but does not load the root process. Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

Memory Management
by Mark Reus 22 Nov '16

22 Nov '16

Hi I have a general case about memory allocation in particular with that of the Vspace. I have been reading some documents and trying to compare how it is in Linux Kernel. Any program Virtual memory in a Linux kernel is as shown in picture below where all processes have 1GB of virtual memory which is mapped to kernel space for faster context switches and system calls. _____________________ | Kernel Space (1GB) | |_____________________| | | | User Mode Space | | (3 GB) | | | |_____________________| I have come across this this link http://os.inf.tu-dresden.de/pipermail/l4-hackers/2014/006262.html detailing a little about the sel4 memory management. But I haven't been able to completely comprehend it . I wanted to know if the seL4 kernel also has a similar mapping of kernel space. Regards Mark

2 1

Syscall errors with musl
by Rinat Dobrokhotov 21 Nov '16

21 Nov '16

Hi all, I have written simple programme which gets system time. I get syscall errors when programm is calling gettimeofday function: *main.c:* #include <time.h> #include <sys/time.h> #include <stdlib.h> #include <stdio.h> int main(int argc, char *argv[]) { int iterations = 1000000; struct timeval start, end; gettimeofday(&start, NULL); for (int i = 0; i < iterations; i++) { } gettimeofday(&end, NULL); printf("%ld\n", ((end.tv_sec * 1000000 + end.tv_usec) - (start.tv_sec * 1000000 + start.tv_usec))); return 0; *Errors:* libsel4muslcsys: Error attempting syscall 263 libsel4muslcsys: Error attempting syscall 78 Could you tell me where I mistook? -- Best regards, Rinat Dobrokhotov

2 1

seL4RPC vs seL4RPCCall?
by Andrew Gacek 18 Nov '16

18 Nov '16

What's the difference between seL4RPC and seL4RPCCall in CAmkES? Is there documentation on the various connectors somewhere? Thanks, Andrew

2 1

Send input to seL4 in QEMU
by Andrew Gacek 17 Nov '16

17 Nov '16

Hi, We are developing an seL4 application that will process UDP packets coming in over a network connection. Eventually, we'll be running this on real hardware with real drivers, but for now we are using QEMU. We have a python script that can generate packet payloads. Is there a way to send this information into QEMU so that we can develop our seL4 application without having the drivers and hardware in place? If it matters, we are using CAmkES as well. Thanks, Andrew

2 3

seL4 Kernel Profiler
by Chris Guikema 17 Nov '16

17 Nov '16

Hello, I am working on a Code Profiler for use in seL4 Systems. I see that the Kernel already has some form of profiling/benchmarking functionality built in. However, I do not see anything in the documentation that covers how this is used. Is there a guide that I can follow to get the kernel profile functional? Thanks Chris Guikema

2 1

Will seL4_Word ever be anything but uintptr_t?
by Corey Richardson 17 Nov '16

17 Nov '16

I guess this is a somewhat philosophical question. It's come up a bit in the Rust libs I've been writing. Casting from pointer-sized things to *specifically* u32/u64 is bit tiresome for the places where I can't abstract over that. -- cmr http://octayn.net/ +16038524272

2 1

seL4 on i.MX53
by Yevgeny Lavrov 15 Nov '16

15 Nov '16

Hello. I've multiple ARM devices at my disposal that I want to use to experiment with seL4, one of them is USB Armory (Architecture: ARMv7 Cortex-A8 Processor: i.MX53 800MHz). Before I get into it, I would like to know if seL4 supports this ARM device. Thanks

2 1

Unable To Map Physical Frame
by Mark Reus 13 Nov '16

13 Nov '16

Hi I want to map the arm global timer which is located at memory location 0xF8F00200 . However, when I am trying to get the physical frame using : error = simple_get_frame_cap(&simple, (void*)global_timer_paddr, 12, &ep_cap_path); if (error) { ZF_LOGE("Failed to find frame at paddr %p\n", global_timer_paddr); return error; } I get the Error Statement on stduout as "main@main.c:209 Failed to find frame at paddr 0xf8f00200" If i print the bootinfo during bootup, I can see that I have access to this region 0xf8000000 | 00000012 | [520 <--> 521 ] Can someone help me as why this issue may be caused? I know that this global timer is said to be mapped in the private region. But I do not what exactly that means and if we cannot do it. Regards Mark

2 1

malloc and SCHED0004
by Vasily A. Sartakov 04 Nov '16

04 Nov '16

Greetings. I am keep working, and now I would like to discuss my second memory-related issue. In contrast with first one, the second issue happens only in SCHED004 test, in malloc function: helper_thread_t **threads = (helper_thread_t **) malloc(sizeof(helper_thread_t*) * NUM_PRIOS); malloc dies because there is no record inside TLB. someone tries to write something to an address, for example, 0x54f1c8. This address is important because it is located outside of the virtual memory allocated for the test. Previous, elf_loader allocates a region and the region ends exactly on 0x54efff. I have experimented with different setups, added some debug functions, and each time I saw the same picture: malloc dies because tries to write to next page outside the allocated region. I know what is the function tries to write. It is a pretrim, part of libmuslc: static int pretrim(struct chunk *self, size_t n, int i, int j) { size_t n1; struct chunk *next, *split; /* We cannot pretrim if it would require re-binning. */ if (j < 40) return 0; if (j < i+3) { if (j != 63) return 0; n1 = CHUNK_SIZE(self); if (n1-n <= MMAP_THRESHOLD) return 0; } else { n1 = CHUNK_SIZE(self); } if (bin_index(n1-n) != j) return 0; next = NEXT_CHUNK(self); printf("next - %x, n1 = %x\n", next, n1); split = (void *)((char *)self + n); <————— the split points outside the allocated region split->prev = self->prev; <————— here we die split->next = self->next; split->prev->next = split; split->next->prev = split; split->psize = n | C_INUSE; split->csize = n1-n; next->psize = n1-n; self->csize = n | C_INUSE; return 1; } As a previous, I would like to ask, should I keep in mind something platform specific? maybe you have modified, like a_and asm functions or something else in libmuslc? Also, malloc itself raises questions: void *malloc(size_t n) { struct chunk *c; int i, j; if (adjust_size(&n) < 0) return 0; <….> i = bin_index_up(n); for (;;) { uint64_t mask = mal.binmap & -(1ULL<<i); mal.binmap is used uninitialised. also, when we set up bits inside it? Moreover, I have different values on ARM (0x80000000000) and MIPS (0x8000000000000000), I am not sure that it is ok Thank you! -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 6

Timer for Performance Measurement
by Andrew Mine 04 Nov '16

04 Nov '16

Hi Is there any inbuilt library to get the time like get_time in seL4? I want to measure IPC performance and overheads for my tasks. Regards Andrew

1 0

Does anyone use recycle?
by Adrian.Danis＠data61.csiro.au 03 Nov '16

03 Nov '16

Hi All, If you do not know what recycle is and/or have not used it then you can probably ignore this e-mail. We are considering removing the recycle operation from cnodes, and replacing it with a 'revoke badges' operation. Currently the semantics of recycle are ill defined but can generally be summed up as "put an object back into its initial state". It turns out this is not particularly useful, and is completely unused by us. The proposal is to remove this and have an invocation that will only operate on endpoints and will remove any badged versions of that endpoint, hence the name 'revoke badges'. This is the current semantics of recycling an endpoint, and we see this as the only useful thing recycle does, hence the desire to keep it around. Whilst we do not use recycle we would like to first find out if anybody in the community is using recycle, or has a strong argument for why they would like it to stay. If this is you, please let us know, otherwise we will continue with our plans for removal. Adrian

5 11

need ideas
by Vasily A. Sartakov 01 Nov '16

01 Nov '16

Hello. I have a problem. It is a very complicated problem. I understand that It is hard to give an advice without looking into the sources. But I am stuck and need some ideas in ‘brainstorm’ format as an input for me. So, here is the problem: There are many tests from sel4test suit are working. This is how does it look like: http://pastebin.com/vvnDaUe9 Unfortunately, I found several configurations of the tests, which causes crashes with stable and different symptoms. One of them is looking following: 11 #include <sel4test/test.h> 12 #include "../test.h" 13 #include "../helpers.h" 14 15 #define MIN_EXPECTED_ALLOCATIONS 100 16 17 18 19 20 21 22 23 int test_allocator(env_t env) 24 { 25 /* Perform a bunch of allocations and frees */ 26 vka_object_t endpoint; 27 int error; 28 29 for (int i = 0; i < MIN_EXPECTED_ALLOCATIONS; i++) { 30 error = vka_alloc_endpoint(&env->vka, &endpoint); 31 test_assert(error == 0); 32 test_assert(endpoint.cptr != 0); 33 vka_free_object(&env->vka, &endpoint); 34 } 35 36 return sel4test_get_result(); 37 } 38 DEFINE_TEST(TRIVIAL0001, "Ensure the allocator works", test_allocator) 39 DEFINE_TEST(TRIVIAL0002, "Ensure the allocator works more than once", test_allocator) as you might see, this is little bit modified version of trivial.c tests. Usual, when I am testing all tests, there is no problem with this test. But when I am running this file alone, I have a problem. Also, you might see, that there are several free lines with numbers from 16 to 22. I made this not accidental, it is a source of error. If the test_allocator(env_t env) is lockated in the 23rd line, this tests has no problem. But if I add one more free line, I have an error like this: Starting test suite sel4test Starting test 0: TEST_TRIVIAL0001 TEST_TRIVIAL0001 726:trap!, address error on store! $0 : 0 fffffff8 7 10089000 $4 : 6a6ffc 3f 0 ffffffff $8 : 1 7 1 20 $12 : 70f 0 2 6ae $16 : 6a6ffc 5a6a50 ffffff30 6a6ffc $20 : 3f 5a6e58 5a6a50 6a6fdc $24 : 20 41bab0 0 0 $28 : 0 100848d8 fffffffe 41faf0 Hi : 20 Lo : 0 epc : 41f818 fi : 41f814 ra : 41faf0 Status: 20000002 Cause : 414 Config: 80008482 BadVaddr: f which means, that the test-drivers (I know the ASID) tries to store something to the address 0x0000000f by the instruction located in the 0x41f818 (EPC). Also, it is failed before the starting of trivial.c test! This is what I on the address: 0041f7b4 <unbin>: 41f7b4: 8c83000c lw v1,12(a0) 41f7b8: 27bdffd8 addiu sp,sp,-40 41f7bc: 8c820008 lw v0,8(a0) 41f7c0: afb0001c sw s0,28(sp) 41f7c4: 00808021 move s0,a0 41f7c8: afbf0024 sw ra,36(sp) 41f7cc: 1462000e bne v1,v0,41f808 <unbin+0x54> 41f7d0: afb10020 sw s1,32(sp) 41f7d4: 00a03021 move a2,a1 41f7d8: 00002021 move a0,zero 41f7dc: 0c107afa jal 41ebe8 <.pic.__ashldi3> 41f7e0: 24050001 li a1,1 41f7e4: 3c04005a lui a0,0x5a 41f7e8: 00022827 nor a1,zero,v0 41f7ec: 24846a50 addiu a0,a0,27216 41f7f0: 0c107dac jal 41f6b0 <a_and> 41f7f4: 00038827 nor s1,zero,v1 41f7f8: 3c04005a lui a0,0x5a 41f7fc: 02202821 move a1,s1 41f800: 0c107dac jal 41f6b0 <a_and> 41f804: 24846a54 addiu a0,a0,27220 41f808: 8e030008 lw v1,8(s0) 41f80c: 8e02000c lw v0,12(s0) 41f810: 8fbf0024 lw ra,36(sp) 41f814: 8fb10020 lw s1,32(sp) 41f818: ac430008 sw v1,8(v0) I am quite sure that there is no problem here with unbin function, and the problem somewhere with contexts, or alignment or something else. Also, I am mapping this area RO, so I am also sure that there is no corruption of the user-space regions. Also, I see, that there is a correlation between size of the image and faults: 1349892 ./sel4test-tests.bin_23 1349900 ./sel4test-tests.bin_24 The border line is 1349900 if I have a size of the image below the value -- there is no problem. Unfortunately, 1349900 is not a 'round' value, somehow related to TLB sizes of something else what I know. Also, I should mention, that 'key' variable wich changes when I add new line is an argument of _sel4test_failure: mips-mti-linux-gnu-objdump -d sel4test-tests.bin_23 > bin23.asm mips-mti-linux-gnu-objdump -d sel4test-tests.bin_24 > bin24.asm diff -ua bin23.asm bin24.asm Disassembly of section .init: @@ -3143,7 +3143,7 @@ 4030f0: 3c050043 lui a1,0x43 4030f4: 2484c248 addiu a0,a0,-15800 4030f8: 24a5c964 addiu a1,a1,-13980 - 4030fc: 2406001f li a2,31 + 4030fc: 24060020 li a2,32 403100: 0c107b51 jal 41ed44 <_sel4test_failure> 403104: 0000f021 move s8,zero 403108: 8fbf0074 lw ra,116(sp) @@ -3383,7 +3383,7 @@ 4034b0: 2484c950 addiu a0,a0,-14000 4034b4: 24a5c964 addiu a1,a1,-13980 4034b8: 0c107b51 jal 41ed44 <_sel4test_failure> - 4034bc: 24060020 li a2,32 + 4034bc: 24060021 li a2,33 4034c0: 03c01021 move v0,s8 4034c4: 8fbf0074 lw ra,116(sp) 4034c8: 8fbe0070 lw s8,112(sp) That is all that I have now. Any ideas? Now I do not see any other choice but to gradually reduce the amount of code with keeping this 'border' situation, until I will not have very small set of system functions. Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 3

Configuring Process Issue
by Andrew Mine 28 Oct '16

28 Oct '16

Hi I am working with Zynq based seL4 and currently have written an app which configures two processes using sel4utils_configure_process. Both my other processes are apps that are also elf files generated during the build. I have noticed that when I am configuring two processes in the root task as 102: sel4utils_process_t process1,process2; 103: error = sel4utils_configure_process(&process1, &vka, &vspace, seL4_MaxPrio, PROCESS1_IMAGE_NAME); 104: assert(error == 0); 105: 106: error = sel4utils_configure_process(&process2, &vka, &vspace,seL4_MaxPrio, PROCESS2_IMAGE_NAME); 107: assert(error == 0); The code compiles but I get a runtime error as _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark vka_alloc_object@object.h:51 Failed to allocate object of size 4096, error 1 _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark new_pages_at_vaddr@vspace.c:325 Failed to allocate page load_segment@elf.c:82 ERROR: failed to allocate frame by loadee vka: 10 _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark sel4utils_elf_load_record_regions@elf.c:272 Failed to load segment sel4utils_configure_process_custom@process.c:550 Failed to load elf file _allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and failed from watermark sel4utils_configure_process_custom@process.c:593 Could not clean up vspace Assertion failed: error == 0 (latest-sel4-tutorial/apps/zynq-comm/src/main.c: main: 107) If I remove any one of the process from the root process, it actually works and my process gets launched. I am assuming there is some conflict when the elf is being loaded as both processes are elf files. Regards Andrew

1 0

CallWithMRs is an unexercised code path
by Jeff Waugh 27 Oct '16

27 Oct '16

Hi all, Last night I opened two pull requests to begin fixing the CallWithMRs code path on x86_64 and aarch32. syscall_stub_gen.py couldn't generate x86_64 stubs for the CallWithMRs / non-IPCBuffer path. That didn't surprise me too much, as x86_64 support is relatively new. Then I discovered that libsel4 *always* [1] uses the IPCBuffer path. Hrm. Changing that prompted a quick fix to aarch32's apparently unused, long since even built CallWithMRs. (Similar fixes might be needed in some of the other functions.) The test suite failed with it on aarch32, which I could poke at in more depth, but it worked fine for x86_64. So… what's the status of the *WithMRs functions? Based on my understanding of the source (particularly the new helper functions) and assembly output, they're destined for the chopping block, right? Thanks, Jeff [1] hard coded --buffer parameter to syscall_stub_gen.py in libsel4/Makefile, since late 2015

2 6

Build Error
by Andrew Mine 26 Oct '16

26 Oct '16

Hi I have used sel4-tutorial branch earlier and was able to build and run earlier. I realized that my branch is way behind, so I have cloned the new branch into a separate folder and am compiling for zynq device. I get the following build error: [apps/hello-1] building... [HEADERS] [STAGE] autoconf.h [CC] src/main.o [CC] src/util.o [LINK] hello-1.elf sel4tutorials/stage/arm/zynq7000/lib/libsel4.a: error adding symbols: Archive has no index; run ranlib to add one collect2: error: ld returned 1 exit status make[1]: *** [hello-1.elf] Error 1 make: *** [hello-1] Error 2 Is anyone else facing this issue? I am using arm-none-eabi-gcc for compiling. Regards Andrew

2 1

Allocman Error
by Neelesh Vemula 26 Oct '16

26 Oct '16

Hi I have created a new process from the root/init task. In the new process I have the following code for initializing the allocman as below: vka_t vka; allocman_t *allocman; vspace_t vspace; #define ALLOCATOR_STATIC_POOL_SIZE ((1 << seL4_PageBits) * 10) UNUSED static char allocator_mem_pool[ALLOCATOR_STATIC_POOL_SIZE]; #define ALLOCATOR_VIRTUAL_POOL_SIZE ((1 << seL4_PageBits) * 100) int main(int argc, char **argv) { allocman = bootstrap_use_current_1level(SEL4UTILS_CNODE_SLOT, CONFIG_SEL4UTILS_CSPACE_SIZE_BITS, 0, (1u << CONFIG_SEL4UTILS_CSPACE_SIZE_BITS), ALLOCATOR_STATIC_POOL_SIZE, allocator_mem_pool); allocman_make_vka(&vka, allocman); vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); ZF_LOGF_IFERR(error, "Failed to allocate new endpoint object.\n"); I have the following definition structure shared as enum sel4utils_cspace_layout { /* * The root cnode (with appropriate guard) */ SEL4UTILS_CNODE_SLOT = 1, /* The slot on the cspace that fault_endpoint is put if * sel4utils_configure_process is used. */ SEL4UTILS_ENDPOINT_SLOT = 2, SEL4UTILS_PD_SLOT = 3, FREE_SLOT = 4, }; This particular program has compiled for zynq-7000 platform and when running it I get the following output in the stdout : Just entered the user function vka_alloc_object@object.h:51 Failed to allocate object of size 16, error 1 Assertion failed: error == 0 (/apps/zynq-comm-user/src/main.c: main: 71) I have been not able to figure out why this error is occurring. I can only guess that the allocman was not initialized properly. Can someone help me with what I may have done wrong? Regards Neelesh Vemula

2 1

Exynos Arndale 5420 support
by Yevgeny Lavrov 25 Oct '16

25 Oct '16

Hello. Exynos Arndale 5250 is listed as seL4 supported ARM devices. I would like to know if seL4 also supports Exynos Arndale 5420 board, and if it does, then would the process of mounting seL4 onto Arndale 5420 be the same as with 5250? Thanks

2 1

seL4 Call Issue
by Chris Guikema 25 Oct '16

25 Oct '16

Hello, I am working on a lock system using templates (based on what is found here: https://github.com/seL4/camkes/tree/master/apps/mutex) This system can work, but there are some issues with the components just going back and forth when calling the locks. I believe this is an issue with multiple components using the same endpoint to communicate with the "lock server" and the calls getting pre-empted by other threads. Here are the system calls that are used to hit the endpoint with the (un)lock request. seL4_Send(/*? ep ?*/, info); info = seL4_Recv(/*? ep ?*/, NULL); And in the lock server: seL4_MessageInfo_t info = seL4_Recv(/*? ep ?*/, &sender); ...do locking things seL4_Send(/*? ep ?*/, info); So in order to prevent preempting by other threads, I went and changed the (un)lock request system call to info = seL4_Call(/*? ep ?*/, info); Using print statements, I was able to determine that the lock server receives the proper message on the endpoint and performs the locking operations. However, when it reaches the seL4_Send operation, the system locks up. This shouldn't be the case, because one component is waiting on the endpoint with the seL4_Call, and the other is sending information on the same endpoint, especially when having separate Send & Recv statements works. Am I doing something incorrect? Thanks for your help, Chris Guikema

1 0

Starting Threads in New seL4Utils processes.
by Richard Habeeb 24 Oct '16

24 Oct '16

Hello all, I am using seL4Utils to create some new processes. For these I am also transferring capabilities to some untyped kernel memory so that those processes can start their own worker threads and make endpoints. I've managed to get those threads started; however, I am a bit confused about how the CSpace is laid out now. My problem is that I want these worker threads to have capabilities to an endpoint created by the child process, but I can't figure out how to copy the cap. This is my TCB configure line. error = seL4_TCB_Configure(THREAD_2_CAP, seL4_CapNull, seL4_MaxPrio, SEL4UTILS_CNODE_SLOT, seL4_NilData, SEL4UTILS_PD_SLOT, seL4_NilData, ipc_buffer_vaddr, THREAD_2_IPC_BUF_CAP); Any guidance is appreciated. Thanks. -- Richard Habeeb Research Assistant, Computer Science, USF http://habeebr.bitbucket.org/

1 1

timers in seL4
by Horace Blanc 24 Oct '16

24 Oct '16

Hi, I am trying to understand the timer design of both seL4 as a kernel and as a hypervisor on ARM architecture. I understand that in both cases, seL4 uses a timer in order to preempt its threads. This means that seL4 must keep the control over that timer and cannot let threads use it directly. I also understand that seL4 does not provide any timer API to its threads. It seems then that the intended use is to implement a timer driver in userland in order for other application to access timing functions. But this timer driver cannot access the same timer as seL4. Does this mean that at least two physical timers (or at least two physical timer interfaces) are necessary? ARM virtualization extensions offers a virtual timer to be used by VMs and which is implemented with an offset register. They also offer different timers (one for an hypervisor, one for kernel/application and one for the virtual timer). It seems that the current seL4 as a hypervisor project does not use these extenstions. Do they? If not why? Thank you for your answers

1 0

Freelance
by Marco Reus 21 Oct '16

21 Oct '16

Hi I apologize if this is not the right platform to reach people. But I am looking for a freelancer who has some expereince in working with seL4 kernel. I need some aid in implementation of a project. Regards Vicky

1 0

Larger badges on 64-bit?
by Corey Richardson 21 Oct '16

21 Oct '16

Is there a future in which we recover the extra 32+ bits of padding on 64-bit systems for use in badges? In Robigalia, 28 bit badges are extremely limiting for what we want to use them for. -- cmr http://octayn.net/

2 1

CAmkES Groups
by Robert VanVossen 19 Oct '16

19 Oct '16

Hello, I have been trying to get groups with CAmkES 2.2 working, but it doesn't look like it will build correctly. At first, when I place components in a group, I get that there is an unresolved reference to one of the components during compilation. I was able to get past this by moving the function assign_address_spaces in camkes/camkes/runner/Transforms.py from POST_RESOLUTION to PRE_RESOLUTION, but after that I still ran into some issues: [LD] MyGroup_group_bin if [ 2 -eq 1 ]; then cp "comp1.instance-copy.bin" " MyGroup_group_bin"; else /usr/bin/ccache arm-xilinx-eabi-gcc comp1.instance-copy.bin comp2.instance-copy.bin -Wl,--build-id=none -L<stage_dir>/lib -Wall -nostdinc -std=gnu11 -O2 -D_XOPEN_SOURCE=700 -marm -Wtrampolines -mcpu=cortex-a9 -g -Wno-main -fno-stack-protector -Wl,--start-group -lsel4 -lsel4debug -lc -lsel4muslccamkes -lsel4camkes -lsel4sync -lutils -lsel4vka -lsel4utils -lsel4platsupport -lplatsupport -lsel4vspace -lgcc -Wl,--end-group -static -nostdlib -u _camkes_start -e _camkes_start -o MyGroup_group_bin; fi <stage_dir>/lib/libsel4camkes.a(crt0.o): In function `_camkes_start': (.text+0x6c): undefined reference to `_start' Any insight on this? Are groups supported yet? Thanks, Robbie VanVossen

2 1

SDHC driver in Sabre Lite
by Norrathep Rattanavipanon 19 Oct '16

19 Oct '16

Is there any example on how to use sdhc driver in ( https://github.com/SEL4PROJ/projects_libs/tree/master/libsdhcdrivers)? Currently, I'm struggling to read a block of data from micro-sd in seL4. I use the following code (assertions are omitted here for readability) to instantiate the driver : ps_io_mapper_t io_mapper = {0}; error = sel4platsupport_new_io_mapper(simple, vspace, vka, &io_mapper); ps_dma_man_t dma_man = {0}; error = sel4utils_new_page_dma_alloc(&vka, &vspace, &dma_man); ps_io_ops_t io_ops = { .io_mapper = io_mapper, .dma_manager = dma_man }; sdio_host_dev_t* dev = (sdio_host_dev_t*) malloc(sizeof(*dev)); assert(dev != NULL); memset(dev,0, sizeof(*dev)); enum sdio_id id = sdio_default_id(); error = sdio_init(id, &io_ops, dev); mmc_card_t* mmc_card = (mmc_card_t*) malloc(sizeof(*mmc_card)); error = mmc_init(dev, &io_ops, mmc_card); void* vaddr = (void*) 0x1980000; uintptr_t paddr = (uintptr_t) 0x119a7000; long read_len = mmc_block_read(*mmc_card, 0, 5, vaddr, paddr, NULL, NULL); And the code's stuck in mmc_block_read function where interrupt status (BRR and BWR) are never on. Thanks in advance, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 5

Missing untypeds on x86?
by Jeff Waugh 18 Oct '16

18 Oct '16

Hi all, Using x86 master on qemu with 2G memory, the kernel's map looks good: Parsing GRUB physical memory map Physical Memory Region from 0 size 9fc00 type 1 Physical Memory Region from 9fc00 size 400 type 2 Physical Memory Region from f0000 size 10000 type 2 Physical Memory Region from 100000 size 7fee0000 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from 7ffe0000 size 20000 type 2 Physical Memory Region from fffc0000 size 40000 type 2 But the largest physical address of non-device untyped I get from bootinfo is 0x1faf9000. Same at 1G to 3G, though it does the right thing at 128M. On the other hand, x86_64 looks fine with 0x7ffc0000, and adapts to more. btw, very exciting to see x86_64 code land! Working well so far. Thanks, Jeff

2 1

question about adding device to ARM VM linux
by PX 18 Oct '16

18 Oct '16

Hi, all I have a question about adding a device to ARM VM linux. When a device is added to the vmlinux, two functions, map_device () and map_ram () are invoked. I don't understand the purpose of map_ram(). In map_device(), the capacity to the device is used to set up the mapping between a virtual address and the MMIO (of the device). Then, in the map_ram (), a capacity to the virtual address is allocated. I am confused because the virtual address is already mapped to the mmio of the device. why do we need to allocate a capacity for the virtual address? Should the capacity be the same as the one for the device? Thanks Peng

1 0

Benchmark results?
by Corey Richardson 18 Oct '16

18 Oct '16

Hello, Are there any public results from sel4bench, or should I get my own numbers for some hardware? -- cmr http://octayn.net/

2 1

adding code to the main.c for ARM VMM
by PX 18 Oct '16

18 Oct '16

Hi, I have posted this question before and my problem is not totally solved because I am not familiar with Makefile. I try to make my question more specific as follows. I want to add new code, which is already organized under a directory, say, test. I want to add the directory test to main.c file for ARM VMM, located at ~/projects/vm/apps/vm/components/VM/src/main.c. In the program, we want to refer to the sub-directories by relative path to the directory test. what is the easy to do that? How can we add the directory test to the search path so that we can include the header files by the relative path to the directory test, say include "test1/test1.h"? We tried to modify the makefile at ~projects/vm/apps/vm, but we have to add all the sub-directories, and there are problems for the files with the same name under different directories. thanks Peng

2 1

Re: [seL4] endpoint.c
by Vasily A. Sartakov 17 Oct '16

17 Oct '16

> we take address that causes syscall from the ksCurThread and set them back. Thus, FaultInstruction should point to something different, right? > I have add FaultInstruction in the same manner as it made in ARM platform: sub lr, lr, #4 /* Store FaultInstruction */ str lr, [sp, #(PT_FaultInstruction - PT_LR_svc)] I am tacking address of an instruction causes exception, subtract 4 from the value, and save it into the FauiltInstruction. Now get* and set* functions are: word_t PURE getRestartPC(tcb_t *thread) { return getRegister(thread, FaultInstruction); } void setNextPC(tcb_t *thread, word_t v) { setRegister(thread, CP0_EPC, v); } Also, Faultinstruction is part of frameRegisters and «linked» with cp0_epc of seL4_UserContext (sel4arch.xml) Now both tests are passed: Starting test 27: TEST_RECYCLE0001 TEST_RECYCLE0001 Running test RECYCLE0001 (Basic endpoint recycle testing.) <<seL4 [decodeInvocation/609 T0x8fee3f00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #101.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #163.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #230.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #303.>> <<seL4 [decodeInvocation/609 T0x809a1b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #364.>> <<seL4 [decodeInvocation/609 T0x809db100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #428.>> <<seL4 [decodeInvocation/609 T0x809db300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #491.>> <<seL4 [decodeInvocation/609 T0x809db500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #564.>> <<seL4 [decodeInvocation/609 T0x809db700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #619.>> <<seL4 [decodeInvocation/609 T0x809db900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #694.>> <<seL4 [decodeInvocation/609 T0x809dbb00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #761.>> <<seL4 [decodeInvocation/609 T0x809dbd00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #828.>> <<seL4 [decodeInvocation/609 T0x809dbf00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #831.>> <<seL4 [decodeInvocation/609 T0x8fe29100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #898.>> <<seL4 [decodeInvocation/609 T0x8fe29300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #965.>> <<seL4 [decodeInvocation/609 T0x8fe29500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1032.>> <<seL4 [decodeInvocation/609 T0x8fe29700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1099.>> <<seL4 [decodeInvocation/609 T0x8fe29900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1170.>> <<seL4 [decodeInvocation/609 T0x8fe29b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1221.>> <<seL4 [decodeInvocation/609 T0x80a13100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1295.>> <<seL4 [decodeInvocation/609 T0x80a13300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1354.>> <<seL4 [decodeInvocation/609 T0x80a13500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1427.>> <<seL4 [decodeInvocation/609 T0x80a13700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1490.>> <<seL4 [decodeInvocation/609 T0x80a13900 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1563.>> <<seL4 [decodeInvocation/609 T0x80a13b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1628.>> <<seL4 [decodeInvocation/609 T0x80a13d00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1635.>> <<seL4 [decodeInvocation/609 T0x80a13f00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1698.>> <<seL4 [decodeInvocation/609 T0x80aa1100 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1765.>> <<seL4 [decodeInvocation/609 T0x80aa1300 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1828.>> <<seL4 [decodeInvocation/609 T0x80aa1500 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1897.>> <<seL4 [decodeInvocation/609 T0x80aa1700 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #1966.>> <<seL4 [decodeInvocation/609 T0x80aa1b00 "child of: 'RECYCLE0001'" @40f9f8]: Attempted to invoke a null cap #2033.>> Test RECYCLE0001 passed Starting test 28: TEST_RECYCLE0002 TEST_RECYCLE0002 Running test RECYCLE0002 (Recycle deletes caps) <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #297.>> <<seL4 [decodeInvocation/609 T0x809a1500 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #165.>> <<seL4 [decodeInvocation/609 T0x809a1700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #231.>> <<seL4 [decodeInvocation/609 T0x809a1900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #297.>> <<seL4 [decodeInvocation/609 T0x809a1b00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #361.>> <<..> <<seL4 [decodeInvocation/609 T0x80a90700 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2003.>> <<seL4 [decodeInvocation/609 T0x80a90900 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2073.>> <<seL4 [decodeInvocation/609 T0x80a90b00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2131.>> <<seL4 [decodeInvocation/609 T0x80a90f00 "child of: 'RECYCLE0002'" @40f8b8]: Attempted to invoke a null cap #2203.>> Test RECYCLE0002 passed Can you please tell me something about the Faultinstruction context field, and, in general, what the assumptions about the behaviour of CPU you put into the design. For example, in MIPS, in a case of a trap, EPC points on instruction causes a trap, but in a case of an interrupt, PC and further EPC points on next instruction. Should I take this into the account somewhere in the kernel? > >> Hope that helps. >> >> Regards, >> Hesham >> ________________________________________ >> From: Devel <devel-bounces(a)sel4.systems> on behalf of Vasily A.Sartakov <sartakov(a)ksyslabs.org> >> Sent: Friday, October 14, 2016 12:33 AM >> To: devel(a)sel4.systems >> Subject: [seL4] endpoint.c >> >> Hello. >> >> I have a problem with endpoint.c test (RECYCLE0001): >> >> Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 of file /long/path/apps/sel4test-tests/src/tests/endpoints.c >> >> I am reading MR(0) in call_func above this check and see, that seL4_Call returns values that were sent before. For example, 100 for the first thread, 101 for the second and etc. Thus, as far I understand, cnode_recycle does not work at all. I am pretty sure that my seL4_Call syscall was implemented properly. I have looked inside the kernel, and tried to track everything related to cteRecycle and do not see anything platform specific. I know that it is a complicated question, but any ideas or hints where to look?

2 2

Fwd: Microkernels / Component-based OSes devroom - Call for Participation
by Vasily A. Sartakov 17 Oct '16

17 Oct '16

Just want to invite you to FOSDEM’17 > The developers of several free and open-source microkernel-based > operating systems will meet at FOSDEM 2017 [1] in Brussels, Belgium > and will share a developer room on Saturday of February 04, 2017 [2]. > The devroom is currently looking for content in the form of talks and > activities related to the area of microkernel-based operating systems. > Possible topics include, but are not limited to: > > * Introduction of a specific OS or framework > * Design of subsystems and the general architecture of an OS > * Enabling support for hardware (architectures, device drivers) > * Used languages and tools > * Maintainance and testing > * Security and robustness > * Trends and challenges > * Use cases, experiences, lessons learned and demos > > Please use the Pentabarf [3] system to submit your proposals and file it > under the track “Microkernels and Component-based OS”. You do not need > to create a new account if you already have one. When in doubt, please > use the devroom mailing list [4]. If you do not want to give a talk > yourself, you may still send suggestions for what else you would like to > see, or do in the devroom. Please send your suggestions to the mailing > list. The deadline for your proposal is on December the 4th. > > Make sure to include the following in your proposal: > > * Title of your talk (will be printed in the FOSDEM booklet) > * Your full name (will be printed in the FOSDEM booklet) > * A short abstract (one or two paragraphs) > * Duration of your talk (please, at least 25 and no longer than 45 min) > > The official devroom schedule (along with the accepted talks) will be > announced on December the 11th on the devroom's mailing list and the > speakers will be notified via e-mail. The schedule will also be published > on the FOSDEM website. > > > About FOSDEM > > FOSDEM is a two-day event organised by volunteers to promote the > widespread use of free and open source software. Taking place in the > beautiful city of Brussels (Belgium), FOSDEM is widely recognised as the > best such conference in Europe. FOSDEM covers a wide spectrum of free > and open source software projects, and offers a platform for people to > collaborate. To this end, FOSDEM has set up developer rooms (devrooms) > with network/internet connectivity and projectors where teams can meet > and showcase their projects. Devrooms are a place for teams to discuss, > hack and publicly present latest directions, lightning talks, news and > discussions. Besides developer rooms, FOSDEM also offers main tracks, > lightning talks, certification exams and project stands. Every year, > FOSDEM hosts more than 5000 developers at the ULB Solbosch campus. > Participation and attendance is totally free, though the organisers > gratefully accept donations and sponsorship. No registration necessary. > > > About the devroom > > Since the first Microkernel devroom in 2012 this devroom has been part of > each following FOSDEM. By now it has become a somewhat institutionalized > tradition for the micro kernel community to meet there; to this date over > a dozen projects have participated in one way or another. Each of the > projects face similar challenges but come up with partially differend > solutions. Therefore, the goal of the Microkernel devroom is to bring the > various projects together, let them exchange ideas, cross-pollinate and > socialize. > > > Social events > > It also has become a habit that the microkernel projects dine together > somewhere in downtown Brussels after the devroom closes. The year 2017 > will not be any different, so there is going to be a microkernel family > dinner on Saturday night. The exact location and time will be specified > later. Consult the FOSDEM web and other projects for additional social > events such as the famous FOSDEM-organized Friday Beer Event and the > FOSDEM-arranged free sightseeing tours for spouses. > > > Important dates recap > > * 04.12.2016: Deadline for submissions > * 11.12.2016: Schedule published and speakers notified of acceptance > * 04.02.2017: The devroom takes places > > > Links > > [1] http://fosdem.org/ > [2] https://fosdem.org/2017/practical/transportation/ > [3] https://fosdem.org/submit > [4] https://lists.fosdem.org/listinfo/microkernel-devroom -- Vasily A. Sartakov sartakov(a)ksyslabs.org

1 0

General Questions
by Mark Reus 17 Oct '16

17 Oct '16

Hi I have recently started with working on sel4 and I have a couple of questions. i) Can a process be spawned or configured only from the root task? (using sel4_configure_process) ii) How to enable or locate prints of ZF_LOGE in kernel? I have enabled kernel prints and debug in make menuconfig. iii) I have followed the tutorial for IPC between a spawned process and root task. The setup is done as follows from the root task: /* create an endpoint */ vka_object_t ep_object = {0}; error = vka_alloc_endpoint(&vka, &ep_object); assert(error == 0); /* * make a badged endpoint in the new process's cspace. This copy * will be used to send an IPC to the original cap */ /* make a cspacepath for the new endpoint cap */ cspacepath_t ep_cap_path; seL4_CPtr new_ep_cap; vka_cspace_make_path(&vka, ep_object.cptr, &ep_cap_path); /* copy the endpont cap and add a badge to the new cap */ new_ep_cap = sel4utils_mint_cap_to_process(&new_process, ep_cap_path, seL4_AllRights, seL4_CapData_Badge_new(EP_BADGE)); assert(new_ep_cap != 0); However, I want to establish communication between two spawned processes. In that case I need to copy the badged endpoint capability of one process into another process. But in the spawned process I wouldn't have access to the pointer (sel4utils_process_t of new process), so how can i use mint_cap_to_process. Can someone help me with these. Thanks in advance. Regards Mark

3 2

endpoint.c
by Vasily A. Sartakov 14 Oct '16

14 Oct '16

Hello. I have a problem with endpoint.c test (RECYCLE0001): Error: seL4_MessageInfo_get_label(tag) == seL4_InvalidCapability at line 50 of file /long/path/apps/sel4test-tests/src/tests/endpoints.c I am reading MR(0) in call_func above this check and see, that seL4_Call returns values that were sent before. For example, 100 for the first thread, 101 for the second and etc. Thus, as far I understand, cnode_recycle does not work at all. I am pretty sure that my seL4_Call syscall was implemented properly. I have looked inside the kernel, and tried to track everything related to cteRecycle and do not see anything platform specific. I know that it is a complicated question, but any ideas or hints where to look? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

sel4 hypervisor communication
by Horace Blanc 12 Oct '16

12 Oct '16

Hi, 1) Is there a mechanism for inter VM communication with seL4 as a hypervisor? 2) If the VMMs run in kernel mode (PL1), as I was told, does it mean they use hvc commands instead of swi/svc commands when sending messages to seL4 as hypervisor? Thank you in advance,

2 1

syscall.c
by Vasily A. Sartakov 11 Oct '16

11 Oct '16

Greetings. I have moved forward to tests in my our MIPS port. Some of them work fine, but not all. Now I have a question about syscall.c test. What exactly we test here? In ARM-based part I see initialisation of 12 registers, performing syscall with further checking that our initialised registers have original values. So, as far I understand, these registers should be modified in a syscall’s inline, thus, they should be allocated on the stack and reloaded after the end of syscall. Right? My issue here is that I have much many than 12 registers and my compiler chooses them randomly (for me). For example, sometimes it uses only S0-S7 with some T0-T9 registers, sometimes all T0-T9 with some S0-S7 registers. Moreover, I cannot put more than 30 asm instructions in one inline (gcc error), thus, maybe I should specify proper register name here. But for that, I should be sure that I understand this test correct. Can we help me? Thank you -- Vasily A. Sartakov sartakov(a)ksyslabs.org

2 2

Spawn new process
by Andrew Mine 11 Oct '16

11 Oct '16

Hi I am working with sel4-tutorials and wanted to spawn a new process using int sel4utils_configure_process_custom(sel4utils_process_t *process, vka_t *target_vka, vspace_t *spawner_vspace, sel4utils_process_config_t config); However, I am not able to understand some of the details required to initialize the parameter config used in the function. Can someone give me link to an example of sorts where this is used. Regards Andrew Mine

1 0

adding new code to VMM on TK1
by PX 10 Oct '16

10 Oct '16

Hi, Please forgive my ignorance. I want to add new code to the seL4-based VM for TK1. However, I find it is hard to add new directories. The newly added directories are always ignored or can not be found by compiler. What's the correct way to add new directories? which scripts we should look into? thanks Peng

3 4

questions about the device driver in virtual machine on ARM seL4 (TK1 board)
by PX 05 Oct '16

05 Oct '16

Hi, I have questions about the device drivers in the virtual machine on ARM seL4. The virtual machine on TK1 board is located on the physical memory starting at 0xb0000000. However, the MMIOs used by the device drivers in the VM are below 0xb0000000. 1.If my understanding is correct, does that mean that a device driver in the VM can actually access a memory block outside of the VM's boundary even though it is mmio. 2. If the device driver actually uses the mmio outside of the VM's memory boundary, do the page tables (including EPT) need to map to this mmio? However, I can not find any code doing the mapping. Do I miss something? Thanks Peng

2 4

Post-mutikernel approach to multiprocessor support?
by Jeff Waugh 04 Oct '16

04 Oct '16

Hi all, Is there anything that can be shared so far about seL4's post-multikernel approach to multiprocessor support? (I couldn't see anything new or upcoming on the publications pages, and figured a paper or two might land before code aimed for Q4'16.) Thanks, Jeff

2 5

Possible seL4 developer day Dec 15–16 in Malibu
by Gernot.Heiser＠data61.csiro.au 04 Oct '16

04 Oct '16

Dear seL4 Community, Part of the Data61 seL4 Team will be in Malibu in mid December and we are considering running another Developer Day. As in the past, this would actually run over 1.5 days, from the morning of the 15th to about mid-day on the 16th and be a combination of lectures and hands-on sessions. As usually we’ll try to make this a free event, provided that our friends at HRL Labs can host us. We have been discussing the possibility of providing an advanced stream besides the “newbie” version we had been running in the past. Right now, we are gauging interest in this. So, if you are interested in participating on those two days, would you please let Ihor know 1) how many participants you expect from your organisation 2) whether you are interested in the newbie or an advanced version, 3) if advanced, what topics you would like covered Examples of advanced materials - advanced driver writing/porting, eg how to port a real Linux driver - advanced real-time topics: eg building stuff from scratch rather than filling in templates - locking and synchronisation - architecting seL4-based systems - process for building real systems: throw everything into a VM, and then extract bits into native components - anything specific you are interested in We’d imagine the advanced stream to be less structured, emphasising largely independent work on a specific problem, with people around to help. It could even be solving a particular problem you have (but we’d need to understand what you’re trying to build beforehand). Gernot & Ihor

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Gernot.Heiser＠data61.csiro.au 29 Sep '16

29 Sep '16

We have just received this comment on github, which I think merits some explanation: > There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. Summary: I accept that this is a valid use case, but the suggested solution is not the right one. There are two reasons why I’m saying this: 1) the current behaviour of send-only IPC is correct and cannot be changed, 2) send-only IPC is the wrong way to address this use case. Re (1): Anyone who tried to use seL4_Send() or seL4_NBSend() will likely have noticed that they are of very little use, because you don’t know whether the message was transferred. So, why can't we return at least a boolean value, indicating whether a message has been delivered or it was dropped on the floor? It’s simple: this would violate the dataflow guarantees provided by seL4. Send-only IPC is there to enable one-way information flow, and consequently can be invoked using a send-only cap. But a send-only cap must not allow any information flow from the receiver to the sender (or else all our isolation proofs would break down). Basically, a return status that can be influenced by the receiver constitutes a back channel that is not authorised by a cap, and as such is verboten. This means that send-only IPC is of very little practical use, except where you really want one-way information transfer, or you have a higher-level protocol that lets you get away with not knowing whether the message was lost. (Eg if the receiver being not ready is a protocol violation by the receiver, and it has only itself to blame for losing the message.) So, could we make send-only IPC a bit more useful by changing the semantics slightly? For example, we could have a return value that indicates successful message delivery if the send was invoked with a send+receive cap, but will always return false if the invocation used a send-only cap? In principle that would be doable without violating security requirements. The cost would be extra checking. It would also be somewhat unsystematic if the semantics of a send-only operation would depend on whether your cap has receive rights as well. It’d be arguably misleading, as you’re doing more than sending. This gets me to (2): send-only IPC is the wrong way to solve the problem. The above use case is clearly one where info flow is inherently two-way: you send something and need an acknowledgment of receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. The problem, of course, is that seL4_Call() is always blocking, there is no polling variant of this syscall. Should there be an seL4_NBCall()? Arguably yes, just as the RT branch already provides a seL4 SignalRecv() syscall, which is the non-blocking equivalent of seL4_ReplyRecv(). Will it happen? Possibly, but not in mainline the near future. The reason is that to add this (fairly simple) feature to the mainline kernel will require verifying it, and our verification engineers are presently very busy delivering on contracted milestones. We’ll discuss this internally. In the meantime I’ve added some explanation of the semantics of seL4_Send()/seL4NBSend() to the FAQ on the seL4 wiki. Gernot

4 6

quesion about TK1 Linux irq
by PX 27 Sep '16

27 Sep '16

Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng

2 1

Fwd: [Fwd: quesion about TK1 Linux irq]
by Jason.Butler＠data61.csiro.au 27 Sep '16

27 Sep '16

The irq numbers are remapped in: kernel/include/plat/tk1/plat/machine.h Jason ? -------- Forwarded Message -------- From: PX <seawolf.peng(a)gmail.com> To: devel(a)sel4.systems Subject: [seL4] quesion about TK1 Linux irq Date: Mon, 26 Sep 2016 17:38:47 -0400 Hi, I have questions about the irqs defined for TK1 guest linux. 1. The linux_pt_irqs[] defined in tk1_vmlinux.h lists all the IRQs for I/O devices, but why they are different from TK1 manual? Does seL4 perform some mapping for guest Linux? 2. what 's the Physical address for Ethernet card on TK1 board? Thanks Peng _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel

1 0

Why send-only IPC doesn't and shouldn't return a success indicator
by Matt Rice 26 Sep '16

26 Sep '16

Gernot.Heiser wrote: > We have just received this comment on github, which I think merits some explanation: >> There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place. ... >This gets me to (2): send-only IPC is the wrong way to solve the problem. > >The above use case is clearly one where info flow is inherently two-way: you send >something and need an acknowledgment of > receipt. This means call-type IPC is the right mechanism, it does exactly that. And on top of that it is more efficient than > separate send-receiver, and avoids (thanks to reply caps) the need to set up a separate reply channel. New to sel4 and the list (so sorry for stuffing up the threading) Couldn't at the expense of an extra notification send, use a notification where the receiver of the notification then should call the then do a non-blocking reply. I didn't see reply being non-blocking described in the manual so please correct me if i am wrong. This only works one party is willing to block correct, and there is no way to short circuit the call if an incoming message could be delivered to the call'ing process before the call can be completed? Although it would seem to take some amount of gymnastics to balance sending and receiving... so if really neither are willing to wait there is always notifications+shared memory?

3 4

Questions about Capability model
by Daniel Wang 21 Sep '16

21 Sep '16

Hi all, I’m new to the capability concept of seL4. Please correct me if I’m wrong. My understand of the capability is that it is a reference to a chunk of memory that allocated for specific purpose. Say if I want to do IPC between two threads A and B, I will need to apply an chunk of memory as endpoint, which give me a capability that I can pass from thread A to thread B is that correct? Also it is ok to assume the message passing mechanism in IPC is a producer-consumer model? The reason I ask it because I’m thinking is it possible for three (or more) threads that need to communicate with each other using the same endpoint, or it has to be paired for each two of those threads to use an endpoint? Thanks -Dan

3 4

developing a Ethernet card server for seL4
by PX 19 Sep '16

19 Sep '16

Hi, all, We want to develop a networking service on top of seL4, which works as a hypervisor, on Jetson TK1. We know that there is source code for lwip under /projects/util_libs/libethdrivers, but there is no support for TK1. We want to know how much effort needed to port the code to TK1 platform? Is it straightforward? Is there any TK1 ethernet driver source code available? Peng

3 3

How to run seL4 as a hypervisor?
by Daniel Wang 19 Sep '16

19 Sep '16

Hi all, Is there any document/tutorial about using seL4 as a hypervisor to running Linux on top? Appreciate for your help. Thanks -Dan

2 1

General Questions
by sixpackgurkenwasser＠use.startmail.com 15 Sep '16

15 Sep '16

Hello, I've got several questions. 1. Is there a simple way to relate a virtual address in the initial threads address space to the corresponding frame cap in the BootInfo? 2. In 8.2.2 of the manual it is stated in that "seL4 provides no way to obtain the physical address of a page from its capability". Isn't that exactly what the GetAddress method of a Page object does(10.4.14)? Cheers, Steve

3 2

Re: [seL4] General seL4 Kernel Questions
by Kofidoku.Atuah＠data61.csiro.au 13 Sep '16

13 Sep '16

Hey, welcome: ? > 1) Once the kernel boots, the control is given to a root task which we define. Does this root task have all permissions and capabilities or do we still need to assign it capabilities? The root task is given capabilities to all kernel objects , and it has full permissions (Read-write-grant) on all of them -- you needn't do any work to cause the root task to have permissions/control over the initial objects. Just need to read and parse the BootInfo struct that describes how they are laid out in your CSpace. >2) Who is in-charge of scheduling or thread suspend (We can start new threads from root task), is it also responsibility in root task to manage and schedule it? Who is in charge of migrating the tasks, flushing CPUs loading new stack etc? The kernel handles scheduling in the main, but threads can be suspended as needed by any other thread that has a capability to the TCB of the thread that you want to manage. Mainline seL4 currently doesn't support multicore, so there is no thread migration, and I do not know what form the multicore extensions will take, with regards to CPU affinity configuration as yet. It's not easy to speculate either, since the entire scheduler is going to undergo intrusive changes when the Real Time extensions are released. >3) While spawning a new thread? Who allocates virtual memory to it? And is the virtual memory allocated equal to 4 GB like in linux kernel where all applications get same Virtual Memory size but different mappings? A new thread is initially a blank TCB -- to associate a virtual address space (VSpace) with it, you'd need to create a VSpace (seL4_Untyped_Retype), and then pass that to the kernel while configuring the TCB (seL4_TCB_Configure). The VSpace is also just a blank page directory, so you have to then create the page tables for the address space, and then create frames to map into the page tables, etc. The VSpace object is a light wrapper around hardware page tables, so yes, they cover a 4GiB address range, but like Linux, seL4 takes up some of that 4GiB for itself. >4) What are the default things loaded into Virtual Memory of a thread? Only the Cspace maybe made available via CNode_mutates? or something else? Nothing -- the day that comes after the darkest night has the greatest number of possibilities -- or something like that: what I'm trying to say is that because no policy is enforced by the kernel (not even executable format) you have the greatest range of flexibility to do what you want with the new thread's VSpace. When you create a new VSpace there is nothing in it at all. The only exception is that when the kernel creates the root task's VSpace, it also then goes on to put the bootinfo struct into it, and in addition it allocates a stack and IPC buffer, and expands the root task's ELF image -- this is a special case because the root task is special. Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)data61.csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________

3 2

Re: [seL4] General seL4 Kernel Questions
by Andrew Mine 13 Sep '16

13 Sep '16

Hi Thanks a lot for the responses. It is much clearer now. I will delve a little bit more into this. Regards Andrew Mine On Mon, Sep 12, 2016 at 2:07 AM, <Kofidoku.Atuah(a)data61.csiro.au> wrote: > Hey, welcome: > > > 1) Once the kernel boots, the control is given to a root task which we > define. Does this root task have all permissions and capabilities or do we > still need to assign it capabilities? > > The root task is given capabilities to all kernel objects , and it has > full permissions (Read-write-grant) on all of them -- you needn't do any > work to cause the root task to have permissions/control over the initial > objects. Just need to read and parse the BootInfo struct that describes how > they are laid out in your CSpace. > > >2) Who is in-charge of scheduling or thread suspend (We can start new > threads from root task), is it also responsibility in root task to manage > and schedule it? Who is in charge of migrating the tasks, flushing CPUs > loading new stack etc? > > The kernel handles scheduling in the main, but threads can be suspended as > needed by any other thread that has a capability to the TCB of the thread > that you want to manage. Mainline seL4 currently doesn't support multicore, > so there is no thread migration, and I do not know what form the multicore > extensions will take, with regards to CPU affinity configuration as yet. > It's not easy to speculate either, since the entire scheduler is going to > undergo intrusive changes when the Real Time extensions are released. > > >3) While spawning a new thread? Who allocates virtual memory to it? And > is the virtual memory allocated equal to 4 GB like in linux kernel where > all applications get same Virtual Memory size but different mappings? > > A new thread is initially a blank TCB -- to associate a virtual address > space (VSpace) with it, you'd need to create a VSpace > (seL4_Untyped_Retype), and then pass that to the kernel while configuring > the TCB (seL4_TCB_Configure). The VSpace is also just a blank page > directory, so you have to then create the page tables for the address > space, and then create frames to map into the page tables, etc. The VSpace > object is a light wrapper around hardware page tables, so yes, they cover a > 4GiB address range, but like Linux, seL4 takes up some of that 4GiB for > itself. > > >4) What are the default things loaded into Virtual Memory of a thread? > Only the Cspace maybe made available via CNode_mutates? or something else? > > Nothing -- the day that comes after the darkest night has the greatest > number of possibilities -- or something like that: what I'm trying > to say is that because no policy is enforced by the kernel (not even > executable format) you have the greatest range of flexibility to do what > you want with the new thread's VSpace. When you create a new VSpace there > is nothing in it at all. > > The only exception is that when the kernel creates the root task's VSpace, > it also then goes on to put the bootinfo struct into it, and in addition it > allocates a stack and IPC buffer, and expands the root task's ELF image -- > this is a special case because the root task is special. > > Kofi Doku Atuah > Kernel engineer > DATA61 | CSIRO > E kofidoku.atuah(a)data61.csiro.au > www.data61.csiro.au > > CSIRO's Digital Productivity business unit and NICTA have joined forces to > create digital powerhouse Data61 > ------------------------------ > > >

1 0

General seL4 Kernel Questions
by Andrew Mine 12 Sep '16

12 Sep '16

Hi I need help with some basic questions which I am getting confused of how seL4 is working. I am currently using the tutorials-seL4 branch. 1) Once the kernel boots, the control is given to a root task which we define. Does this root task have all permissions and capabilities or do we still need to assign it capabilities? 2) Who is in-charge of scheduling or thread suspend (We can start new threads from root task), is it also responsibility in root task to manage and schedule it? Who is in charge of migrating the tasks, flushing CPUs loading new stack etc? 3) While spawning a new thread? Who allocates virtual memory to it? And is the virtual memory allocated equal to 4 GB like in linux kernel where all applications get same Virtual Memory size but different mappings? 4) What are the default things loaded into Virtual Memory of a thread? Only the Cspace maybe made available via CNode_mutates? or something else? I am sorry if the questions are silly, but I am getting confused. Thanks and Regards Andrew Mine

1 0

seL4 GDB
by Chris Guikema 08 Sep '16

08 Sep '16

Hello everyone, DornerWorks has developed a GDB-stub system for the ARMv7 platform (specifically Zynq 7000) that can be found at the following repos: https://github.com/dornerworks/gdbstub-app https://github.com/dornerworks/gdbstub-app-manifest If you have any questions, feel free to ask.

1 0

CAmkES Question
by Chris Guikema 02 Sep '16

02 Sep '16

Hello Ihor, My name is Chris Guikema, and I am an embedded systems engineer at DornerWorks, located in Grand Rapids Michigan. I am currently working on a project that requires the use of the CAmkES system, and I would like some help, if you are willing to. The project is to allow for debugging using CAmkES. The debugging process was successfully implemented in a simple seL4 program by using the init thread to set up an exception thread and setting up the exception endpoint, which was mapped to the init thread. The init thread was then used to implement a bad assembly code, which fired an exception. The exception handler thread was waiting on something to appear at the endpoint, and then grabbed the program counter and the stack of the init thread and sent it to a GDB function, which allowed debugging. My job is to replicate the debugging using CAmkES. However, CAmkES doesn't seem to want the application to utilize any of the seL4 system calls, and I don't believe the application knows its root cspace and vspace, so any attempt to initialize a debug thread and setup an exception endpoint just don't work. What steps do I need to take to 1, set up an endpoint that I could map to the exception endpoint (the simple libraries cause a vm fault), and 2, set up a thread that waits on the application to throw an exception and allow the debugging to occur. Any help you could send me would be appreciated. I look forward to hearing from you. Thanks Chris Guikema

2 1

sel4 as hypervisor
by Horace Blanc 01 Sep '16

01 Sep '16

Hi, I would like to have more information concerning the design of the hypervisor functionality in the sel4 project on ARMv7 architectures. >From what I read (FAQ/announcement from Adrian Danis in this mailing list), sel4 can run an application called VMM which adds that functionality. Here are my questions: 1) Did the design of this functionality require any change in the sel4 microkernel or is it just the VMM in userland that permits it? (what was in the arm_hyp branch that is now in master?) 2) Does this mean that it is a type-2 hypervisor? Do the guest OS run on top of the VMM? 3) How are the virtualization extentions of ARM used? More precisely what runs on the different protection levels (PL0, PL1 and PL2)? 4) To what extent is this hypervisor design pure? Do the guest OS know that it is running on top of seL4? Best, Horace BLANC

2 1

Genode 16.08 supports dynamic workloads on seL4
by Alexander Boettcher 31 Aug '16

31 Aug '16

Hello, we are proud to announce that the just released version 16.08 of the Genode OS Framework brings vastly extended seL4 support, which allows interactive and dynamic system scenarios to run directly on the x86 version of the seL4 kernel. With the new version, users of seL4 can compose dynamic operating systems from a plethora of ready-to-use Genode components. First, there are our time-tested device drivers and protocol stacks: - VESA driver (based on x86emu of XOrg) - Intel graphics driver (based on Linux 4.4.3), e.g., to drive external connectors - Intel wireless stack (based on Linux 4.4.3) including WPA supplicant - Network driver (based on iPXE) - AHCI, PS/2, PIT, ACPI driver - Audio driver (ported from OpenBSD 5.9) - USB driver (based on Linux 4.4.3) with hot-plug support - lwIP - light weight TCP/IP stack - Linux TCP/IP Stack (ported from Linux 4.4.3) - File-system support, e.g., ext2 based on Rump kernels Also, Genode includes a range of low-complexity resource multiplexers: - Secure GUI multiplexer - Nitpicker - Highly configurable and dynamical window manager - Audio mixer - Virtual networking components - Virtual file-system support For application development, there are several runtime environments and high-level libraries: - Noux - UNIX-like subsystem to run command-line-based GNU software like bash, vim, coreutils, gcc/g++, ... - Environments for the Rust, Python, and Lua programming languages - Base libraries like libc, standard C++ library, pthreads, OpenSSL, Readline etc. - Qt5 libraries and applications, including Webkit There's a lot more to explore and - in the pure microkernel way - each of these components are executed in user mode as separate protection domains on seL4. More details about version 16.08 can be found in the extensive release documentation: https://genode.org/documentation/release-notes/16.08 and, for the impatient, a life demo scenario of Genode on seL4 can be downloaded: https://www.genode.org/documentation/release-notes/16.08#Try_Genode_seL4_at… Best regards, -- Alexander Boettcher Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

1 0

Kernel extensions and userspace options
by Jonathan C Day 30 Aug '16

30 Aug '16

Hi, I am very interested in SEL4, partly because I was assured it was impossible to use Formal Methods in kernel development, partly because it's a fascinating project in its own right, but right now because there are some embedded applications that could do with the high level of reliability and security that provable correctness implies. Unfortunately, said applications need a comprehensive network stack and a powerful packet filtering/mangling engine. The latter could imaginably be done in the kernel, as it's deterministic, but I don't see any obvious value. Nonetheless, if someone has coded such a system as a third-party add-on, I would be very interested. There are good arguments for why the former can't be done, in a way that can be proven, and I really want the correctness. In terms of userspace, I believe I could use something like L4Linux (as long as it is still maintained), and I think there's one supplied, but are there other options? Has anyone ported OpenBSD to it? To be honest, I'm not sure I need a multitasking userspace, but I do absolutely need the network stack and packet filter. Everything else can be ported, albeit with difficulty. However, network operating systems are thin on the ground and tend to be proprietary, exactly what I don't want. For those curious, I'm looking to end up with a system with strong bounds on robustness and security, and that can handle things like multipath TCP, network failover, QoS and OpenFlow. However, all of these requirements boil down to a sequential process. Unnecessary complexity is where you end up with problems. If current wisdom says that there's nothing suitable in userspace, then does anyone know if there are there any existing Coloured Petri Nets that I could use to build what I need into the kernel? Even if I can't get better than a quasi-guarantee, it would be something.

3 6

Re: [seL4] Devel Digest, Vol 27, Issue 16 - High Assurance Hardware
by Tyga 30 Aug '16

30 Aug '16

> > Re: > > ------------------------------ > Date: Mon, 29 Aug 2016 23:01:45 +0000 > From: <Gernot.Heiser(a)data61.csiro.au> > <snip> > You may *think* that the manufacturers don?t make changes to the more > conventional bits of the hardware, and thus they are ?correct", but that > isn?t true, of course. And on top of that we know that there are > intentional backdoors in commercial hardware. > The only way around this is high-assurance hardware, and this doesn?t come > at an affordable cost. > > I think it?s an illusion to think one can partition hardware into trusted > and untrusted bits. In the end, the OS is at the mercy of the hardware, if > it?s faulty then you lose, there?s no way around it. A key attraction of seL4 is the trustworthiness of the microkernel. Running it on hardware with known bugs or features (e.g. recent Intel CPUs) that compromise the kernel's trustworthiness counteracts the perceived advantages. Perhaps, it would be possible to list CPUs (and possibly boards) that are recognised for being free of known potential attack vectors. I would certainly not want to invest time and effort into making seL4 run on hardware that could have be reasonably known to be of low assurance.

2 1

IA32 syscall bindings
by Norman Feske 26 Aug '16

26 Aug '16

Dear seL4 developers, first, I'd like to thank you for publishing seL4 under GPL. I am very happy that I can finally get my hands dirty with working with the kernel of your group. :-) Currently, I am taking the first baby steps to bring the Genode OS framework (http://genode.org) to seL4. For reference, I am using the experimental branch. The first smallish issue I stumbled upon stems from the fact that Genode is written in C++. By compiling the seL4 syscall bindings with a C++ compiler, I got the following error: error: inconsistent operand constraints in an ‘asm’ It can be reproduced by putting the following code snippet into a cc file and compiling it with 'g++ -m32 -c' (tested with the Genode tool chain as well as with GCC 4.8.1): typedef enum { seL4_SysDebugPutChar = -9, _enum_pad_seL4_Syscall_ID = (1U << ((sizeof(int)*8) - 1)) } seL4_Syscall_ID; void seL4_DebugPutChar(char c) { asm volatile ( "pushl %%ebp \n" "movl %%esp, %%ecx \n" "leal 1f, %%edx \n" "1: \n" "sysenter \n" "popl %%ebp \n" : : "a" (seL4_SysDebugPutChar), "b" (c) : "%ecx", "%edx", "%esi", "%edi", "memory" ); } When compiling the same code snippet with 'gcc' instead of 'g++', everything is fine. It turns out that the C++ compiler does not like the enum value to be specified as input argument. I found the following ways to circumvent this problem: * Changing the enum value 'SysDebugPutChar' to a positive value, * Removing the definition of '_enum_pad_seL4_Syscall_ID', * Casting 'seL4_SysDebugPutChar' to an integer: : "a" ((int)seL4_SysDebugPutChar), In any case, I seem to have to change the bindings. Do you see a way around it? If not, would you consider one of the solutions above for the seL4 headers? On another note, I noticed that the bindings use the EBX register. Unfortunately, this makes it impossible to compile seL4 userland software as position-independent code (PIC). E.g., when compiling the above code snippet via 'g++ -m32 -fPIC -c', the following error occurs: error: inconsistent operand constraints in an ‘asm’ However, PIC is required in order to use shared libraries. The solution would be to not use EBX to pass arguments to the 'asm' statements, save EBX on the stack prior moving the respective kernel argument to the register, and, of course, restoring it after sysenter returns. Before I start changing the bindings, I'd like to know: is there anyone else working on the same problem? Would you be open to accept a change of the bindings to become PIC compliant on the costs of a few added instructions? Or do you have another suggestion how I should go about it? Best regards Norman -- Dr.-Ing. Norman Feske Genode Labs http://www.genode-labs.com · http://genode.org Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

4 7

syscalls and tlb
by Vasily A. Sartakov 26 Aug '16

26 Aug '16

Greetings. I am working on MIPS port of seL4. Now I can run very simple hello world application which reads and dumps bootinfo page. In other words, I modified elfloader, added platform and architecture support to the kernel, add _sel4_start for mips in libsel4platsupport, adopted mips support of libmuslc to work with __sysinfo in mips and more. Now I have some questions. I see that for different ‘syscalls' muslc uses different routes but with the same end. For example, SYS_ioctl from __stdout_write uses __syscall, provided by libmuslc/arch/<arch>/syscall_arch.h (implemented as CALL_SYSINFO). In the same time, syscall_cp function from __stdio_write is implemented inside libmuslc/src/internal/<arch>/syscall.s which uses __sysinfo in turn. So, that question is why? The second question is about the kernel. Now I am using static configuration of TLB in kerne: I have one region for rootserver aligned to 2MB, and one region for boot info page (also aligned). Thus, I do not have tlb traps since everything is in the TLB. In future, of course, I should add a processing of TLB misses somewhere in the plat/arch part of kernel. I am not familiar with memory support in seL4 yet, is there any syscall for delivery tlb traps? (I see nothing similar) Is there any check inside, for example, SEND call, about a presence of page in TLB? thank you. -- Vasily A. Sartakov sartakov(a)ksyslabs.org

4 5

Does anyone pay attention to Google's new operating system fuchsia
by XilongPei 24 Aug '16

24 Aug '16

Hi, Google has announced a new operating system fuchsia, https://github.com/fuchsia-mirror Its kernel is called Magenta, Magenta has a capability-based security model, this is very similar to seL4. Does anyone pay attention to Google's new operating system fuchsia? Xilong Pei Tongji University Shanghai, China 2016/8/24

3 3

x86: loosing edge triggered interrupts when using I/O APIC
by Alexander Boettcher 24 Aug '16

24 Aug '16

Hi, we are using as user level timer driver the PIT on Genode/seL4 and experience situations that the driver does not get IRQs after a while. It happens on Qemu as also on native x86 hardware. We tracked down the problem to the masking of edge-triggered IRQs on the I/O APIC in the seL4 kernel. According to Intel, [0] chapter 3.2.4 "Interrupt Mask R/W", edge interrupts on a masked interrupt pin gets ignored and are not held pending. On [2] there are also some discussion about this topic too. We solved/workaround the issue by this patch [1]. I looked additionally into two other microkernels using the I/O APIC and they don't mask edge level triggered I/O APIC interrupts. I wonder if anybody already stumbled about the issue on seL4/x86? If not, please take the patch or give advices to adapt the patch so that it may get upstream. Thanks, Alexander Boettcher. [0] http://www.intel.com/design/chipsets/datashts/29056601.pdf [1] https://github.com/genodelabs/genode/blob/master/repos/base-sel4/patches/io… [2] http://yarchive.net/comp/linux/edge_triggered_interrupts.html

2 1