- Devel - lists.sel4.systems

next seL4 developers day on Sep 6?
by Gerwin.Klein＠data61.csiro.au 16 Aug '16

16 Aug '16

We’re contemplating running a seL4 developers day in conjunction with the DARPA HACMS PI meeting in Pittsburgh on Tue, Sep 6 2016. If you would be interested in attending, please drop me a short email by Thursday night of your local time zone. If enough people register interest we will try to organise one. Cheers, Gerwin -- Prof Gerwin Klein, Research Group Leader, Trustworthy Systems DATA61 | CSIRO gerwin.klein(a)data61.csiro.au T +61 2 8306 0578 http://data61.csiro.au NICTA and CSIRO’s Digital Productivity business unit have joined forces to create the digital powerhouse Data61

1 0

Interrupt in seL4
by Norrathep Rattanavipanon 14 Aug '16

14 Aug '16

I have a few questions about how interrupts work in seL4. 1) Is it possible to enable/disable interrupt (i.e. __enable_irq or __disable_irq for ARM) in the userspace code of sel4? We want to make sure that the execution of the code in the initial process does not get interrupt. 2) My understanding is that the scheduling mechanism in seL4 is priority-based first and round-robin if two processes/threads have the same priority. Assume process A is the initial process spawned by kernel. 2.0) is my understanding about sel4 scheduling correct? 2.1) Is the initial process guaranteed to have the maximum priority in seL4? 2.2) If another process, say process B, is created by process A with lower priority. Is it possible for process B to interrupt process A and execute code in B instead while A is executing? Thanks, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

4 6

up-to-date formal verification
by Horace Blanc 09 Aug '16

09 Aug '16

Hi, I would like to know if the verification of the seL4 is up-to-date with the newest version of the sel4 microkernel (3.2.0). If so, how do I access it? When I run make ASpec in l4v, I get a pdf with the Abstract Formal Specification in version 1.3. Does it refer to the seL4 microkernel version 1.3 or has the Abstract Formal Specification its own versions? Also, what is the best way to explore this specification in Isabelle/jedit? thanks in advance Horace Blanc

2 1

on Zynq
by Neelesh Vemula 08 Aug '16

08 Aug '16

Hi all, I am completely new with seL4, embedded systems as well as the fpga world. I am working on installing seL4 on Zynq fpga and use it. I have successfully able to boot up a "hello world" application using uboot(sd card bootup) on the zynq device. However, I have no clue as in how to setup communication between the sel4 logic and the PL(fpga fabric). If I am correct some sort of device driver has to be written or is there anything that is inbuilt or someone else who has worked on a similar project. Any guidance in this regard will be utmost helpful. Thanks a ton! Neelesh Vemula

2 1

capDL configuration file
by Norrathep Rattanavipanon 03 Aug '16

03 Aug '16

So I was reading capDL paper and it mentions about having a human-readable XML file for configuration of the initial thread which allows the system initialize into a know state. I assume this is not specific to camkes. so is there any way I can see/get the XML file and the code that generates it in the regular seL4? Thanks, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

memory map/unmap performance
by Yuxin Ren 02 Aug '16

02 Aug '16

Hi all, I am curious memory mapping/unmapping performance. Are there any applications that stress the memory mapping and unmapping utility? Thanks a lot! Yuxin

4 4

beaglebone ethernet support
by Julien Delange 27 Jul '16

27 Jul '16

Hello, I noticed that there is some source code to support the ethernet driver of the beaglebone black. I look especially in projects/seL4_libs/libsel4platsupport/src/plat/am335x/cpsw_beaglebone.c According to https://github.com/seL4/seL4_libs/blob/master/libsel4platsupport/src/plat/a… the file has been introduced by NICTA - I am wondering if there is any existing example/support for it. In a nutshell, I am trying to use the ethernet driver. I started to integrate the startcode from TI on a camkes application before discovering this code. So, is there any sample application to use it? It is supported/working? Thanks for any help, Julien.

1 0

sel4 on Hikey board
by rahul mahadev 26 Jul '16

26 Jul '16

Hi , I'm trying to run sel4 on a hikey board, I'm following this wiki https://wiki.sel4.systems/Hardware/HiKey . I'm having issues as the link to the linaro-edk2 patch does not work(asks for some auth) , can someone provide another link or direct me . Thank you

2 1

Image lies outside of usable physical memory
by Alexander Boettcher 22 Jul '16

22 Jul '16

Hi, I want to boot seL4 (x86) 3.2.0 on a native machine (Lenovo X201) and I get a message like: End of loaded userland image lies outside of usable physical memory seL4 called fail at sel4/src/arch/x86/kernel/boot_sys.c: in function boot_sys, saying "boot_sys failed for some reason :( (Full log below attached) It seems that our used bootloader put the image to high in physical memory for seL4 (the other x86 kernels we use don't complain so far). Is this right that only memory below PPTR_TOP (0x1fc00000 on x86 3.2.0) can be used for the initial boot modules? Can this be changed or should we not try to touch this define (it seems to be derived from various other defines). Is there maybe a description about the required physical memory layout of the kernel and why it has to be as it is? Just in order to understand better the constraints we probably have to apply to our bootloader ;-) Thanks in advance, Alex. Parsing GRUB physical memory map Physical Memory Region from 0 size 89000 type 1 Physical Memory Region from 89000 size 17000 type 2 Physical Memory Region from d2000 size 2000 type 2 Physical Memory Region from dc000 size 24000 type 2 Physical Memory Region from 100000 size bb17c000 type 1 Adding physical memory region 0x100000-0x1fc00000 Physical Memory Region from bb27c000 size 6000 type 2 Physical Memory Region from bb282000 size dd000 type 1 Physical Memory Region from bb35f000 size 12000 type 2 Physical Memory Region from bb371000 size 81000 type 4 Physical Memory Region from bb3f2000 size 1d000 type 2 Physical Memory Region from bb40f000 size 60000 type 1 Physical Memory Region from bb46f000 size 1f9000 type 2 Physical Memory Region from bb668000 size 80000 type 4 Physical Memory Region from bb6e8000 size 27000 type 2 Physical Memory Region from bb70f000 size 8000 type 1 Physical Memory Region from bb717000 size 8000 type 2 Physical Memory Region from bb71f000 size 4c000 type 1 Physical Memory Region from bb76b000 size c000 type 4 Physical Memory Region from bb777000 size 3000 type 3 Physical Memory Region from bb77a000 size 7000 type 4 Physical Memory Region from bb781000 size 1000 type 3 Physical Memory Region from bb782000 size 9000 type 4 Physical Memory Region from bb78b000 size 1000 type 3 Physical Memory Region from bb78c000 size 13000 type 4 Physical Memory Region from bb79f000 size 60000 type 3 Physical Memory Region from bb7ff000 size 1000 type 1 Physical Memory Region from bb800000 size 800000 type 2 Physical Memory Region from bc000000 size 4000000 type 2 Physical Memory Region from e0000000 size 10000000 type 2 Physical Memory Region from feaff000 size 1000 type 2 Physical Memory Region from fec00000 size 10000 type 2 Physical Memory Region from fed00000 size 0 type 2 Physical Memory Region from fed1c000 size 4000 type 2 Physical Memory Region from fed20000 size 70000 type 2 Physical Memory Region from fee00000 size 1000 type 2 Physical Memory Region from ff000000 size 1000000 type 2 Physical Memory Region from 0 size 38000000 type 1 Kernel loaded to: start=0x100000 end=0x147000 size=0x47000 entry=0x10003e ACPI: RSDP paddr=0xf68e0 ACPI: RSDP vaddr=0xdfcf68e0 ACPI: RSDT paddr=0xbb7f07a2 ACPI: RSDT vaddr=0xdfff07a2 ACPI: DMAR paddr=0xbb781000 ACPI: DMAR vaddr=0xdff81000 ACPI: IOMMU host address width: 36 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0 ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x2 fun=0x0 ACPI: 3 IOMMUs detected ACPI: MADT paddr=0xbb7feb45 ACPI: MADT vaddr=0xdfffeb45 ACPI: MADT apic_addr=0xfee00000 ACPI: MADT flags=0x1 ACPI: MADT_APIC apic_id=0x0 ACPI: MADT_APIC apic_id=0x1 ACPI: MADT_APIC apic_id=0x4 ACPI: MADT_APIC apic_id=0x5 ACPI: MADT_IOAPIC ioapic_id=1 ioapic_addr=0xfec00000 gsib=0 ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0 ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd ACPI: 4 CPU(s) detected Detected 4 CPUs. Only just 1 Detected 1 boot module(s): module #0: start=0x7fc7a000 end=0x7ffff338 size=0x385338 name='/image.elf' ELF-loading userland images from boot modules: size=0x385000 v_entry=0x2000000 v_start=0x2000000 v_end=0x2385000 p_start=0x80000000 p_end=0x80385000

2 1

3.1.0 to 3.2.0 (x86) upgrade issue
by Alexander Boettcher 22 Jul '16

22 Jul '16

Hello, after upgrading the seL4 kernel (x86) from 3.1.0 to 3.2.0 we get for the very first invocation of seL4_X86_Page_Map an errorcode of *3* (seL4_IllegalOperation). We bisected the commits between 3.1.0 and 3.2.0 and [0] is the first bad commit for us. If we use the 3.2.0 release with [0] reverted on top than everything works as before - so no changes to Genode/seL4 as used for the 3.1.0 kernel are necessary. It's a know issue, or maybe something changed which must be adjusted in userland/roottask ? Thanks, Alex. [0] https://github.com/seL4/seL4/commit/c8819792d76ae5aecd89bcff656ca561e62959a5

2 2

Re: [seL4] [sel4utils question] stack size of the second process
by Kofidoku.Atuah＠data61.csiro.au 21 Jul '16

21 Jul '16

Hi, Our malloc currently uses mmap() for large allocations (and therefore the matching munmap() for freeing those large allocations). See https://github.com/seL4/musllibc/blob/sel4/src/malloc/malloc.c#L352. So while the mmap() call is implemented, the munmap() call is not, and this is why you're seeing this issue with "syscall 91" not being successful: https://github.com/seL4/musllibc/blob/sel4/arch/i386/bits/syscall.h#L92 https://github.com/seL4/musllibc/blob/sel4/arch/arm/bits/syscall.h#L67 ? Usually you allocate such a big chunk of memory for private use and management, so free() probably isn't a mission critical thing here (for the tutorials), unless there are factors I can't see -- let me know if this was helpful -- Kofi Doku Atuah Kernel engineer DATA61 | CSIRO E kofidoku.atuah(a)csiro.au www.data61.csiro.au CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61

1 0

[sel4utils question] stack size of the second process
by Norrathep Rattanavipanon 21 Jul '16

21 Jul '16

Hi, So I followed hello-4 example. I can create a static array inside a second process (hello-4-app) and the second process works fine. However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work. Any help would be appreciated. Thanks, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

1 1

Re: [seL4] [sel4utils question] stack size of the second process
by Kofidoku.Atuah＠data61.csiro.au 20 Jul '16

20 Jul '16

Hi, Thanks for popping by! The answer to the question in the subject line of your email (stack size of processes spawned by sel4utils_configure_process()) is that sel4utils_configure_process() calls sel4utils_configure_thread(), which allocates the stack using vspace_new_pages(), found here: (https://github.com/seL4/seL4_libs/blob/master/libsel4vspace/include/vspace/…) The stack size is determined by CONFIG_SEL4UTILS_STACK_SIZE, which can be set in your `make menuconfig` settings. Try: `make menuconfig` -> select "seL4 Libraries" -> "libsel4utils" and change the stack size as desired. That said, > However, when I try to increase the size of an array to 80,000 bytes, the second process wont start. I tried to increase ALLOCATOR_VIRTUAL_POOL_SIZE but it still does not work. Sorry, I'll need to know a bit more about what's going on here: could you post some more detailed output, or maybe a diff, so I can try to aid you? --Yours truly, Kofi

1 0

Cortex-M port?
by Stefan Wallentowitz 18 Jul '16

18 Jul '16

Hi, I was wondering if anyone ever started a port to a v7-M platform? Cheers, Stefan

2 1

3.2.0 release issues?
by Jeff Waugh 18 Jul '16

18 Jul '16

Hey there, I noticed the wiki "latest" links now point to 3.2.0. I haven't seen an announcement for 3.2.0 yet, so perhaps this is all a matter of staging, but the current sel4test manifest points to 3.2.x-compatible tags that don't exist in most of the repos. Just thought I'd mention it as I imagine it's the primary way people acquire new releases. Thanks, Jeff

2 4

RELEASE: seL4 3.2.0 release
by Parthasarathi Susarla 18 Jul '16

18 Jul '16

We are pleased to announce the release of 3.2.0 of seL4. This release contains the following changes: * ARM Hypervisor support. * ARM Jetson-TK1: Cleanup. * Benchmarking now supports tracking of syscalls. * Support for XSAVE feature set for x86 CPUs. * Simplified ARM platform selection during configuration. = ABI Changes = * seL4_BootInfo has a new entry for IOSpace caps for ARM SMMU. The release tarballs can be directly downloaded from: https://github.com/seL4/seL4/archive/3.2.0.tar.gz 7210ecc65f0f8a04490605e92f7b89b4 3.2.0.tar.gz The manual for this release can be downloaded here: http://sel4.systems/Info/Docs/seL4-manual-3.2.0.pdf 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 <parthasarathi.susarla(a)nicta.com.au> ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

verification requirements
by Gergely Buday 13 Jul '16

13 Jul '16

Hi, what are the requirements for running the whole sel4 verification proof? Is 32G RAM and 20G disk space enough? How about the processor needs? I guess what is enough in batch mode will be enough for interactive development. - Gergely

2 1

Frame buffer
by Rinat Dobrokhotov 09 Jul '16

09 Jul '16

Hello, Could you tell me if framebuffer is released for seL4? -- Best Regards, Rinat Dobrokhotov

6 7

[sel4] persistent storage / file system
by rahul mahadev 06 Jul '16

06 Jul '16

Hi, I wanted to know if persistent storage/ file system have been tried on sel4 before ,if so can I have more details on it. Regards , Rahul S Mahadev

5 5

Capabilities of binary images
by Norrathep Rattanavipanon 06 Jul '16

06 Jul '16

Hi, I need to access the user image from a user application for verifying that the binary is installed correctly. So I found in bootinfo.h that it contains userImageFrames and its supposed to be the one I'm looking for but it gave me an error when I map the frames via vspace_map_pages(vspace, info->userImageFrames.start, ...) at the root task. The error is : ERROR:sel4utils_map_page_pd:223: Error mapping pages, bailing: 2 What am I doing wrong here? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 2

Get real time clock data (and timer) from I.MX6
by Norrathep Rattanavipanon 30 Jun '16

30 Jun '16

Hi, I was wondering if there's any real time clock implementation for I.MX6 in sel4. And if there isnt any, what would be the best way to use a timer in sel4 (since I saw many implementations of those)? through sel4platsupport_get_default_timer? Best, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 5

ARM Hypervisor extensions in master
by Adrian Danis 28 Jun '16

28 Jun '16

The ARM hypervisor extensions are now supported in the master seL4 kernel. This support has existed on a public development branch (arm_hyp) for some time, but this marks the beginning of proper support and a verification target. What is done: * Hypervisor extensions supported on odroid-xu and Jetson TK1 platforms * SystemMMU supported on Jetson TK1 platform Limitations: * Currently any usage of hyp extensions or SystemMMU is *not* verified * SystemMMU contains work around currently for the VMM to map in large amounts of memory (fix for this relies on a kernel change currently being verified) You can use the manifest https://github.com/seL4proj/camkes-arm-vm-manifest to get the project https://github.com/seL4proj/camkes-arm-vm and then use one of the two default configs for the TK1 and odroid-xu platforms. Adrian ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

camkes-VM with QEMU and virutal PCI device
by Samuel Weiser 28 Jun '16

28 Jun '16

Hi again, I'm playing around with camkes-vm in QEMU+KVM. I want to add a virtual PCI device to Linux, which is running as vm0 on top of seL4. However, I got stuck with some errors during system boot. My setup is as follows: QEMU is configured to share a 1MB memory region between the host and the QEMU guest (seL4). Here's what QEMU sets up: (qemu): info mtree ... 00000000fe000000-00000000fe0fffff (prio 1, RW): ivshmem-bar2-container 00000000fe000000-00000000fe0fffff (prio 0, RW): ivshmem.bar2 00000000febf1000-00000000febf10ff (prio 1, RW): ivshmem-mmio ... (qemu): info pci ... Bus 0, device 4, function 0: RAM controller: PCI device 1af4:1110 IRQ 11. BAR0: 32 bit memory at 0xfebf1000 [0xfebf10ff]. BAR2: 64 bit prefetchable memory at 0xfe000000 [0xfe0fffff]. id "" ... I adapted a previously working configuration (optiplex9020.camkes) accordingly with what I thought should be correct. Especially, I added vm0_config.pci_devices_iospace and vm0_config.pci_devices as well as the PCI irq. Here's the configuration: configuration { VM_CONFIGURATION_DEF() VM_PER_VM_CONFIG_DEF(0, 2) vm0.simple_untyped24_pool = 12; vm0.heap_size = 0; vm0.guest_ram_mb = 1536; vm0.kernel_cmdline = VM_GUEST_CMDLINE; vm0.kernel_image = C162_KERNEL_IMAGE; vm0.kernel_relocs = C162_KERNEL_IMAGE; vm0.initrd_image = C162_ROOTFS; vm0.iospace_domain = 0x00; vm0_config.ram = [ [ 0x20800000, 23 ], [ 0x21000000, 24 ], [ 0x22000000, 25 ], [ 0x24000000, 26], [ 0x28000000, 27], [0x30000000, 28], [0x40000000, 29] , [0x60000000, 30], [0xa0000000, 28]]; vm0_config.ioports = [ {"start":0x2f8, "end":0x2ff, "pci_device":0, "name":"COM2 Serial Port"}, {"start":0x2e8, "end":0x2ef, "pci_device":0, "name":"COM4 Serial Port"} ]; vm0_config.irqs = [ {"name":"Serial", "source":3, "level_trig":0, "active_low":0, "dest":3}, {"name":"PCI", "source":11, "level_trig":1, "active_low":1, "dest":11} ]; vm0_config.pci_devices_iospace = 1; vm0_config.pci_devices = [ {"name":"PCI", "bus":0, "dev":0x04, "fun":0, "irq":"PCI", "memory":[ {"paddr":0xfe000000, "size":0x100000, "page_bits":12}, ], }, ]; } However, after creating the MMIO frames and doing some other stuff, the boot process fails, as shown below. The error also occurs if I change or completely remove just the "memory" definition of my PCI device. I also tried different values for "iospace_domain" (QEMU should use 0 as default PCI domain). Thanks in advance for any hints and ideas! Best, Sammey Starting Loader... Parsing bootinfo... 1041793 free cap slots, from 6783 to 1048576 Untyped memory (24) 0x0000000000100000 - 0x0000000000108000 0x0000000000108000 - 0x0000000000109000 0x0000000003000000 - 0x0000000004000000 0x0000000004000000 - 0x0000000008000000 0x0000000008000000 - 0x0000000010000000 0x0000000010000000 - 0x0000000018000000 0x0000000018000000 - 0x000000001c000000 0x000000001c000000 - 0x000000001e000000 0x000000001e000000 - 0x000000001f000000 0x000000001f000000 - 0x000000001f800000 0x000000001f800000 - 0x000000001fc00000 0x0000000001b6b000 - 0x0000000001b6c000 0x0000000001b6c000 - 0x0000000001b70000 0x0000000001b70000 - 0x0000000001b80000 0x0000000001b80000 - 0x0000000001c00000 0x0000000001c00000 - 0x0000000001e00000 0x0000000001e00000 - 0x0000000001f00000 0x0000000001f00000 - 0x0000000001f80000 0x0000000001f80000 - 0x0000000001fc0000 0x0000000001fc0000 - 0x0000000001fe0000 0x0000000001fe0000 - 0x0000000001ff0000 0x0000000001ff0000 - 0x0000000001ff2000 0x0000000001ff2000 - 0x0000000001ff3000 0x0000000001ff3000 - 0x0000000001ff3800 Loader is running in domain 0 Device untyped memory (30) 0x0000000000001000 - 0x0000000000002000 0x0000000000002000 - 0x0000000000004000 0x0000000000004000 - 0x0000000000008000 0x0000000000008000 - 0x0000000000010000 0x0000000000010000 - 0x0000000000020000 0x0000000000020000 - 0x0000000000040000 0x0000000000040000 - 0x0000000000080000 0x0000000000080000 - 0x0000000000100000 0x000000001fc00000 - 0x0000000020000000 0x0000000020001000 - 0x0000000020002000 0x0000000020002000 - 0x0000000020004000 0x0000000020004000 - 0x0000000020008000 0x0000000020008000 - 0x0000000020010000 0x0000000020010000 - 0x0000000020020000 0x0000000020020000 - 0x0000000020040000 0x0000000020040000 - 0x0000000020080000 0x0000000020080000 - 0x0000000020100000 0x0000000020100000 - 0x0000000020200000 0x0000000020200000 - 0x0000000020400000 0x0000000020400000 - 0x0000000020800000 0x0000000020800000 - 0x0000000021000000 0x0000000021000000 - 0x0000000022000000 0x0000000022000000 - 0x0000000024000000 0x0000000024000000 - 0x0000000028000000 0x0000000028000000 - 0x0000000030000000 0x0000000030000000 - 0x0000000040000000 0x0000000040000000 - 0x0000000060000000 0x0000000060000000 - 0x00000000a0000000 0x00000000a0000000 - 0x00000000e0000000 0x00000000e0000000 - 0x0000000000000000 Sorting untypeds... Untyped 0 (cptr=1a39) is of size 15. Placing in slot 17... Untyped 1 (cptr=1a3a) is of size 12. Placing in slot 20... Untyped 2 (cptr=1a3b) is of size 24. Placing in slot 5... Untyped 3 (cptr=1a3c) is of size 26. Placing in slot 2... Untyped 4 (cptr=1a3d) is of size 27. Placing in slot 0... Untyped 5 (cptr=1a3e) is of size 27. Placing in slot 1... Untyped 6 (cptr=1a3f) is of size 26. Placing in slot 3... Untyped 7 (cptr=1a40) is of size 25. Placing in slot 4... Untyped 8 (cptr=1a41) is of size 24. Placing in slot 6... Untyped 9 (cptr=1a42) is of size 23. Placing in slot 7... Untyped 10 (cptr=1a43) is of size 22. Placing in slot 8... Untyped 11 (cptr=1a44) is of size 12. Placing in slot 21... Untyped 12 (cptr=1a45) is of size 14. Placing in slot 18... Untyped 13 (cptr=1a46) is of size 16. Placing in slot 15... Untyped 14 (cptr=1a47) is of size 19. Placing in slot 11... Untyped 15 (cptr=1a48) is of size 21. Placing in slot 9... Untyped 16 (cptr=1a49) is of size 20. Placing in slot 10... Untyped 17 (cptr=1a4a) is of size 19. Placing in slot 12... Untyped 18 (cptr=1a4b) is of size 18. Placing in slot 13... Untyped 19 (cptr=1a4c) is of size 17. Placing in slot 14... Untyped 20 (cptr=1a4d) is of size 16. Placing in slot 16... Untyped 21 (cptr=1a4e) is of size 13. Placing in slot 19... Untyped 22 (cptr=1a4f) is of size 12. Placing in slot 22... Untyped 23 (cptr=1a50) is of size 11. Placing in slot 23... Creating objects... ... Creating object conn1_mmio_frame_4261412864 in slot 6808, from untyped 1a3c... device frame, paddr = 0xfe000000, size = 12 bits Creating object conn1_mmio_frame_4261416960 in slot 6809, from untyped 1a3c... device frame, paddr = 0xfe001000, size = 12 bits Creating object conn1_mmio_frame_4261421056 in slot 6810, from untyped 1a3c... device frame, paddr = 0xfe002000, size = 12 bits ... Creating object vm_vm0_pre_init_ep in slot 10275, from untyped 1a3c... Creating object conn1_iospace_32 in slot 10276, from untyped 1a3c... <=== This is ignored! Creating object conn4_iport_760_767 in slot 10276, from untyped 1a3c... ... Populating slot 21 with cap to conn1_iospace_32... minting (with badge/guard 0x20)... <<seL4 [decodeCNodeInvocation/107 T0xe1ff3900 "rootserver" @804a911]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.>> capDL-loader :: << Error: init_cnode_slot:1689: seL4_FailedLookup >>

2 1

Autocorres Error.
by Dan DaCosta 24 Jun '16

24 Jun '16

seL4 Developers: I apologize in advance if this is not the correct place for this email. I am experimenting with Autocorres as an intern at Rockwell Collin's Advanced Technology Center in Minnesota. My latest experiment is in building a small verified library for manipulation and analysis of adjacency lists. My initial work towards this end generated the following error: exception CTERM raised (line 948 of "~/development/rockwellcollins/verification/l4v/tools/autocorres/utils.ML"): autocorres: Internal var uu_::"int" is exposed. Please notify the AutoCorres maintainers of this failure. In the meantime, use "autocorres [keep_going]" to ignore the failure. I am using the latest version of Autocorres and Isabelle. The c and theory file that generated this error can be found here: https://github.com/chaosape/autocorresexperiments/tree/master/graph Thanks! Dan DaCosta

3 3

Resolving issue using camkes-vm with qemu
by Samuel Weiser 20 Jun '16

20 Jun '16

Hi, I just want to share some information which I needed to run camkes-vm with qemu, especially addressing one issue which prevented the guest vm to boot. I basically follow the recommendations of Adrian in [1] and only focus on the simple case without vt-d. 1. use the 'optiplex9020_onevm' configuration as it basically just specifies physical RAM. 2. enable nested KVM [2,3] 3. run QEMU with enough RAM: qemu-system-i386 -nographic \ -m 3GB \ -enable-kvm \ -cpu host \ -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-experimental-image-ia32-pc99 Following the above steps gives you a booting camkes vmm, however it fails to eventually activate Intel vt-x, needed to run the guest vm. The reason for that is that the seL4 kernel requires the IA32_FEATURE_CONTROL MSR to have VMXON enabled (bit 2) and locked (bit 0) (i.e. a value of 5). Normally, it's the job of the BIOS to do so, however I couldn't find an appropriate QEMU BIOS ROM which does so. The quick workaround is to enable VMXON within the seL4 kernel itself. The corresponding diff is attached. With this minor change, the recompiled kernel works like a charm. PS: One could consider making a separate option in Kconfig for that purpose. Best, Sammey [1] https://sel4.systems/pipermail/devel/2016-March/000717.html [2] http://www.rdoxenham.com/?p=275 [3] https://wiki.archlinux.org/index.php/QEMU#Enabling_KVM

2 1

Rust application support
by Kent.Mcleod＠data61.csiro.au 20 Jun '16

20 Jun '16

Using rust (https://www.rust-lang.org) in user applications on top of seL4 with existing C libaries and apps now has limited support. See here for more information: https://wiki.sel4.systems/Rust What you can do: + Build system support for using a rust cargo project as a library or app on seL4 + Use most core libraries (core, alloc, collections, rustc_unicode, and a limited std) + Use rust dependencies from crates.io on seL4 + Use rust to implement camkes components + Using rust's FFI support it is possible to call rust from C and C from rust. Two sample apps are located here: https://github.com/SEL4PROJ/rust-camkes-samples Instructions for building and running are on the wiki page. Has been tested on x86 i386 and arm kzm both in qemu and hardware. Caveats: + Rust's libstd functionality is limited by which muslc syscalls are supported on seL4. + Rust's libstd requires muslc thread local storage support which is not currently available on seL4. We currently use a muslc branch called rust that uses a global TLS struct. Kent McLeod Kernel engineer / Thesis Student DATA61 | CSIRO

1 0

WIll seL4 support any Unikernel
by XilongPei 16 Jun '16

16 Jun '16

Hi, According to wikipedia.org, Unikernels are specialised, single address space machine images constructed by using library operating systems. A developer selects, from a modular stack, the minimal set of libraries which correspond to the OS constructs required for their application to run. These libraries are then compiled with the application and configuration code to build sealed, fixed-purpose images (unikernels) which run directly on a hypervisor or hardware without an intervening OS such as Linux or Windows. Will seL4 support any unikernel, such as Drawbridge or MirageOS, in the future? Xilong Pei Tongji University Shanghai, China 2016/6/13

3 2

Beaglebone black/CAmkES issue
by Julien Delange 16 Jun '16

16 Jun '16

I am using the second serial interface of the beaglebone black. According to the source code (in libsel4platsupport/plat_include/am335x/sel4platsupport/plat/hw/soc_AM335x.h), the address is 0x48022000). The following line is found in the source #define SOC_UART_1_REGS (0x48022000) So, in CAmkES, I configure the hardware component that represents the serial hardware component with the following attributes: drv.mem_attributes = "0x48022000:0x1000"; The application compiles fine. However, when launching the image on the target, I have the following issue. Any idea about how to solve this? Does anybody successfully used UART1 on the beaglebone black? Or have any idea/suggestion to investigate? Thanks. Julien. Creating object conn1_frame__timer_0 in slot 728, from untyped 29b... device frame, paddr = 0x48040000, size = 12 bits Creating object conn2_frame__Cons_PingMe_0 in slot 729, from untyped 29b... device frame, paddr = 0x48022000, size = 12 bits capDL-loader :: << Error: Failed to find device frame at paddr = 0x48022000 >> Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid sys_tkill assuming self kill

4 8

Tidying and real-time
by Jeff Waugh 16 Jun '16

16 Jun '16

This commit… https://github.com/seL4/seL4/commit/c5b6a6a58aae75129cdf5a83f861bdacddbf51d6 … is pleasing. As is the RT API. Passive servers! A seemingly viable and sensible approach to user-space scheduling! Just a quick thumbs up for recent progress. :-)

1 0

CAmkES parsing issue
by Julien Delange 11 Jun '16

11 Jun '16

Hi, I am trying to build a camked application with a UART driver. When trying to build the application, I got the following error: While rendering uart_mem.from.source: 'drv' However, the component is well define. How can I try to get more information/debug of the camkes assembly and find out what is wrong? Thanks! Note: the project can be found there: https://drive.google.com/file/d/0Bxl72qH3r6BjRGxYSXd2LUllcDQ/view?usp=shari…

3 6

camkes arm vm I/0 devices
by Josh Tuttle 08 Jun '16

08 Jun '16

Hey, We have been playing around with the busybox for tk1 that was included in the build. While trying to verify all the I/0 devices, we noticed that the Ethernet device would not come up. Looking though dmesg, it seems to load a driver but never initializes a device. Ifconfig just errors when trying to bring up eth0. Has anyone verified the I/0 devices on tk1 using this build? Not being familiar with busybox, can we follow this: http://elinux.org/Jetson/Busybox_RootFS guide to building a busybox image to include all appropriate drivers? Thanks, Josh

2 1

seL4 benchmarks available
by Anna Lyons 07 Jun '16

07 Jun '16

Hi all, I've just finished pushing the seL4 benchmarking suite out to github. Get it: * manifest: https://github.com/seL4/sel4bench-manifest * explore the applications: https://github.com/seL4/sel4bench. Cheers, -- Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons(a)nicta.com.au<mailto:anna.lyons@nicta.com.au> www.data61.csiro.au<http://www.data61.csiro.au> CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

Unable to build camkes-vm
by Samuel Weiser 07 Jun '16

07 Jun '16

Hello, didn't manage to build camkes-vm. Is there any working setup available or did I make something wrong? 1.) I tried to build c162_twovm_defconfig with the "default.xml" manifest 1a.) I get compile errors regarding some definitions of seL4_X86.... It seems that seL4_libs (March 2016) are inconsistent with the kernel version (Dec 2015). Updating to a newer kernel, i.e. 3.1.0 solves this issue but creates new ones: 1b.) The bootinfo struct is too big to fit one page. I get the error: compile_assert(bi_size, sizeof(seL4_BootInfo) <= BIT(BI_FRAME_SIZE_BITS)) So I reduced the max. no of bootinfo untyped caps from 800 to 167 1c.) Error: No rule to make target 'libsel4simple-default', needed by 'libsel4platsupport-y' Since the kernel is not stable, it falls back to default but does not manage to correctly reference the default lib. First, I added the missing symlink in libs. Then, I added the default lib to the main Kconfig and the apps/c162_twovm/Kbuild. 1d.) The next error is: x86/pc99/include/vmm/guest_state.h:60:44: error: unknown type name ‘seL4_VCPUContext’ ... 2.) I also tried building with the "working.xml" manifest, which already failed to fetch the correct revisions 2a.) In the working.xml, I fixed the seL4_libs upstream to 'master' Also, the kernel revision is broken, seL4.git points to an experimental commit, which couldn't be fetched. I changed it to kernel 3.1.0. 2b.) The same error as in 1d) appears. This is where I gave up. Any hints? Thanks in advance, Sammey

2 1

VM on SeL4 for TK1
by Joshua Tuttle 06 Jun '16

06 Jun '16

Hi, I am working with Peng Xie to run the vm for tk1 code that Adrian gave out a couple of days ago, located at https://github.com/seL4proj/camkes-arm-vm-manifest. We have successfully been able to build and run on our tk1 board, but are met with a buildroot login prompt. What is the username and password, we should be using? Also, is this a para-virtualized or fully-virtualized environment? Thanks, Josh Tuttle Research Engineer Intelligent Automation, Inc. 15400 Calhoun Dr., Suite 109 Rockville, MD 20855 Ph: (301) 795-2706 jtuttle(a)i-a-i.com<mailto:jtuttle@i-a-i.com> ________________________________ This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.

2 1

Latest experimental RT kernel released
by Anna Lyons 03 Jun '16

03 Jun '16

= Latest experimental RT kernel released = The RT kernel provides + periodic scheduling, + temporal isolation, + support for criticality and criticality mode changes, + temporal exceptions, .. and more. == Caveats == The RT kernel does not compile or run on all platforms, we currently support: + x86: ia32 platforms with TSC_DEADLINE mode + ARM: Sabre lite, Beagle board, and Odroid-xu (all armv7-a). The RT kernel is not verified, and as such we provide no guarantees, and there's likely still some bugs hiding in there. The other platforms require driver work at user level and in the kernel. If you are keen to get a certain platform working, contributions are welcome! == Available == + *Kernel branch* on github: https://github.com/seL4/seL4/tree/rt + *Release notes* (detailed API changes from current seL4 latest release): https://wiki.sel4.systems/seL4%201.0.0-rt-dev + *RT kernel manual* http://sel4.systems/Info/Docs/seL4-manual-1.0.0-rt-dev.pdf + *whitepaper* http://arxiv.org/abs/1606.00111 == Try it == Check out the rt branch of sel4test-manifest with repo: $ repo init -u https://github.com/seL4/sel4test-manifest.git -b rt Feedback on the API would be *extremely* valued. Enjoy! -- Anna Lyons Kernel engineer / PhD Student DATA61 | CSIRO E anna.lyons(a)nicta.com.au<mailto:anna.lyons@nicta.com.au> www.data61.csiro.au<http://www.data61.csiro.au> CSIRO's Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

3 3

Memory allocation & threads
by Доброхотов Ринат 03 Jun '16

03 Jun '16

Hello, I don't understand how static and virtual pool's size related to thread's available working space. I got the example app from the sel4-tutorials project with process creation (app-4). A static pool and a virtual pool are created in this app. I have done experiments with size of this pools and size of arrays in the second thread. For example I set size of virtual pool to zero, as I understand this pool need to create kernel objects. Also I define the test array size of (1 << 23)~8,3Mb. If test array is static, static pool size must be equal to ((1 << seL4_PageBits) * 100) ~0,4Mb. If test array is no static, static pool size not limited. Why is it so? -- Best Regards, Rinat Dobrokhotov

4 4

Will the codes in branch rt be merged into master
by XilongPei 02 Jun '16

02 Jun '16

Hi, I got information from https://wiki.sel4.systems/seL4%201.0.0-rt-dev , the development branch for the seL4 realtime extensions. My question is that will the codes in branch rt be merged into master, and add some build option. If a working tree always not in the master branch, it will be very difficult to be managed. Xilong Pei Tongji University 2016/6/1

2 1

RT branch questions
by Julien Delange 27 May '16

27 May '16

I am currently trying the RT branch and have some questions: 1. What emulator to use in order to try the examples? I am trying to use x86 with qemu but it seems that it does not work. I got the following trace at execution Starting node #0 APIC: unsupported platform, TSC-deadline mode is not supported seL4 called fail at /home/sel4/camkes-sc-tests/kernel/src/arch/x86/kernel/boot_sys.c:451 in function boot_sys, saying "boot_sys failed for some reason :( So, is there an emulator (for any supported platform) to try it? 2. In the RT-camkes extensions, I have the following new attributes: _period _budget _priority What is the semantics of these attributes? Any information about them? How they are supposed to be isolated from each other then? How to define the scheduling plan for the system then? Also, how these attributes apply to all thread: a thread is created for each interface of the component, so, how can we then define the priority/budget of each thread? Do these attributes apply to all the components of the thread? Thanks for any help/clarification. Julien. assembly { composition { component Client client1; component Client client2; } configuration { client1._priority = 100; client1._period = 10000; client1._budget = 7500; client2._priority = 50; client2._period = 10000; client2._budget = 7500; } }

3 6

Advice on camkes and regular seL4 for driver components
by Norrathep Rattanavipanon 27 May '16

27 May '16

Hello, I currently had codes, implemented as regular seL4, since camkes does not support some features (i.e. transferring capabilities or accessing address space outside the process), Everything is fine up to this point but now I want to create several drivers. And I found that the best and easiest way to do that is to use camkes. So is it possible to use existing regular codes in conjunction with camkes? Or would the best way be to implement drivers as regular seL4 codes? Thanks, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

building VMM on Jetson TK1 board
by PX 26 May '16

26 May '16

Hi, all we want to build the seL4-based VMM from https://github.com/smaccm/sel4arm-vmm.git on Jetson TK1 board. However, the seL4 kernel in that project does not support TK1 board. We want to use the new version seL4 version (arm_hyp) at https://github.com/seL4/seL4.git. My questions are: 1) It is feasible to do that? 2) If so, what are the correct steps to do that? 3) we try to compile these source code, but failed. We do the following modifications: A) we add TK1 source codes (i.e. TK1 folders from https://github.com/seL4/seL4.git) to the corresponding libraries in the VMM source code from https://github.com/smaccm/sel4arm-vmm.git; and B) we add relevant config definitions to the VMM code. Currently, we can successfully compile the seL4 kernel code, but have trouble to compile the VMM libraries. Do we miss something here? thanks Peng

2 1

Availability of RT branch?
by Julien Delange 25 May '16

25 May '16

Hi all, Follow-up on our recent discussions on the RT branch: is the RT branch now available? How could I get it and access the related documentation? If not available, is there any idea of when it will be available? Thanks. Julien.

1 0

Getting timer info from seL4 kernel
by Will Klieber 19 May '16

19 May '16

Hi, Is there any way of obtaining the number of elapsed timer ticks from the seL4 kernel (using ARM / BeagleBoard platform)? I know the kernel uses this information internally for the scheduler, but I couldn't find any way of accessing it from userland. Specifically, my usage scenario is as follows. Two mutually distrustful programs are running, and each wants to run an action periodically. We want to temporally isolate the two programs using seL4 time domains. In this case, interacting with the hardware timer in userland seems difficult, since we want to get the updated time whenever a new timer tick arrives, but the userland device driver for the timer can only operate in exactly one of the seL4 time domains. Please let me know if I am misunderstanding something or if there might be a better way to approach this situation. Thanks, Will

5 6

Hello. I'm Kihyun-seo in South Korea.
by 서기현 17 May '16

17 May '16

Hello, I am a student of the Hanseo University in Korea. I want to create a UAV(drone) that uses Odroid XU4 Odroid XU4's Detailed Specifications = http://www.hardkernel.com/main/products/prdt_info.php?g_code=G143452239825 I want to install seL4 on the board for the security of the drones. The board has “ubuntu-15.04-robotics-odroid-xu4-201” 32bit linux version. I have two questions. First, I understood that after installing the seL4 first, and installing the linux later after seeing the 1.jpg. However, in the “https://wiki.sel4.systems/Getting%20started”. “Setting up your machine - These instructions are for Ubuntu. They assume you already know the basics of using the command line, compilers and GNU Make.” So then, Should I install the Linux(ubuntu) first, and install the seL4 later? I wonder what is correct. and I need more detailed explanation. Second, An error occurred during install the seL4 like 2.jpg. (command = "make menuconfig" in "Build ia32" part.) I need a solution about the error. Please answer my two questions.

3 2

multi-core support
by PX 17 May '16

17 May '16

Hi, Just want to double check if the seL4 under link https://github.com/seL4/sel4test supports multi-core? If so, the multi-core support is configured by default? If the sel4 does not support multi core, where can we get the experimental version supporting multi core? thanks Peng

2 1

Trusted Execution Environment on seL4
by rahul mahadev 11 May '16

11 May '16

Hi, I am Rahul Mahadev, I'm currently working on a Google Summer Of Code project with the organization lowRISC. My project is to implement a Trusted Execution Environment for the RISC-V platform. Last year's gsoc had a port of sel4 for RISC-V platform by Hesham Almatery. I plan on using seL4 for the port by either of the two methods. 1. paravirtualize OPTEE(Linaro's TEE) on top of seL4 2. implement an API similar to OPTEE for seL4 I have written a blog post explaining this, I wanted your opinion + ideas regarding this. link: http://mahadevrahul.blogspot.in/2016/05/gsoc-2016-implementing-trusted.html Thank You, Rahul Mahadev

2 1

Is the L4-embedded microkernel here means seL4
by XilongPei 20 Apr '16

20 Apr '16

Dear all, The web page http://ssrg.nicta.com.au/about/#achievements says: !$ All recent Apple iOS devices ship with a <http://www.apple.com/business/docs/iOS_Security_Guide.pdf> security processor controlled by a fork of our L4-embedded microkernel; I wonder whether the L4-embedded microkernel means seL4. thanks Xilong Pei Tongji University 2016/4/14

4 5

Problem porting sel4 into XU4
by Norrathep Rattanavipanon 19 Apr '16

19 Apr '16

Hi, I'm trying to port sel4 into ODROID-XU4 by following the wiki ( https://wiki.sel4.systems/Hardware/odriod-XU) So far I can successfully enable HYP mode as indicated by [ 0.198398] [c0] CPU: All CPU(s) started in HYP mode. [ 0.198433] [c0] CPU: Virtualization extensions available. as well as generate sel4test-driver-image-arm-exynos5 image. However, we cant do fastboot in XU4 since it doesnt have usb otg. Thus, I followed booting from sd card from https://wiki.sel4.systems/Hardware/General-ARM and copied the image into the first partition of sd card and do the following: Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5 Exynos5422 # bootelf 0x48000000 and here's the output: ## 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..4126401f] ELF-loading image 'kernel' paddr=[40000000..4002dfff] vaddr=[e0000000..e002dfff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[4002e000..40388fff] vaddr=[8000..362fff] virt_entry=13868 Enabling hypervisor MMU and paging Enabling MMU and paging Jumping to kernel-image entry point... �⧹I�AIq9Fy6 1)�a&I99)�6� Yq��摦P�^б��F��^/A�yyyyyyyyy�Y �)aay��XY�ǡyQ)�q��O�a@ Ia)!Fyaay �)��XY��.6I�)&FvF�6fF��VƑ�y��P�)aay��XY�ǡyQ)�q��O�a@ Ia Is it expected? or am I doing something wrong? Any help would be appreciated. Best, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

3 6

building VMM on multi-core seL4
by PX 14 Apr '16

14 Apr '16

Dear all, I have some questions about building VMM on top of seL4. I know there is a sel4-based VMM on github (https://github.com/smaccm/sel4arm-vmm-manifest) Gernot also told me that this version of VMM does not support multi core. My questions are: 1) Can this single core version of VMM be run on top of multi-core sel4 just using one core without modification? 2) If not, what supports are missed in the multi-core version of sel4? I assume single-core version applications should be compatible with multi-core micro kernel. 3) If my assumption is wrong, what do we (as VMM developer) need to add to the VMM code to make it workable on the multi-core seL4? thanks Peng

2 1

Re: [seL4] [seL4/seL4] Real performance comparisons (#21)
by Gernot Heiser 11 Apr '16

11 Apr '16

On 11 Apr 2016, at 8:09 , fresheneesz <notifications(a)github.com<mailto:notifications@github.com>> wrote: I imagine this isn't the right place for this, but i can't find a better one. The correct one is this (devel(a)sel4.systems<mailto:devel@sel4.systems>) I see the performance comparisons at http://l4hq.org/docs/performance.php are run on all different processors. In its current form, the performance numbers here are completely useless. It would be very informative to have real performance benchmarks where the exact same processor is used for every OS in comparison. Otherwise, what am I supposed to do with those number? You’re right that comparisons across different processors are of limited power, but they aren’t useless either, especially when expressed in cycles (and ideally coupled with an understanding of the underlying hardware, eg the insane pipeline depth and speculation of the Pentium 4). However, given that these are different implementations spanning 20 years (some written in assembler), it isn’t possible to run them on the same hardware. The key observation is that no-one has ever done better on any of those processors. Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

i have some questions about domain and thread
by 김은영 04 Apr '16

04 Apr '16

Hi, all first, I do not speak English well. please answer to me easily. i'm studying seL4 kernel source code. i have some questions. 1. What is domain? i read manual but i don't understand well. I hope that you explain to me in detail about the domain. 2. What is the maximum number of threads that can be created in one domain? 3. Usually there is a function to create a new thread in kernel source code. but i can't find the function in seL4 kernel source code. What is the way to create a new user thread in seL4? also, what is the way to exit user thread in seL4? thanks.

2 1

Questions about Kernel Memory Mapping
by Daniel Wang 01 Apr '16

01 Apr '16

Hi all, I’m trying to understand the seL4 kernel source code. I think the memory mapping between physical memory and virtual memory is a key point since it is directly related to how kernel functions and manage badges. I noticed that the kernel turns on the paging very early. Can someone help me or point out some resources how kernel memory is allocated? Especially how during and after the booting what the kernel memory snapshot looks like and things like that. For example, I traced to map_kernel_window() function and even before that there is some pptr to paddr conversion. I would really appreciate the help. Thanks -Dan

3 2

seL4 Documentation/Tutoria
by xurongfeik 31 Mar '16

31 Mar '16

Hi folks Is there any Documentation/Tutorial about execution time for typical invocations of the seL4 system calls? Thanks! -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

2 1

sel4 build tutorial
by Jorge Alberto Garcia 31 Mar '16

31 Mar '16

Hi folks Is there any Documentation/Tutorial about how to do a build to start testing seL4 ? where can I find the current boards/architectures supported? Thanks!

2 2

Network Stack and Driver
by Norrathep Rattanavipanon 31 Mar '16

31 Mar '16

Hello, My name is Oak and I'm working with Prof. Gene Tsudik for remote attestation project using sel4. I know that you guys are not interested in developing network stack and drivers for sel4. But do you happen to know if anyone else has done some work with network stack and Wi-fi, Bluetooth or ethernet driver in sel4? Regards, Oak -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

答复:答复: 答复:Re: About the execution time of seL4 API
by xurongfeik 30 Mar '16

30 Mar '16

裴老师：您好！谢谢您的资料。现在我们学校有两个团队在做这方面的工作：其中我们实验室主要在模型层对seL4微内核进行建模仿真，主要是把微内核基本功能机制建模成为一个基本模型，对User Mode扩展部分以策略模型的方式与基本模型进行编织，从而建立一套在设计早期通过模型仿真验证策略的方法。目前，我们正着手建立一个能准确反映真实seL4微内核运行的模型，但是由于仿真时钟的不准确，我们希望在某一硬件环境上把seL4微内核模型下层的系统调用时间统计出来，通过时间累加计算seL4微内核模型上的应用执行过程。但是目前不知道该如何获取这些系统调用的执行时间，不知道裴老师您那边是否有相关的数据？另外一个团队主要是基于seL4微内核的操作系统开发，主要考虑分区、并发的不确定性。目前主要用于航天的应用中。如果裴老师有相关的研究，非常愿意共同合作！祝好！许荣飞在 2016-03-29 14:39:35，"XilongPei" <pei.xilong(a)kortide.com> 写道： XuRongfei: 我是同济大学电信学院老师裴喜龙，我们从事你说的这个方向好几年了。附件文件是我把seL4的说明书翻译成了中文，下面这个链接是我们做的高可用操作系统的项目工程页面。 http://elastos.org/redmine/projects/rt-elastos这个工程的源码在： https://github.com/elastos/HD-Elastos 我们基于AOP思想做的操作系统（正在开发中），官网：http://elastos.org/project-guide/ 源码开源在github: https://github.com/elastos/ElastosRDK5_0它基于AOP思想，提出一种构件技术CAR，并基于这个构件技术，实现了一… 希望国内做相关工作的人能合作，共同做一些大的工程。同济大学裴喜龙 2016年3月29日星期二发件人: Devel [mailto:devel-bounces@sel4.systems] 代表 xurongfeik 发送时间: 2016年3月29日 14:11 收件人: Thomas Sewell <thomas.sewell(a)nicta.com.au> 抄送:devel@sel4.systems 主题: [seL4] 答复:Re: About the execution time of seL4 API Thank you for your reply！ My name is XuRongfei, and I am a PHD student from China,Beijing. Now I focus on RTOS Modeling and Simulation. As we know, an important principle of microkernel design is the separation of mechanism and policy, it is what enables the construction of arbitrary systems on top of a minimal kernel. This separation of mechanism and policy is similar to AOM(Aspect-Oriented Modeling) and we can model the mechanism and policy separately. The biggest advantage is that analysis and verification of the policy applied in the implementation phase will be advanced to the design stage. As seL4 Microkernel is "the world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement". So if we want to construct an RTOS on top of seL4 Microkernel, it is necessary to simulate and analyse the policy model on the microkernel model first. To simulate the seL4 Microkernel model accurately and agree with the real situation, the execution time of seL4 typical API (such as send\receive\notify message and Resume\Suspend\Create thread) for certain platform. So how can we get the execution time of this APIs for certain platform? Is it possible? Thank you very much! At 2016-03-29 11:45:42, "Thomas Sewell" <thomas.sewell(a)nicta.com.au> wrote: Hmm, what do you mean by measuring the time? You can measure the typical execution time of various system calls easily enough by checking the CPU cycle counter. There is an internal "sel4bench" project which is similar to "sel4test" but measures timing information of some system calls. My understanding is that this will be released at some point in the near future. It's also possible to calculate the worst-case execution time of the kernel for some platforms. There's been a lot of research work on this http://ssrg.nicta.com.au/projects/TS/realtime.pml by various people at Data61/NICTA. It's probably possible to replicate for some platform of interest, but it might be quite difficult to do. Cheers, Thomas. On 29/03/16 14:06, xurongfeik wrote: Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

2 1

About the execution time of seL4 API
by xurongfeik 30 Mar '16

30 Mar '16

Hello，everyone： When given a specific platform， is it possible to measure the execution time of seL4 API？ Anyone who has the relative data please send it to me， many thanks！！ -- 许荣飞 Rongfei Xu 北京航空航天大学 Beihang University

3 4

Where can I get the information about Linux on seL4
by XilongPei 29 Mar '16

29 Mar '16

Hi Gernot, I found that the footer of http://ssrg.nicta.com.au/ is: Served by Apache on Linux on seL4 Whare can I get more information about Linux on seL4? Xilong Pei Tongji University 2016/3/29

2 1

Status of ARMv8 support for seL4 ?
by karim.allah.ahmed＠gmail.com 29 Mar '16

29 Mar '16

Hello, >From this roadmap [0], I can see that ARMv8 support is underway at the moment. Is this something that's going to be released soon given that the roadmap says Q1-2016 (at least 32-bit) ? [0] https://sel4.systems/Info/Roadmap -- Karim Allah Ahmed.

1 0

Porting Qubes OS to seL4 project
by Paul Vlase 28 Mar '16

28 Mar '16

No answer ... Am I doing something wrong? Beside not have patience. Could anyone tell about the status of the seL4 Qubes port project and who can I get in touch with to talk more about it? On Tue, Mar 22, 2016 at 11:35 PM, Paul Vlase <vlase.paul(a)gmail.com> wrote: > Hello, > > My name is Paul Vlase and I am following a master degree right now. I > am interested in porting the Qubes OS to seL4 project and I saw that > you are working already on it. Is there anything I can help you on > this project? > > Thank you, > Paul Vlase

2 1

sel4 in TrustZone
by Norrathep Rattanavipanon 27 Mar '16

27 Mar '16

Hi again :) Is it possible to run sel4 as a secure world OS in TrustZone? Has anyone successfully done that before? Thank you, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

6 6

(simple?) build error?
by 谢文龙 27 Mar '16

27 Mar '16

I'm getting an error when building from Ubuntu. I'm building from: repo init -u https://github.com/seL4/sel4test-manifest.git I've configured with: make ia32_simulation_release_xml_defconfig and done "make menuconfig" accepting the defaults. Finally I run make and get errors: [KERNEL] [PBF_GEN] arch/object/structures.pbf [PBF_GEN] arch/api/shared_types.pbf [PBF_GEN] plat/machine/hardware.pbf [PBF_GEN] api/types.pbf [BF_GEN] arch/object/structures_gen.h [BF_GEN] arch/api/shared_types_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/x86/32/machine_asm.s [AS] src/arch/x86/32/machine_asm.o [CPP] src/arch/x86/32/traps.s [AS] src/arch/x86/32/traps.o [CPP] src/arch/x86/32/head.s [AS] src/arch/x86/32/head.o [CPP] src/arch/x86/halt.s [AS] src/arch/x86/halt.o [CPP] src/arch/x86/idle.s [AS] src/arch/x86/idle.o [TOUCH] sources_list_updated [CPP_GEN] kernel_all.c [CPP] kernel_all.c_pp [CP] kernel_final.c [CC] kernel_final.s [AS] kernel.o [LD] kernel.elf /usr/bin/ld:linker.lds_pp:5: syntax error collect2: error: ld returned 1 exit status make[1]: *** [kernel.elf] Error 1 make: *** [kernel_elf] Error 2 make V=3 mkdir -p /home/talos/seL4test/stage/x86/pc99 mkdir -p /home/talos/seL4test/build/x86/pc99 mkdir -p /home/talos/seL4test/images mkdir -p /home/talos/seL4test/stage/x86/pc99/common cp -R /home/talos/seL4test/tools/common/* /home/talos/seL4test/stage/x86/pc99/common [libs/libsel4] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4 CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4 -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4 SOURCE_DIR=/home/talos/seL4test/libs/libsel4 V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4' [GEN] include/sel4/types_gen.h [GEN] arch_include/x86/sel4/arch/invocation.h [GEN] include/sel4/shared_types_gen.h [GEN] sel4_arch_include/ia32/sel4/sel4_arch/invocation.h [HEADERS] [STAGE] api/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] sel4/* [STAGE] sel4/* [STAGE] interfaces/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4' [libs/libsel4] done. [libs/libmuslc] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libmuslc CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libmuslc -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libmuslc/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libmuslc SOURCE_DIR=/home/talos/seL4test/libs/libmuslc V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libmuslc' make[1]: Nothing to be done for `default'. make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libmuslc' [libs/libmuslc] done. [libs/libcpio] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libcpio CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libcpio -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libcpio/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libcpio SOURCE_DIR=/home/talos/seL4test/libs/libcpio V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libcpio' [HEADERS] [STAGE] cpio/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libcpio' [libs/libcpio] done. [libs/libutils] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libutils CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libutils -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libutils/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libutils SOURCE_DIR=/home/talos/seL4test/libs/libutils V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libutils' [HEADERS] [STAGE] utils/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libutils' [libs/libutils] done. [libs/libsel4vka] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4vka CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4vka -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4vka/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4vka SOURCE_DIR=/home/talos/seL4test/libs/libsel4vka V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4vka' [HEADERS] [STAGE] vka/* [STAGE] vka/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4vka' [libs/libsel4vka] done. [libs/libsel4vspace] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4vspace CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4vspace -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4vspace/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4vspace SOURCE_DIR=/home/talos/seL4test/libs/libsel4vspace V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4vspace' [HEADERS] [STAGE] vspace/* [STAGE] vspace/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4vspace' [libs/libsel4vspace] done. [libs/libplatsupport] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libplatsupport CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libplatsupport -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libplatsupport/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libplatsupport SOURCE_DIR=/home/talos/seL4test/libs/libplatsupport V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libplatsupport' [HEADERS] [STAGE] platsupport/* [STAGE] platsupport/* [STAGE] platsupport/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libplatsupport' [libs/libplatsupport] done. [libs/libsel4simple] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4simple CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4simple -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4simple/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4simple SOURCE_DIR=/home/talos/seL4test/libs/libsel4simple V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4simple' [HEADERS] [STAGE] simple/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4simple' [libs/libsel4simple] done. [libs/libsel4simple-default] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4simple-default CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4simple-default -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4simple-default/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4simple-default SOURCE_DIR=/home/talos/seL4test/libs/libsel4simple-default V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4simple-default' [HEADERS] [STAGE] simple-default/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4simple-default' [libs/libsel4simple-default] done. [libs/libsel4platsupport] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4platsupport CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4platsupport -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4platsupport/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4platsupport SOURCE_DIR=/home/talos/seL4test/libs/libsel4platsupport V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4platsupport' [HEADERS] [STAGE] sel4platsupport/* [STAGE] sel4platsupport/* [STAGE] sel4platsupport/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4platsupport' [libs/libsel4platsupport] done. [libs/libelf] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libelf CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libelf -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libelf/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libelf SOURCE_DIR=/home/talos/seL4test/libs/libelf V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libelf' [HEADERS] [STAGE] elf/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libelf' [libs/libelf] done. [libs/libsel4utils] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4utils CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4utils -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4utils/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4utils SOURCE_DIR=/home/talos/seL4test/libs/libsel4utils V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4utils' [HEADERS] [STAGE] sel4utils/* [STAGE] sel4utils/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4utils' [libs/libsel4utils] done. [libs/libsel4muslcsys] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4muslcsys CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4muslcsys -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4muslcsys/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4muslcsys SOURCE_DIR=/home/talos/seL4test/libs/libsel4muslcsys V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4muslcsys' [HEADERS] [STAGE] arch_stdio.h [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4muslcsys' [libs/libsel4muslcsys] done. [libs/libsel4allocman] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4allocman CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4allocman -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4allocman/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4allocman SOURCE_DIR=/home/talos/seL4test/libs/libsel4allocman V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4allocman' [HEADERS] [STAGE] allocman/* [STAGE] allocman/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4allocman' [libs/libsel4allocman] done. [libs/libsel4test] building... mkdir -p /home/talos/seL4test/build/x86/pc99/libsel4test CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/libsel4test -f /home/talos/seL4test/.config -f /home/talos/seL4test/libs/libsel4test/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/libsel4test SOURCE_DIR=/home/talos/seL4test/libs/libsel4test V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/libsel4test' [HEADERS] [STAGE] sel4test/* [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/libsel4test' [libs/libsel4test] done. [apps/sel4test-tests] building... mkdir -p /home/talos/seL4test/build/x86/pc99/sel4test-tests CFLAGS= LDFLAGS= make -C /home/talos/seL4test/build/x86/pc99/sel4test-tests -f /home/talos/seL4test/.config -f /home/talos/seL4test/apps/sel4test-tests/Makefile \ BUILD_DIR=/home/talos/seL4test/build/x86/pc99/sel4test-tests SOURCE_DIR=/home/talos/seL4test/apps/sel4test-tests V=3 \ STAGE_DIR=/home/talos/seL4test/stage/x86/pc99 \ TOOLPREFIX= make[1]: Entering directory `/home/talos/seL4test/build/x86/pc99/sel4test-tests' [HEADERS] [STAGE] autoconf.h make[1]: Leaving directory `/home/talos/seL4test/build/x86/pc99/sel4test-tests' [apps/sel4test-tests] done. [KERNEL] mkdir -p /home/talos/seL4test/build/kernel make -C /home/talos/seL4test/build/kernel -f /home/talos/seL4test/kernel/Makefile \ SOURCE_ROOT=/home/talos/seL4test/kernel O=/home/talos/seL4test/build/kernel V=3 \ TOOLPREFIX= \ CONFIG_DOMAIN_SCHEDULE= \ HAVE_AUTOCONF=1 NO_PRESERVE_TIMESTAMP=1 seL4 build options: =================== ARCH = x86 PLAT = pc99 CPU = TOOLPREFIX = PATH = /home/talos/bin:/home/talos/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games DEBUG = ASSERT = CONFIG_DEFS = CYCLE_COUNTER PERF_COUNTER=CYCLE_COUNTER DANGEROUS_CODE_INJECTION = CC = gcc CC_PATH = CPP = cpp CPP_PATH = AS = as AS_PATH = LD = ld LD_PATH = PARSER = c-parser PARSER_PATH = BF_GEN = bitfield_gen.py BF_GEN_PATH = SYSCALL_ID_GEN = syscall_header_gen.py SYSCALL_ID_GEN_PATH = INVOCATION_ID_GEN = invocation_header_gen.py INVOCATION_ID_GEN_PATH = XMLLINT_PATH = XMLLINT = xmllint.sh CFLAGS = -fno-stack-protector -m32 --std=c99 -nostdlib -nostdinc -ffreestanding -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -Wdeclaration-after-statement "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" -O2 -mno-mmx -mno-sse -mno-sse2 -mno-3dnow -DCYCLE_COUNTER -DPERF_COUNTER=CYCLE_COUNTER -DFASTPATH ASFLAGS = -Wa,--32 "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" CPPFLAGS = -DHAVE_AUTOCONF -I/home/talos/seL4test/include/generated -DARCH_X86 -DIA32 -DARCH_IA32 -D__KERNEL_32__ -DX86_32 -DPLAT_PC99 -DFASTPATH -DCYCLE_COUNTER -DPERF_COUNTER=CYCLE_COUNTER -DFASTPATH "-I/home/talos/seL4test/kernel/include/arch/x86/arch/32" "-I/home/talos/seL4test/kernel/include/plat/pc99/plat/32" LDFLAGS = -Wl,--build-id=none -Wl,-m,elf_i386 -nostdlib -nostdinc -Wl,--build-id=none -O2 make[1]: Entering directory `/home/talos/seL4test/build/kernel' [LD] kernel.elf /home/talos/seL4test/kernel/tools/changed.sh kernel.elf gcc -Wl,--build-id=none -Wl,-m,elf_i386 -nostdlib -nostdinc -Wl,--build-id=none -O2 -Wl,-T -Wl,linker.lds_pp \ -o kernel.elf src/arch/x86/32/machine_asm.o src/arch/x86/32/traps.o src/arch/x86/32/head.o src/arch/x86/halt.o src/arch/x86/idle.o kernel.o /usr/bin/ld:linker.lds_pp:5: syntax error collect2: error: ld returned 1 exit status make[1]: *** [kernel.elf] Error 1 make[1]: Leaving directory `/home/talos/seL4test/build/kernel' make: *** [kernel_elf] Error 2

2 1

sel4 benchmark
by Norrathep Rattanavipanon 25 Mar '16

25 Mar '16

Hello, What's the best way to benchmark my program inside sel4? I saw wiki page about running sel4 bench (https://wiki.sel4.systems/Benchmarking%20guide) but it wasnt filled yet. So I wonder if there's any public guide or tutorial on that? I also found this https://github.com/seL4/libplatsupport/blob/master/arch_include/x86/platsup… and tried both rdtsc_pure and rdtsc_cpuid but neither of them seems to produce reliable results. Best, -- Norrathep (Oak) Rattanavipanon M.S. in Computer Science University of California - Irvine

2 1

sel4 job offer
by Julien Delange 24 Mar '16

24 Mar '16

For information, we are looking for people to work on sel4. See https://www.appone.com/maininforeq.asp?Ad=250944&R_ID=1243309&Refer=http://… If you have any question, do not hesitate to contact me and/or apply! Julien.

1 0

Porting Qubes OS to seL4 project
by Paul Vlase 23 Mar '16

23 Mar '16

Hello, My name is Paul Vlase and I am following a master degree right now. I am interested in porting the Qubes OS to seL4 project and I saw that you are working already on it. Is there anything I can help you on this project? Thank you, Paul Vlase

1 0

[CAmkES] CAmkES 2.1.0 Release Notes
by Stephen Sherratt 22 Mar '16

22 Mar '16

CAmkES 2.1.0 Release Notes ========================== ## New Features - runner takes an `--architecture` command line argument which selects the target architecture. Valid arguments are: aarch32, arm_hyp, ia32 - added the ability to specify a hardware dataport as cached. Previously all hardware dataports were mapped uncached. This feature is intended to be used on dataports backed by DMA-able memory to improve access times. Functions to flush dataports from the cache are also provided. - support for seL4 3.0.0 ## Removed Features - `--hyp` command line argument is replaced with `--architecture arm_hyp` ## API Removals ### Unmarshalling Helpers These were intended for use in templates, but are no longer used in any internal templates: - `camkes_marshal` - `camkes_marshal_string` - `camkes_unmarshal` - `camkes_unmarshal_string` ### DMA Utilities These had been deprecated for a long period and are now being removed: - `camkes_dma_page_alloc` - `camkes_dma_page_free` You can find it at: https://github.com/seL4/camkes-tool/tree/camkes-2.1.0 A manifest for the 2.1.0 compatible versions of test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.1.x.xml Release notes on the wiki: https://wiki.sel4.systems/CAmkES%202.1.0 Enjoy! ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

What happens to the IPC buffer when you make another process within the same Vspace?
by Qiwei Wen 20 Mar '16

20 Mar '16

Hi, I'm trying to write a multithreaded seL4 application. It's to be made up of sel4util processes with different cspaces and sharing the same Vspace. I managed to achieve this, but what confuses me is that since the processes share the same Vspace, wouldn't GetIPCBuffer() return the same result for each of them? I looked at libsel4/arch_include/arm/sel4/arch/functions.h, and GetIPCBuffer() is simply: return *(seL4_IPCBuffer**)seL4_GlobalsFrame; Since seL4_GlobalsFrame is just a fixed memory location (0xffffc000) in the shared address space, why does seL4_GetIPCBuffer() return different results for different processes? Below is the output: ========================== PARENT: IPCBUFFER: 00273000 CHILD: GlobalsFrame: ffffc000, *GlobalsFrame 10076000 CHILD: setting shared to 97 PARENT: CHILD DIED, shared char: 97, MR16: 00000000 ============================= Is it that the frame ffffc000 mapping is changed on every context switch perhaps? Can I absolutely trust that IPC is still working correctly with this set up? Thanks, David

5 4

Isabelle itself proven?
by Steve VanderLeest 20 Mar '16

20 Mar '16

Since the formal verification of functional correctness of seL4 was performed using the Isabelle theorem prover, could someone tell me if Isabelle itself has been formally verified? If so, could you suggest some good references to that work? Regards, Steve Steven H. VanderLeest, Ph.D. Chief Operating Officer DornerWorks, Ltd. 3445 Lake Eastbrook Grand Rapids, MI 49546 www.dornerworks.com

3 2

Booting process
by Daniel Wang 19 Mar '16

19 Mar '16

Hi all, I’m very new to seL4 development. I’m particularly interested in understanding seL4 kernel source code. Could someone points me out how the seL4 is booted and where should I start learning? Thanks -Dan

3 2

seL4 wiki
by Anna Lyons 19 Mar '16

19 Mar '16

Hi all, We've created a public wiki for seL4 development here: https://wiki.sel4.systems/ The kernel team have put some effort into creating the initial content, but there is much more to be done. Contributions encouraged! New accounts are restricted to avoid spam, but if you have posted on this mailing list your account will be approved quickly. Otherwise contact us. Thanks, Anna Lyons seL4 Kernel Engineer | PhD Student DATA61 | CSIRO E <mailto:Brigitte.Biscotto@data61.csiro.au> Anna.Lyons(a)data61.csiro.au<mailto:Anna.Lyons@data61.csiro.au> Level 3, K17 Building, UNSW Gate 14, Barker Street, Kensington, NSW, 2033 l Locked Bag 6016, Sydney NSW 1466 www.data61.csiro.au<http://www.data61.csiro.au/> CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 [cid:image001.png@01D0EFD9.052ECFC0] ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

FYI: microkernel.info community site
by Jakub Jermář 14 Mar '16

14 Mar '16

Hello, just FYI, I have set up a simple web page[1] to promote the wider microkernel community and its goals. So far, the page comes with a brief description of the microkernel concept and an incomplete list of microkernel projects with links to each project's web. The description is made out of the first two sentences I found in the "What is XYZ" section or elsewhere on the web of the respective project. I also took the freedom to use the respective project's logo (or what I believed was the project's logo) for promoting it. I hope you will find this small web a good idea. It was inspired by a similar (though a little bit more informative) site set up by the unikernel community [2]. The sources of the [1] web are hosted on Github [3], so feel free to submit issues or PR to make the site better. Please send me a PM if there are any issues pertaining your project's cartouche that cannot be dealt with using Github. Thanks, Jakub [1] http://microkernel.info [2] http://unikernel.org/projects/ [3] https://github.com/jermar/microkernel.info

8 8

Capability faults on seL4_Send and seL4_Call
by Qiwei Wen 12 Mar '16

12 Mar '16

Hi all, I understand that capability faults for seL4_Send and seL4_Call only happen when the look-up fails, and not when illegal operations are attempted, such as calling a null cap or a piece of untyped memory. Is there another way at all, then, that such errors can be handled by user-level code? This is part of a project where the faulting process needs to surrender control to another process whenever it performs a system call on an invalid capability. Is there a way to achieve this given that fault endpoints will not work? Thanks, David

1 0

using camkesvm with qemu
by Julien Delange 10 Mar '16

10 Mar '16

Hi, I am currently trying to use the camkesvm example and run it in qemu. I am currently able to compile the c162_twovm_defconfig application. However, when running, I have the following issue (see below). So, I am wondering what would be the good arguments to start the application in qemu. I noticed that the kernel/initrd image for linux are specific in a header file, I assume this is also included in the image loaded by capdl. Any idea about how to run this example with qemu and/or how to test it? Thanks! Starting node #0 vt-x: not supported <<seL4 [decodeUntypedInvocation/193 T0xe2ff1900 "rootserver" @804afa7]: Untyped Retype: Insufficient memory or offset outside untyped>> Unmasking IOAPIC source 2 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 3 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 4 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 16 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 17 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 18 on ioapic 0 without ever setting its mode! Unmasking IOAPIC source 23 on ioapic 0 without ever setting its mode! <<seL4 [decodeCNodeInvocation/107 T0xe2ff1900 "rootserver" @804a4b2]: CNode Copy/Mint/Move/Mutate: Source slot invalid or empty.>> capDL-loader :: << Error: init_cnode_slot:1471: seL4_FailedLookup >> Ignoring call to sys_rt_sigprocmask

3 4

Recovering from cap fault?
by Qiwei Wen 10 Mar '16

10 Mar '16

Hi all, On page 26 of the manual (1.2) there's an instruction on how to restart a thread following a capability fault. The program counter where the faulting thread should pick up execution is said to be message register 0. What I'm trying to do is to restart the execution on the next instruction following the system call instruction so as to skip it. Try as I might, it will not work and the faulting thread is stuck in an endless number of faults. Below is the relevant code: seL4_Word pc = seL4_GetMR(0); printf("cap fault, pc: %08x, on %s\n",pc,seL4_GetMR(2)?"wait":"send"); //assert(!faultnum++); seL4_MessageInfo_t info = seL4_MessageInfo_new (seL4_CapFault,0,0,1); seL4_SetMR(0,pc + 4); seL4_Reply(info); It does restart, but immediately cap-faults again at the very same program counter. Is it supposed to work? What did I do wrong? Cheers, David

2 1

seL4 Tutorial Idea
by da Tyga 09 Mar '16

09 Mar '16

Hi Andrew Jackman! First of all apologies about my assumptions. In my hasty reading of your question I got the impression you were talking about yourself and not the intended audience for your tutorial material proposal. Like yourself, I too would use a practical, tutorial style guide if it were available. So I would like to give my vote for your idea. Unfortunately, I'm a one-man-show and thus not in a position to make a pledge towards a tutorial effort. Perhaps the good folks who are involved with seL4 could suggest how your proposal could come about. Reading these digests, tit would appear that there are quite a few people who are trying to come to grips with seL4. Yes, I was referring to the material that you linked. Cheers, Tyga >>> thread in reverse chrono-order: Andrew Jackman kd7nyq(a)gmail.com On Sun, Mar 6, 2016 at 11:04 AM, Jackman <kd7nyq(a)gmail.com> wrote: > Is anyone interested in tutoring on the topic of sel4? I have two > objectives: > > First, I'm interested in beginning programming, like getting through the > Hello World process. I would hope this eventually includes things like > basic driver development and practical application development. > > Second, I want to understand how virtualization works with sel4 and the > infrastructure behind it. My objective is to be able to stand up my own > virtualization host and guests. > > I'm not sure how payment would work. I'd be interested in turning our > experience into tutorials for community consumption, which may be more > valuable to some of you than the money. > > Thank you. > > Andrew Roy Jackman Hi Andrew, I don't wish to discourage you, but if you are just starting out programming and have limited knowledge of operating systems, etc ... then seL4 might be a very big undertaking to understand and learn from. There are a lot of topics you would need to come up to speed on. I suggest taking a look Gernot's course material at unsw.edu.au. > da Tyga: Thank you for writing back. I totally agree with your assessment. Permit me to elaborate a bit more on my situation. I am a professional software engineer who is primarily dedicated to writing virtualization automation software for sales demonstrations. Naturally, our department is always interested in ways in which we can improve the efficiency of our virtualization environment(s). After reading 'L4 Virtualization and Beyond' (2008, http://os.inf.tu-dresden.de/papers_ps/haertig08_l4_virtualization_and_beyon… ), I became fascinated with L4. I am here talking to you all because of the amount of press that seL4 has gotten as the proofed L4 kernel and because it appears to have the best, most easily understood documentation. Now, that does not mean that I think seL4 is well documented, just that it's the best documented of the L4 projects. The purpose of my original email was to very gently say that the introductory material to seL4 is so bad, that I'm willing to pay someone to either bring it up to date, assist me with it, or both. For example, there is a thread about RefOS, wherein Kevin wrote, "RefOS was a student project that is now no longer actively maintained." Gapry and HyperNewbie, however, provided at least some fixes, but their fixes don't appear to have gotten any attention from upstream. This was on 11 February. Nevertheless, RefOS appears to be the only seL4 project geared towards newcomers on the 'Getting Started' page ( https://sel4.systems/Info/GettingStarted/) You should note that, on that page, there is no indicator that newcomers should, in fact, stay away from that project because it's no longer maintained. I don't think requesting some attention on documentation is a bad or unjust thing. I would hope that lowering the barriers to entry to the seL4 community would increase the flow of developers, users, and sponsors to the seL4 project. In turn, I hope that would be seen as a good thing. I'm offering part-time, albeit unofficial, company sponsored development in exchange for some paid tutoring. I am not asking for a hand-out. If I didn't have to worry about ramp-up time or coming up with deliverables, I wouldn't be bugging you. Now, if you're worried about my qualifications, I'm a university educated computer scientist. While I've spent most of my career on web programming, I've studied operating systems development both at school and on my own. I began a toy kernel with the help of the osdev.org resources, and I'm happy with my progress. When I take inventory, however, I realize I don't have the desire to (re-)write an L4 kernel, nor do I think I can improve upon it. Finally, I think you're referring to Professor Gernot Heiser's page at https://www.cse.unsw.edu.au/~gernot/, and probably more specifically the CS9242 course at http://www.cse.unsw.edu.au/~cs9242/current/. If you're referring to another course, please be more specific. Thank you. Andrew Jackman kd7nyq(a)gmail.com

5 5

Tutor?
by Jackman 09 Mar '16

09 Mar '16

Is anyone interested in tutoring on the topic of sel4? I have two objectives: First, I'm interested in beginning programming, like getting through the Hello World process. I would hope this eventually includes things like basic driver development and practical application development. Second, I want to understand how virtualization works with sel4 and the infrastructure behind it. My objective is to be able to stand up my own virtualization host and guests. I'm not sure how payment would work. I'd be interested in turning our experience into tutorials for community consumption, which may be more valuable to some of you than the money. Thank you. Andrew Roy Jackman

2 2

Performce test for CAMKES or RefOS
by ぷ风过无痕?? 08 Mar '16

08 Mar '16

Hi everyone, I want to measure a variety of important aspects of system performance on CAMKES or RefOS. I know that Lmbench is an extensive suite of micro-benchmarks that give powerful insights into system performance. And lmbench is written in ANSI-C,so it is portable across a wide variety of systems and architectures. Can I measure the system performance on CAMKES or RefOS using Lmbench ? Thank you.

2 1

Re: [seL4] Devel Digest, Vol 22, Issue 1
by da Tyga 08 Mar '16

08 Mar '16

Hi Andrew, I don't wish to discourage you, but if you are just starting out programming and have limited knowledge of operating systems, etc ... then seL4 might be a very big undertaking to understand and learn from. There are a lot of topics you would need to come up to speed on. I suggest taking a look Gernot's course material at unsw.edu.au. On 7 March 2016 at 12:00, <devel-request(a)sel4.systems> wrote: > Send Devel mailing list submissions to > devel(a)sel4.systems > > To subscribe or unsubscribe via the World Wide Web, visit > https://sel4.systems/lists/listinfo/devel > or, via email, send a message with subject or body 'help' to > devel-request(a)sel4.systems > > You can reach the person managing the list at > devel-owner(a)sel4.systems > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Devel digest..." > > > Today's Topics: > > 1. Tutor? (Jackman) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Sun, 6 Mar 2016 11:04:25 -0700 > From: Jackman <kd7nyq(a)gmail.com> > To: devel(a)sel4.systems > Subject: [seL4] Tutor? > Message-ID: > < > CAADorGK4z2oW4JoBq+K--72LDGc0d-2-1jTxUu41UxidvwjkHw(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Is anyone interested in tutoring on the topic of sel4? I have two > objectives: > > First, I'm interested in beginning programming, like getting through the > Hello World process. I would hope this eventually includes things like > basic driver development and practical application development. > > Second, I want to understand how virtualization works with sel4 and the > infrastructure behind it. My objective is to be able to stand up my own > virtualization host and guests. > > I'm not sure how payment would work. I'd be interested in turning our > experience into tutorials for community consumption, which may be more > valuable to some of you than the money. > > Thank you. > > Andrew Roy Jackman >

1 0

Can not build RefOS
by Gapry Un 08 Mar '16

08 Mar '16

Dear all, I follow the official step (https://github.com/seL4/refos-manifest) to build RefOS and it occurs the following error message. In file included from /home/chi-wai/Workspaces/microkernel/RefOS/libs/librefos/src/sync.c:16:0: ~/Workspaces/RefOS/stage/arm/imx31/include/refos/refos.h:73:1: *error: unknown type name ‘uint32_t’* ~/Workspaces/RefOS/stage/arm/imx31/include/refos/refos.h:73:23: *error: unknown type name ‘uint32_t’* In file included from /home/chi-wai/Workspaces/microkernel/RefOS/libs/librefos/src/sync.c:18:0: ~/Workspaces/RefOS/stage/arm/imx31/include/refos-util/cspace.h:44:72: *error: unknown type name ‘uint32_t’* ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_create_mutex’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:49:5: *warning*: ‘seL4_Notify’ is deprecated (declared at /home/chi-wai/Workspaces/microkernel/RefOS/stage/arm/imx31/include/sel4/deprecated.h:23): use seL4_Signal [-Wdeprecated-declarations] ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_acquire’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:65:5: *error: invalid initializer* ~/Workspaces/RefOS/libs/librefos/src/sync.c: In function ‘sync_release’: ~/Workspaces/RefOS/libs/librefos/src/sync.c:74:5: *warning*: ‘seL4_Notify’ is deprecated (declared at /home/chi-wai/Workspaces/microkernel/RefOS/stage/arm/imx31/include/sel4/deprecated.h:23): use seL4_Signal [-Wdeprecated-declarations] make[1]: *** [src/sync.o] Error 1 make: *** [librefos] Error 2 Does RefOS use the old seL4 API ? If it is, which version I need to downgrade? Thanks for any help or suggestion, Gapry. https://gapry.wordpress.com/

6 9

Re: [seL4] Devel Digest, Vol 21, Issue 11
by ぷ风过无痕?? 23 Feb '16

23 Feb '16

Hi everyone,I find an interesting problem when I read the code of endpoint(kernel\src\object\endpoint.c). In the sendIPC and receiveIPC functions , I see there are 3 states for an endpoint(Idle , send , receive). Below it is the state machine diagram. sendIPC EPState_Recv ——> EPState_Idle ——>EPState_send receiveIPC EPState_send——> EPState_Idle ——>EPState_Recv But when I add some print infomation, I find the endpoint can never reach the Send state. I think the correct state machine diagram just has two states(idle and receive). sendIPC EPState_Recv ——> EPState_Idle receiveIPC EPState_Idle ——>EPState_Recv Am I right???

2 1

Timer for AM335x
by Julien Delange 18 Feb '16

18 Feb '16

I am trying to develop a camkes application with one component having access to the timer. I got some inspiration from the time server for the kzm machine. Now, I am trying to port that to the am335x machine to execute on a beagleboard black. I dig into the code and found the appropriate platform-specific functions to call. Unfortunately, when trying to compile, it fails (see below). Anybody has an idea why this happens? Also, if you want to look at the camkes application, I put it on github at https://github.com/juli1/sel4-experiments/tree/master/camkes/pingimpl-am335x Thanks for any help! /home/sel4/test/camkes/build/arm/am335x/pingimpl/src/timer/static/components/timer/src/timer.o: In function `irq_callback': /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:22: undefined reference to `dm_handle_irq' /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:32: undefined reference to `dm_oneshot_relative' /home/sel4/test/camkes/build/arm/am335x/pingimpl/src/timer/static/components/timer/src/timer.o: In function `run': /home/sel4/test/camkes/apps/pingimpl/components/timer/src/timer.c:58: undefined reference to `dm_oneshot_relative' collect2: error: ld returned 1 exit status

2 2

handling timer with camkes
by Julien Delange 17 Feb '16

17 Feb '16

Dear all, I would like to build a scheduler on top of camkes. I figure that I have to get access to the timer irq and start from there (e.g. then, dispatch other tasks according to the number of elapsed ticks). I did find some relevant examples, especially in the camkes-vm ( https://github.com/seL4/camkes-vm) but nothing I can try. Is there any information about such materials? I tried to reuse the component but always got build error. I was wondering if there was an existing tutorial or an example I could try that will help me. Thanks. Julien.

2 3

Allocation of untyped memory
by Norman Feske 09 Feb '16

09 Feb '16

Hello, while moving Genode's seL4 support to seL4 version 2, I stumbled over the dynamic allocation within untyped memory regions. In the old experimental branch that I used previously, the retype-untyped operation allowed me to manually specify an offset where the new kernel object should be placed within the untyped memory region. So I was able to manage the allocation of untyped memory manually. In short, I added each initial untyped memory region to a roottask-local "phys-mem" allocator. Each time when creating a kernel object, I asked this allocator for a region of the required size and alignment, determined the untyped-memory capability that belongs to the found region, and used this capability to create the kernel object(s) at the calculated offset within the untyped-memory region. This worked very well. After switching to version 2, I found the retype-untyped operation to lack the offset argument (which admittedly was never present in the non-experimental version). Instead of accepting an offset parameter, the kernel maintains a built-in allocator per untyped-memory region. (please correct me if my understanding is wrong) The allocator is basically a simple offset value ("FreeIndex") that is increased with each allocation. Since I no longer have the chance to specify the offset explicitly, I have to rely on the allocation policy of the kernel and hit the following problem: There exists an untyped memory region of size 0x2000. Initially, the FreeIndex is 0. Now, I am creating the following kernel objects within the untyped-memory region: 1. CNode with totalObjectSize 0x400: -> The allocation increases FreeIndex to 0x400. 2. CNode with totalObjectSize 0x800: -> The FreeIndex gets aligned to 0x800 (natural alignment of the to-be-created CNode). This creates a gap between 0x400 and 0x800. -> The allocation increases FreeIndex to 0x1000. 3. seL4_IA32_4K with a totalObjectSize 0x1000: -> The allocation increases FreeIndex to 0x2000. 4. CNode with totalObjectSize 0x400: <<seL4 [decodeUntypedInvocation/209 T0xe3fc9900 "rootserver" @2013228]: Untyped Retype: Insufficient memory (1 * 1024 bytes needed, 0 bytes available).>> Since FreeIndex equals the size of the untyped memory region, the kernel concludes that untypedFreeBytes is 0. Even though there exists a gap of 0x400 within the untyped memory region that satisfies the alignment of the to-be-created kernel object, the kernel won't allow me to use it. In contrast, with the retype-untyped-at-offset operation, such a situation never occurred. Right now, I am a bit puzzled about how to proceed and have the following questions in the back of me head: * What is the rationale behind fixing the allocation policy within untyped memory regions in the kernel. Doesn't this design contradict with the principle of avoiding policy in the kernel? In my specific case, this policy seemingly makes my life much more difficult. To use the kernel in a deterministic way, I would need to model the kernel's allocation behavior in the user land. * From what I gather from the kernel's source code, the built-in allocator would not allow me to reuse parts of untyped memory regions because 'FreeIndex' is always increasing. E.g., after revoking the CNodes of steps 1 and 2, I still cannot create any new kernel objects within the untyped memory region because FreeIndex remains equal the size of the untyped memory region. Is this correct? * Is it possible to give me the retyped-untyped-at-offset operation back? ;-) e.g., in the form of a patch? Or alternatively, are there any best practices that I could follow wrt managing untyped memory? Maybe I'm just approaching the problem from the wrong angle? 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

3 5

Upgrading to Camkes 2.0
by Jeff Hieb 26 Jan '16

26 Jan '16

I was looking to upgrade to CAmkES release 2.0. but can't get an example arm configuration to compile. I did a a fresh clone using https://github.com/seL4/camkes-manifest.git and found the ia32_simple_defconfig compiles fine, but not arm_simple_defconfig make arm_simple_defconfig make [libs/libsel4] building... make[1]: *** No rule to make target `/home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/arm/interfaces/sel4arch.xml', needed by `include/interfaces/sel4_client.h'. Stop. make: *** [libsel4] Error 2 looks like the arm directory got renamed to aarch32 and part of the build system doesn't know? $ ls /home/sysjeff/Camkes2/libs/libsel4/sel4_arch_include/ aarch32/ ia32/ Is there something simple I am missing? Thanks, Jeff -- Jeffrey L. Hieb Department of Engineering Fundamentals University of Louisville Louisville Kentucky 40292 (502) 852 0465

2 2

Issue with CAmkES tutorial
by James Hasner 21 Jan '16

21 Jan '16

All, Noticed an issue with the tutorial for creating a dataport application with CAmkES components. This issue is on https://wiki.sel4.systems/CAmkES%20Tutorial within the Makefile and Kbuild section. You titled the application "helloevent" instead of hellodataport, causing the newly created application to not be able to access the header files needed. Thanks, James

2 1

Announcing Robigalia, make seL4 applications with Rust!
by Corey Richardson 07 Jan '16

07 Jan '16

Hi all, On behalf of the Robigalia project I am pleased to announce our first public release of the core libraries for using Rust on seL4. Currently, this consists of a raw interface akin to libsel4 and a higher-level "Rustic" interface. Currently, only x86 is supported. An ARM port is in progress. We have a website: https://robigalia.org/ And a mailing list: https://lists.robigalia.org/listinfo/robigalia-dev The goal of the Robigalia project is to promote Rust as a robust choice for application development on seL4 and has the long-term goal of producing Robigo, a POSIX-compatible personality on seL4. We're in the initial stages of development. We are primarily a group of students from Clarkson University, though other contributors are starting to trickle in. Currently in-progress is a port of the tutorial from the sel4-tutorials repositories and examples of doing various things using the libraries we've created. Beyond those, we're also working on x86 platform support, right now virtio and PCI bus management. (I didn't intend on posting this for another week, to finish the tutorial and high-level library, but it was scooped on HN, so I figured I might as well) -- cmr +16032392210 http://octayn.net/

2 1

Hardware Platform for sel4 and running linux as guest os
by Julien Delange 07 Jan '16

07 Jan '16

Dear all, I am looking to purchase a board for a project that will use sel4. I have the following hardware requirements: - serial port - ethernet - potentially usb Then, I want to run linux on top of sel4 and have also some native components. In the linux partition, I would like to control the usb and potentially the ethernet. In the native components, I am planning to use the serial port (communication with other components). I thought the beagleboard black would be a good match. Does anyone tried to run linux as a guest os on this platform? If yes, is there any tutorial/example to set it up? Also, any information about how to use the serial ports and other hardware components? Also, if you have an experience with any other board (x86 or ARM - the platform does not really matter), is it possible to indicate what you would recommend? Thanks for any help or suggestion, Julien.

6 6

CAmkES 2.0.0
by Ihor Kuz 06 Jan '16

06 Jan '16

The Trustworthy Systems Team at Data61 (formerly NICTA) is pleased to announce CAmkES release 2.0.0 The new release updates CAmkES to be compatible with seL4 version 2.0.0. It also marks the transition to more frequent and regular releases, as well as switching our release process to semantic versioning, so it's easy to tell which CAmkES releases are source-compatible, or will require updates to user-level code, and also with which seL4 versions they will be compatible. You can find it at: https://github.com/seL4/camkes-tool/tree/2.0.0 And a manifest for the 2.0.0 compatible versions of the CAmkES test and example apps: https://github.com/seL4/camkes-manifest/blob/master/default-2.0.x.xml Enjoy! ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

Extending errors to always include argument numbers
by Corey Richardson 05 Jan '16

05 Jan '16

For consistency, it seems like it'd beneficial if: seL4_RangeError seL4_AlignmentError seL4_DeleteFirst seL4_FailedLookup seL4_RevokeFirst included an indication of which argument the error applies to. For some of these errors, not every call has a unique argument which can cause the erorr. This seems like a relatively straightforward change for me to get acquainted with the full process of modifying and re-verifying the kernel. Are there tradeoffs hidden here that would make this undesirable? -- cmr +16032392210 http://octayn.net/

3 2

seL4 & camkes questions
by Julien Delange 05 Jan '16

05 Jan '16

Hello, First of all, thanks for the help you provided previously. After downloading the virtual machine, everything was fine and I was able to try seL4 and camkes by using the tutorials. Thanks also for making this documentation available publicly, it definitively helps a lot to learn the principles of this operating system. I still do have some questions regarding sel4 and camkes. - About camkes, what are the thread mapping rules. How a component is transformed into one (or several) sel4 threads? Is there a mapping 1 component = 1 thread or is it possible to have multiple threads per component? - How can I find the code generated by camkes? The idl/adl code is ultimately transformed into C code and I was wondering where I could see the code. - How the real-time requirements are handled in camkes? For example, how can I specify that a component is executed periodically every XXX ms. Does the ADL supports that? - How can we specify the scheduling constraints? Can we have an ARINC653-like scheduling where every process has a fixed time slice to be executed? Since the behavior of the system can be deduced from the execution time, allocated a fixed time slice also avoid some attacks - About scheduling, what are the policies actually supported? - How timing is handled? I tried to use nanosleep() from the libc but it seems the syscall/service is not implemented. I also tried the timer example from the sel4 tutorial but when compiling, there is an error (the function timer_handle_irq needs an IRQ as a parameter). Any idea how to fix the example and more information about how time is handled? - is it possible for the OS to load and launch multiple elf at the same time or other processes must be manually started? - How capabilities and services are associated? From the example hello-2 in the sel4 tutorial, I see that a capability is declared (with vka_alloc_endpoint(&vka, &ep_object)) but I do not understand how this is associated with the message being sent between both tasks. In other words, how is it possible to associated a capability with a service. When sending or receiving a message (for example, by using seL4_SetMR(0, MSG_DATA);), there is no use of the capability. So, how the kernel can check that the thread can effectively send a message? - Is there any efforts to support standards such as ARINC653 or MILS? (even experimental) - Is there any significant/big projects that are available online and you would recommend to learn the OS and its associated libraries? Hope you do not mind such a list of questions! I really enjoy digging into the OS and it seems very interesting. Thanks for any help/comment.

4 4

DMA
by Raymond Jennings 04 Jan '16

04 Jan '16

Is it ever possible for seL4 to run on a conventional machine without an IOMMU if any code that manipulates a DMA capable device is included as trusted or does DMA automatically void any assurance? Reason for question: Running seL4 on a system without an IOMMU.

4 8

Determining when would-have-blocked
by Corey Richardson 04 Jan '16

04 Jan '16

Looking at the manual and the C impl, it seems there is no robust way to determine if a non-blocking send failed. How should an application handle this? NBRecv sets the badge register to zero when the recv "failed" - is it expected that most/all endpoints will be badged? I'm still trying to get a feel for what a system designed for this model would look like. -- cmr +16032392210 http://octayn.net/

3 2

Tutorial error
by Julien Delange 24 Dec '15

24 Dec '15

Hello, I am trying to reproduce the tutorial. I followed the steps from the slides on https://github.com/seL4-projects/sel4-tutorials/blob/master/docs/seL4Tutori… When trying to compile, I got the following error in [1]. It seems to be a warning from the compiler, so, I edit the CFLAGS in the .config and tried to compile but then got the error in [2], which then avoid any potential compilation. Is there any special setup for the compiler? I am currently using gcc 5.2.1. Thanks for any suggestion, Julien. [1] /home/julien/tmp/sel4-tutorials/stage/x86/pc99/include/vka/object.h:286:5: warning: 'seL4_AsyncEndpointObject' is deprecated (declared at /home/julien/tmp/sel4-tutorials/stage/x86/pc99/include/sel4/objecttype.h:23): use seL4_NotificationObject [-Wdeprecated-declarations] [2] /home/julien/tmp/sel4-tutorials/kernel/src/plat/pc99/machine/acpi.c:38:13: error: size of array '__assert_failed_acpi_rsdp_packed' is negative

2 2

Camkes dependencies & development environment
by Julien Delange 23 Dec '15

23 Dec '15

Dear all, First of all, sorry if this question has been asked several times already. I am currently trying to use sel4 & camkes on a debian stable. I installed all the dependencies but I am facing an error message when trying to build the tool (see below). My version of cabal is 1.20, so, version should not be an issue. After searching, it seemed that the version of ghc might be the root cause so I upgraded to testing and/or unstable but faced other issues then. My question is then what is the best development environment to use sel4 and camkes? Any special recommendation? I would like to keep my existing debian/stable as much as possible. Thanks for any help or suggestion, Julien. [parse-capDL] building... export CONFIG_CAPDL_LOADER_MAX_IRQS=256 && cabal configure && cabal build && cp dist/build/parse-capDL/parse-capDL . Resolving dependencies... cabal: The package 'capDL-tool' requires Cabal library version -any && >=1.18 but no suitable version is installed. Makefile:45: recipe for target 'parse-capDL' failed make[1]: *** [parse-capDL] Error 1 Makefile:49: recipe for target '/home/julien/tmp/camkes/stage/arm/imx31/parse-capDL/parse-capDL' failed make: *** [/home/julien/tmp/camkes/stage/arm/imx31/parse-capDL/parse-capDL] Error 2

3 3

domain problems
by ぷ风过无痕?? 23 Dec '15

23 Dec '15

Hi everyone, I'm running the RefOS project on arm kzm board. The config file is kzm_debug_defconfig. I am tring to set two domains in the RefOS by changing the CONFIG_NUM_DOMAIN parameter from 1 to 2 in this file and rebuilt RefOS. When running RefOS it gets stucked and some servers cannot be initialized.How to resolve this bug?

1 0

domain problems
by ぷ风过无痕?? 23 Dec '15

23 Dec '15

Hi everyone, I'm running the RefOS project on arm kzm board. The config file is kzm_debug_defconfig. I am tring to set two domains in the RefOS by changing the CONFIG_NUM_DOMAIN parameter from 1 to 2 in this file and rebuilt RefOS. When running RefOS it gets stucked and some servers cannot be initialized.How to resolve this bug? The full output information is in the adjunct file.

1 0

RTEMS working with seL4
by Hesham Almatary 16 Dec '15

16 Dec '15

Hi all, I got an RTEMS port working for RISC-V architecture along with seL4. This depends on my earlier seL4 port for RISC-V. RTEMS runs with support of seL4 microkernel, and it runs in Supervisor mode (on another core). seL4 application would allocate and map memory for it from its untyped memory (userspace), before off-loading it to another core. seL4 application that loads/runs RTEMS is pretty much the same as SOS. For more details (and instructions) about how to build/run the project, see the github repo of the port [1], and/or this blog post [2] [1] https://github.com/heshamelmatary/rtems-riscv [2] http://heshamelmatary.blogspot.co.uk/2015/12/rtems-port-for-risc-v-withwith… Cheers, -- Hesham

2 2

VSpace translation?
by Ben Karel 14 Dec '15

14 Dec '15

Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)?

4 4

Capability resolution depth mismatches
by Ben Karel 14 Dec '15

14 Dec '15

Hi all, Some capability resolution, such as for fault handling, winds up calling resolveAddressBits with n_bits = wordBits, and any remaining bits are ignored. In other cases, such as the destination slot for seL4_CNode_Copy, the user provides a resolution depth parameter, and the call to resolveAddressBits is mediated by lookupSlotForCNodeOp, which fails with a depth mismatch if there are any bits remaining. Individually these seem like reasonable choices, but it leads to code like this: seL4_CNode cspace_root = ...; // freshly allocated 256-slot CNode with no guard seL4_CPtr slot_for_copy = 0x23; // arbitrary slot we know is available seL4_CPtr slot_for_tcb = slot_for_copy << 24; seL4_CNode_Copy(cspace_root , endpoint_for_copy, 8, ...); seL4_TCB_Configure(..., endpoint_for_tcb, ...); I found it surprising that two different CPtrs are needed to describe the same slot! Is there a conceptual-model-explanation that doesn't involve appeal to the underlying implementation? Also: my current understanding is that the depth parameter is only needed to disambiguate indirections through CNode-containing slots. What goes wrong if the depth mismatch checks are relaxed?

2 2

Timing side channel via idle thread code?
by Brian Mastenbrook 12 Dec '15

12 Dec '15

While pulling up the Haskell model to respond to the previous question, I noted the following statement: "The idle thread's code is at an arbitrary location in kernel memory. For convenience in the Haskell model, we place it in the globals frame, but there is no need for it to be in user-accessible memory." Given that the globals frame is mapped cacheable, doesn't this lead to a potential timing side channel? Tasks would be able to determine whether the idle thread's code has been evicted from cache, which may or may not reveal something interesting about the state of the system as a whole. -- Brian Mastenbrook CTO Wearable Inc. Makers of AirStash

3 2

vspace_reserve_range_at
by Robert VanVossen 12 Dec '15

12 Dec '15

Hello, I am trying to map a device 1:1 in my root thread. When I try to reserve a range at the specific location, using the vspace_reserve_range_at() function I get the following error: ERROR:sel4utils_reserve_range_at_no_alloc:585: Range not available at 0xf8f00000, size 0x64000. Is there something that the kernel or the root task needs to do before this to make this range available for reservation? BTW, I am still using seL4 1.0. Thanks, Robbie VanVossen DornerWorks

2 1

vspace_reserve_range_at
by Robert VanVossen 12 Dec '15

12 Dec '15

Hello, I am trying to create a 1:1 physical to virtual mapping in my root thread. My first step in attempting this is to reserve the virtual address I need using the vspace_reserve_range_at() function, but I get the following error: ERROR:sel4utils_reserve_range_at_no_alloc:585: Range not available at 0xf8f00000, size 0x64000 Is there something I need to do in the kernel or in the root thread to actually allow this memory to be reserved? BTW, I am still using seL4 1.0. Thanks, Robbie VanVossen DornerWorks

1 0

verifying concurrency
by Gergely Buday 09 Dec '15

09 Dec '15

Hi there, what should I read if I want to understand the verification of concurrent programs related to the sel4 project? I have found https://ssrg.nicta.com.au/publications/papers/Daum-phd.pdf https://ssrg.nicta.com.au/publications/papers/Daum_DSW_08.pdf http://ssrg.nicta.com.au/projects/concurrency/ Are there others? Cheers - Gergely

3 2

Reminder: Microkernel-devroom CfP deadline is on this Sunday
by Jakub Jermar 07 Dec '15

07 Dec '15

Hi folks, the CfP deadline for the Microkernel devroom at FOSDEM 2016 is due this Sunday. See the original CfP [1] for information on what to do if you would like to give a talk about some microkernel-related topic. At the same time, I would like to encourage you to submit a talk proposal. It would be shame not to let the wider microkernel community know about the latest and greatest developments in your project. Lastly, please forward this reminder to whoever you think may want to give a talk in the devroom and is not among the recipients of this message. Thanks, Jakub [1] http://trac.helenos.org/wiki/Devroom2016

1 0

haskell on sel4
by Tim Newsham 05 Dec '15

05 Dec '15

I just noticed the web page says "we have Haskell sort-of running on seL4 (thanks or friends from Galois for their help), should be released in the near future" This is great news. Are you able to share any details such as when any of this will be public, what the porting strategy was (is this similar to HalVM?), what dependencies haskell compiled code requires, if there are sel4 bindings, etc? Tim

3 4

Initial Thread physical to Virtual Mapping
by Robert VanVossen 04 Dec '15

04 Dec '15

Hello, I am attempting to integrate the Xilinx drivers, provided through their SDK, with seL4 on the Zynq7000. In the root thread, I created a virtual mapping for the SD Card peripheral, and I pass that virtual address into the driver, so that it is reading and writing to it. The controller has a built-in DMA that gets used for data transfer. I created a buffer in the root thread's virtual space to pass to the DMA, but it needs a physical address. I calculated the virtual/physical offset from the physical and virtual addresses for the application that are given by the elfloader, but that didn't seem to be the correct mapping. Is there a good way to get that mapping, either from within the application itself or from the kernel before hand? Thanks, Robbie VanVossen DornerWorks

3 2

Assigning GPIO buffer to a new process
by Karl Apsite 02 Dec '15

02 Dec '15

Ahoy there! I'm working on a Zynq 7000 - ZC702 dev board. I've setup a capability associated with the GPIO buffer, and have successfully ran a small test in the root process that could read a button's state via GPIO. The next step is to send the capability to a second process so that it can read the button's state. I'm having some trouble understanding how I should go about using the IPC calls to achieve this transfer. I'll try to give a summary of my efforts, to clear up where I am, and what I've done so far. To start: I borrowed (heavily) from the 4th tutorial that established two separate processes Main: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello… App: https://github.com/seL4-projects/sel4-tutorials/blob/master/solutions/hello… I felt inclined to inform the second process about the whereabouts of the new endpoint as opposed to making an assumption as to where it was allocated. I crammed the address into the argc/argv constructs as the process starts, and it seems to be able to continue just fine. 1. Is that an OK thing to do? I understand that I shouldn't be too willing to share vital information freely between both processes, and I'm not sure if abusing argc/argv to inform the second process is appropriate here. I left the main thread in seL4_Wait(). My idea is: other processes are expected to send a message representing a command that main can respond to. Main can check the message, badge(s), and privileges as necessary, and respond with the capability if it so desires. With the capability in hand, and a tag with extracaps set to one, I was NOT able to successfully send the cap. The second process would only receive a tag with extra caps set to zero, so it must be failing somewhere along the way. I loaded the cap into the first slot using seL4_SetCap(0, my_cap) and the cap was functioning previously, so I doubt it's erroring when I send. I expect an error on the receiving end somewhere. I have NOT been able to prepare a path for a capability in the second process, and notify seL4 of the location using seL4_GetCapReceivePath(root_node, new_cap, 32). 2. How should the second process obtain a reference to its root cnode? 3. How should the second process allocate a new cnode? I think the new_process_t structure in the main process has the addresses I'm after (to obtain the root cnode at least, and maybe allow me to a new cnode?), but I don't understand the implications of informing the second process about the information in the new_process_t structure. 4. Is the new process expected to know all of that information? 5. Is there an API to establish this sort of information (along with the IPC endpoint that I had to cram into argc/argv earlier?)

2 1

seL4 2.0.0 Release Notes
by Anna Lyons 01 Dec '15

01 Dec '15

Introducing seL4 2.0.0 ====================== Version 2.0.0 introduces more consistent terminology to manual and code, as well as API and performance improvements, including to seL4's formally verified ARMv6 version. We clarified the notion of signals and notifications vs IPC, and added a new feature to the seL4 API that allows user programs to receive notifications while waiting for IPC messages. You can now also poll notification objects. Both of these changes are aimed at simplifying user-level interaction with interrupts. In addition to the new features, seL4 has become even faster than it was before, esp. in scheduling threads. The new features and performance improvements are available on all supported platforms, and are formally verified to full sel4 standards. We have also switched our release process to semantic versioning, so it's easy to tell which seL4 releases are binary-compatible, source-compatible, or will require updates to user-level code. Terminology Changes =================== IPC vs Notifications -------------------- The old terminology of "synchronous IPC" vs "asynchronous IPC" was confusing and misleading. We changed this to reflect the fact that IPC in seL4 is always synchronous and is simply referred to as "IPC", which is enabled by "endpoint" objects. The receive operation is now more appropriately called "receive". What used to be called incorrectly "asynchronous IPC" is now called Notifications, enabled by "notification" objects. Notifications are not a form of message passing, but arrays of binary semaphores, and the new terminology describes this better. The operations on them are consequently called "signal" and "wait" New Features ============ Notification binding -------------------- A notification can be bound to a thread and is referred to as the thread's bound notification object. This is a 1:1 relationship. Whenever a thread waits for an IPC on an endpoint, it will receive any signals sent to its bound notification object, with the signal flags converted into a single-word message. Threads can also explicitly wait for signals by waiting on the notification object itself. For more details, see the 2.0.0 manual Implementation improvements =========================== * introduces the bitfield scheduler: faster scheduler (Was linear in the number of runnable threads, now log n) * improved benchmarking macros: can now specify multiple benchmarking tracepoints at once added CONFIG_RELEASE_PRINTF in addition to CONFIG_DEBUG and CONFIG_RELEASE, which enables printf in a release build API Changes =========== * seL4_Recv replaces seL4_Wait on endpoints * seL4_Wait is now only used on notification objects * Async endpoint -> notification object * sync endpoint -> endpoint * seL4_Recv on an endpoint may now return signals sent to a thread's bound notification object. API Additions ============= * seL4_NotificationObject replaces deprecated seL4_AsyncEndpointObject * seL4_NotificationBits size in bits of a notification object * seL4_IRQHandler_SetNotification replaces deprecated seL4_IRQHandler_SetEndpoint * seL4_Recv replaces seL4_Wait for endpoints * seL4_Wait used on notifications * seL4_NBRecv non-blocking (polling) receive on an endpoint, which fails if there is no message waiting. Opposite of NBSend (which silently fails if there is no receiver waiting) * seL4_Poll collects any signals from a notification objects, returns zero if there are none * seL4_Signal replaces deprecated seL4_Notify * seL4_TCB_BindNotification bind a notification to a tcb * seL4_TCB_UnbindNotification unbind a notification from a tcb Deprecations ============ * seL4_AsyncEndpointObject * seL4_Notify * seL4_IRQHandler_SetEndpoint Note on Syscall names ==================== Logically there are only two operations on capabilities, send and receive, which can take opcodes specifying sup-operations. For example, the Notification operations Signal and Wait are mapped to Send and Receive, respectively. For efficiency reasons, many kernel objects use separate kernel entry points for their operations. You must not rely on either, as this can change at any time. Instead, always use the object-specific wrapper functions. User-level repositories ======================= To simply repository management we have merged many of our user level library repositories. To see the changes please compare 1.0.4.xml and 2.0.x.xml in https://github.com/seL4/seL4test-manifest Upgrade notes ============= Calls to seL4_Wait no longer return a seL4_MessageInfo_t as seL4_Wait is intended to be used on notification objects. Calls to the prior version of seL4_Wait need to be replaced with seL4_Recv. If you don't want to upgrade yet - don't worry. Both the sel4test-manifest and verification manifest repositories have manifests titled 1.0.4.xml which point to the tips of the previously released repositories before today. All library repositories have a branch called '1.0.x-compatible' which are compatible with the 1.0.4 kernel. Note that to use the new merged repositories, you must upgrade to 2.0.0. Full changelog ============== Use git log 1.0.4..2.0.0 in https://github.com/seL4/seL4 More details ============ See the 2.0.0 manual included in the release for detailed descriptions of the new features. Or ask on this mailing list! Enjoy! ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

3 3

Does seL4 support periodic thread
by ぷ风过无痕?? 27 Nov '15

27 Nov '15

Hi everyone,I have some questions about seL4's timer. I know seL4 is controlling the timer device. In the current release version, scheduling is tick-based, there's a periodic interrupt that feeds into the scheduler. I wanna know if seL4 support periodic thread. I want to implement a periodic process in Refos which is above seL4 kernel.And, if seL4 does not support periodic thread, could I modify the kernel scheduler? Does it influences formal verification? I find that Refos modifies _thread_state_t enumeration-type variables (kernel\include\object\structures.h ). Does it influences formal verification? Thank you so much!!

3 2

CAmkES-vm Configuration
by Bryan Ching 24 Nov '15

24 Nov '15

Hi, I was trying to configure the CAmkES-vm to run the vmware configuration. However, I get the following error. [apps/vm] building... /home/bryan/camkes-vm/tools/camkes/camkes.mk:125: /home/bryan/camkes-vm/build/x86/pc99/vm/camkes-gen.mk: No such file or directory [GEN] camkes-gen.mk While transforming AST: /home/bryan/camkes-vm/apps/vm/vm.camkes:4: unresolved reference to VM make[1]: *** [/home/bryan/camkes-vm/build/x86/pc99/vm/camkes-gen.mk] Error 255 make[1]: *** Deleting file `/home/bryan/camkes-vm/build/x86/pc99/vm/ camkes-gen.mk' make: *** [vm] Error 2 I have seen this error before. This time, I used the "make menuconfig" command. I go to Applications --> VMM Main Application --> Configuration. I type in "vmware" to try and configure it. When I am back on the command line, I type "make vmware_defconfig" and then "make silentoldconfig" and finally "make". Where is the camkes-gen.mk file supposed to be located? Thanks, Bryan

2 4

Destroying the Root Thread
by Robert VanVossen 20 Nov '15

20 Nov '15

Hello, I was wondering if I can safely destroy my application root thread after I have setup the capabilities and memory mappings for all of my other threads in the system? Thanks, Robbie VanVossen DornerWorks

5 8

CAmkES-vm Build Question
by Bryan Ching 17 Nov '15

17 Nov '15

Hi, I was just wondering for the CAmkES-vm, where is the Makefile to build it? Also, to clone the github repository, do I use "repo" or can I use "git clone"? Thanks, Bryan

4 7

timing
by Raymond Jennings 13 Nov '15

13 Nov '15

Where does the seL4 microkernel actually get the timing information it needs to enforce scheduling decisions? I can imagine some sort of interrupt or I/O access is required to get it from the raw hardware. How does it get from the timing hardware to the scheduling code?

4 4

CAmkES Tutorial
by Bryan Ching 12 Nov '15

12 Nov '15

Hi, I am following the tutorial for CAmkES and had a few questions. There is a part in the tutorial that says to "create a dependency entry in apps/helloworld/Kbuild for your application". How exactly do you go about creating a dependency? Do you just add it to the first line of the Kconfig file? Also, for the Makefile, I needed to include the camkes.mk file. However, it was not found in the specified directory. This is the command that I included in the Makefile: include ${SOURCE_DIR}/../../tools/common/camkes.mk Where could I get that file? Or if someone had the contents of that file, I could create it myself. Thanks, Bryan

2 6

Call for Participation: NICTA Software Systems Summer School
by Gernot Heiser 11 Nov '15

11 Nov '15

tl;dr 8–9 Feb, free event, travel subsidies for AU/NZ students CALL FOR PARTICIPATION ===================================== Fourth NICTA Software Systems Summer School http://ssrg.nicta.com.au/Events/summer/16 ===================================== Supported by: ANU and UNSW Over two days, this summer school will feature lectures by international leaders in computer systems from industry and academia, interspersed with short student talks and poster sessions. We will emphasise a friendly and informal setting where students can learn and obtain feedback from experts. Topics include operating systems, hypervisors, virtual machines, databases, compilers, language implementation, memory management and security. Research students may apply for participation by submitting a summary (of no more than half a page) on their research interests, indicating how it overlaps with the topic of the summer school. They may also indicate that they would like to give a short talk, although the organisers will only select a small number of student presentations. All attending students will be able to present a poster, and are strongly encouraged to use this opportunity to get feedback from world leaders!. We will also consider submissions from final-stage undergraduate students, post-docs or academic staff, provided they explain the benefits they expect from attendance.Supervisors of attending students are particularly welcome to attend. All submitted material must fit on a single A4 page. COST Attendance is free, but subject to invitation based on the submitted abstract. We will rarely reject an application from a student. Registration includes free lunches and coffee breaks during the summer school, as well as a dinner on the evening of the first day. A limited amount of travel support will be available for students from outside NSW and the ACT. Students requesting travel support must submit a brief justification with their application. Travel support will only be available for students from Australia and New Zealand, and will not exceed the cheapest airfare from their nearest major airport to Sydney. Funds for this are limited, and we will give priority to students likely to benefit most from the summer school, i.e. students whose research is most aligned with the topic. LOCATION The workshop and associated activities will be held in the Computer Science & Engineering building on the UNSW Kensington (main) campus in Sydney. KEY DATES Abstracts Due: Monday, 23 November, 2015, via the SSSS'16 submission site Notification: Friday, 20 November, 2015 Early applications will be notified earlier to help you with planning. ACCOMMODATION For participants from outside Sydney we are holding a limited number of inexpensive rooms at a college on campus. These must be booked (and deposit paid) by the end of November. Latecomers will have to find their own accommodations (there are other colleges and backpacker hostels nearby). ORGANISERS: Gernot Heiser (NICTA and UNSW) <gernot(a)nicta.com.au> Steve Blackburn (ANU and NICTA) <Steve.Blackburn(a)anu.edu.au> PRESENTERS (tentative): • Dr Andrew Baumann, Microsoft Research, Redmond • Prof Steve Blackburn, ANU • Prof Douglas Carmean, Oregon State University • Prof Luis Ceze, University of Washington, Seattle • Prof Kevin Elphinstone, NICTA and UNSW • Prof Alan Fekete, NICTA and Sydney University • Dr Tim Harris, Oracle Labs, Cambridge • Prof Gernot Heiser FACM, NICTA and UNSW, Sydney, Australia • Prof Tony Hosking, NICTA and ANU • Prof Gabriele Keller, NICTA and UNSW • Prof Eliot Moss FACM, UMass Amherst • Dr Karin Strauss, Microsoft Research, Redmond _______________________________________________ Csprofs mailing list Csprofs(a)core.edu.au http://core.edu.au/mailman/listinfo/csprofs_core.edu.au <a href="http://core.edu.au/mailman/listinfo/csprofs_core.edu.au"> Click here to unsubscribe </a> ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

sel4 for armv5 architecture
by vibi sreenivasan 09 Nov '15

09 Nov '15

Hi, Can any one please let me know whether sel4 is supported on armv5 ? I am specifically looking to run sel4 on arm926ej. Thanks & Best Regards Vibi

4 4

Kernel lock
by ぷ风过无痕?? 05 Nov '15

05 Nov '15

Hi, I have a question about kernel lock in seL4. I have read all the code in sel4 kernel,but I just find one file(kernel\include\arch\ia32\kernel\lock.h) related to the lock in the sel4. I also find that the lock here is used to debug.So I think there does not exist a lock in the sel4kernel.But if the lock really does not exist ,that means the sel4 kernel is non-reentrant, does it? does seL4 really not need the lock ? ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Wed, Nov 4, 2015 01:33 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 18, Issue 4 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: How is network stack implemented in sel4 (Tim Newsham) 2. Re: How is network stack implemented in sel4 (Raymond Jennings) 3. Re: How is network stack implemented in sel4 (Gernot Heiser) 4. Re: How is network stack implemented in sel4 (Raymond Jennings) 5. Re: How is network stack implemented in sel4 (Gernot Heiser) 6. Re: How is network stack implemented in sel4 (Yuxin Ren) ---------------------------------------------------------------------- Message: 1 Date: Mon, 2 Nov 2015 15:48:02 -1000 From: Tim Newsham <tim.newsham+sel4(a)gmail.com> To: Yuxin Ren <ryx(a)gwmail.gwu.edu> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGSRWbhESa8qAwNzWjVKzo7Unh=GeGWNTVTBACXbkMA=TbsVQg(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" seL4 does not provide a network stack or even network device drivers. An OS on top of seL4 would have to provide their own drivers and stack and is free to put them in a single server or in different servers and choose how to communicate between them. On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren <ryx(a)gwmail.gwu.edu> wrote: > Hi, > > I have a few questions about network stack in sel4. > > Is network stack implemented in the kernel or user level? > If in user level, are different protocols (IP/TCP) implemented in a > single server or different servers? > If in different servers, how do they communicate with each other? > > Is there any example code to show how to use network? How to send and > receive TCP or UDP packets? > How can I set up the network environment on bare metal machine? Is > there documentation or instruction? > > Thanks a lot! > Yuxin > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151102/34f3782d/attachmen…> ------------------------------ Message: 2 Date: Mon, 2 Nov 2015 17:58:11 -0800 From: Raymond Jennings <shentino(a)gmail.com> To: Tim Newsham <tim.newsham+sel4(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGDaZ_qNsZd+VcH8wwvPcjcq_mQR=xefgKMaR45-L4SO9VBrLQ(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" So basically L4 grants IO caps to the network card's io ports to whatever task acts as the network driver, and it's the driver task's job to bang on the card's I/O and hook up with whatever other tasks represent packet/protocol/whatever layers of the ISO 7 layer stack. On Mon, Nov 2, 2015 at 5:48 PM, Tim Newsham <tim.newsham+sel4(a)gmail.com> wrote: > seL4 does not provide a network stack or even > network device drivers. An OS on top of seL4 > would have to provide their own drivers and stack > and is free to put them in a single server or in > different servers and choose how to communicate > between them. > > > On Mon, Nov 2, 2015 at 2:38 PM, Yuxin Ren <ryx(a)gwmail.gwu.edu> wrote: > >> Hi, >> >> I have a few questions about network stack in sel4. >> >> Is network stack implemented in the kernel or user level? >> If in user level, are different protocols (IP/TCP) implemented in a >> single server or different servers? >> If in different servers, how do they communicate with each other? >> >> Is there any example code to show how to use network? How to send and >> receive TCP or UDP packets? >> How can I set up the network environment on bare metal machine? Is >> there documentation or instruction? >> >> Thanks a lot! >> Yuxin >> >> _______________________________________________ >> Devel mailing list >> Devel(a)sel4.systems >> https://sel4.systems/lists/listinfo/devel >> > > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151102/24c77488/attachmen…> ------------------------------ Message: 3 Date: Tue, 3 Nov 2015 03:05:37 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: Raymond Jennings <shentino(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <E4936E28-39AA-44E9-B202-FB37401E22F9(a)nicta.com.au> Content-Type: text/plain; charset="us-ascii" On 3 Nov 2015, at 12:58 , Raymond Jennings <shentino(a)gmail.com<mailto:shentino@gmail.com>> wrote: So basically L4 grants IO caps to the network card's io ports to whatever task acts as the network driver, and it's the driver task's job to bang on the card's I/O and hook up with whatever other tasks represent packet/protocol/whatever layers of the ISO 7 layer stack. More precisely: seL4 hands all rights to all resources to the initial process, whose job is then to initialise the desired system. It would be that process that hands caps to drivers etc. Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151103/a3a78ad4/attachmen…> ------------------------------ Message: 4 Date: Mon, 2 Nov 2015 19:46:14 -0800 From: Raymond Jennings <shentino(a)gmail.com> To: Gernot Heiser <gernot(a)nicta.com.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAGDaZ_q=98W1c91dFMNN+zL4P1p3+iE-ETAMbfOc51ybxvFwrg(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement? On Mon, Nov 2, 2015 at 7:05 PM, Gernot Heiser <gernot(a)nicta.com.au> wrote: > On 3 Nov 2015, at 12:58 , Raymond Jennings <shentino(a)gmail.com> wrote: > > > So basically L4 grants IO caps to the network card's io ports to whatever > task acts as the network driver, and it's the driver task's job to bang on > the card's I/O and hook up with whatever other tasks represent > packet/protocol/whatever layers of the ISO 7 layer stack. > > > More precisely: seL4 hands all rights to all resources to the initial > process, whose job is then to initialise the desired system. It would be > that process that hands caps to drivers etc. > > Gernot > > ------------------------------ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20151102/528f68fb/attachmen…> ------------------------------ Message: 5 Date: Tue, 3 Nov 2015 03:54:58 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: Raymond Jennings <shentino(a)gmail.com> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <418AEC27-5994-4EAB-8AEB-2D12A7D031A7(a)nicta.com.au> Content-Type: text/plain; charset="utf-8" > On 3 Nov 2015, at 14:46 , Raymond Jennings <shentino(a)gmail.com> wrote: > > So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement? Caps are like keys: they authenticate access. The kernel doesn?t need them for its own purposes. However, our integrity and confidentiality proofs show that the kernel will not on its own access user memory, unless on behalf of a thread who demonstrates that it is authorised by presenting an appropriate caps. Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------ Message: 6 Date: Tue, 3 Nov 2015 12:32:44 -0500 From: Yuxin Ren <ryx(a)gwmail.gwu.edu> To: Gernot Heiser <gernot(a)nicta.com.au> Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> Subject: Re: [seL4] How is network stack implemented in sel4 Message-ID: <CAAKbDrdNod7_M8h+ufyZCkdJ9bDmKeXNpRD-PpKMSCYUnwpLQQ(a)mail.gmail.com> Content-Type: text/plain; charset=UTF-8 Thank you all. But are there any projects on top of sel4 microkernel which implement network functionality? I don't think I need to build the whole network stack from bare metal. It is best for me to just refer some existing projects and run simple network application on top of it. Yuxin On Mon, Nov 2, 2015 at 10:54 PM, Gernot Heiser <gernot(a)nicta.com.au> wrote: > >> On 3 Nov 2015, at 14:46 , Raymond Jennings <shentino(a)gmail.com> wrote: >> >> So the kernel itself doesn't actually "own" any capabilities, just does the bookkeeping and enforcement? > > Caps are like keys: they authenticate access. The kernel doesn?t need them for its own purposes. However, our integrity and confidentiality proofs show that the kernel will not on its own access user memory, unless on behalf of a thread who demonstrates that it is authorised by presenting an appropriate caps. > > Gernot > > ________________________________ > > The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 18, Issue 4 ************************************

4 4

How is network stack implemented in sel4
by Yuxin Ren 04 Nov '15

04 Nov '15

Hi, I have a few questions about network stack in sel4. Is network stack implemented in the kernel or user level? If in user level, are different protocols (IP/TCP) implemented in a single server or different servers? If in different servers, how do they communicate with each other? Is there any example code to show how to use network? How to send and receive TCP or UDP packets? How can I set up the network environment on bare metal machine? Is there documentation or instruction? Thanks a lot! Yuxin

5 7

Running CAmkES Sample Application on Sabre Lite Board
by Bryan Ching 02 Nov '15

02 Nov '15

I was following the CAmkES "Getting Started" tutorial on the seL4 website and followed all the instructions. Here is the link: https://sel4.systems/Info/CAmkES/GettingStarted.pml I managed to get the sample application to run in QEMU (Quick Emulator) like the instructions said. I tried loading the sample application onto the Sabre Lite Board through tftp booting using minicom. However, once I try to boot the .elf file, it displays the memory address and nothing else happens. Is there any configuration file that I need to change to make the sample application run on my Sabre Lite Board? Or is there something else that I am missing? Thanks, Bryan

3 6

Fwd: FOSDEM 2016 - Microkernel devroom CfP
by Martin Decky 28 Oct '15

28 Oct '15

Dear all, I am forwarding the Call for Participation of the Microkernel devroom at FOSDEM 2016. The original announcement did not pass the mailing list gatekeeper for some reason. Martin Decky -------- Forwarded Message -------- Subject: FOSDEM 2016 - Microkernel devroom CfP From: Jakub Jermar <jakub(a)jermar.eu> FOSDEM 2016 - Microkernel devroom CALL FOR PARTICIPATION The developers of several free and open-source microkernel-based operating systems will meet at FOSDEM 2016 [1] in Brussels, Belgium and will share a developer room. 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: * project introductory and status update talks, demos * architecture, subsystem and components' design * hardware and device drivers * tools, languages and toolchains * development, debugging, testing and release engineering * best practices and learning from mistakes * trends and challenges * community and life with a microkernel project Please use the Pentabarf [2] system to submit your proposals. You do not need to create a new account if you already have one. When in doubt, please use the devroom mailing list [3]. The deadline for your CfP submissions is on 2015-12-13. Make sure to include the following in your proposal: * title of your talk * abstract (one or two paragraphs) * your full name * your short bio * a picture of yourself * duration of your talk The official devroom schedule (along with the accepted talks) will be announced on 2015-12-18 in the devroom's mailing list and the speakers will be notified via e-mail. The schedule will also be published on the FOSDEM web and in the FOSDEM booklet. The devroom will take place on Saturday of January 30, 2016 at ULB Solbosch Campus in Brussels, Belgium [4]. 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 its inception in 2012 the Microkernel devroom has been part of each FOSDEM conference. It has become a sort of an institutionalized tradition since then. To this date over a dozen projects have participated in one way or another, delivering forty talks and other contributions in total. The goal of the Microkernel devroom has been to bring the various projects together and let them share ideas, cross-pollinate and socialize. Each year the devroom is organized by one of the projects based on a system of rotating presidency from the pool of projects that opt in. In 2016 it is HelenOS' turn again. Social events It has become a tradition that the microkernel projects dine together somewhere in downtown Brussels after the devroom closes. The year 2016 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 2015-10-23 CfP 2015-12-13 CfP deadline 2015-12-18 Devroom schedule published, speakers notified 2016-01-30 Microkernel devroom takes place 2016-01-30 Microkernel family dinner Links [1] http://fosdem.org/2016 [2] https://penta.fosdem.org/submission/FOSDEM16 [3] https://lists.fosdem.org/listinfo/microkernel-devroom [4] https://fosdem.org/2016/practical/transportation/

1 0

Support for multiple levels of derived capabilities?
by Mark Jones 22 Oct '15

22 Oct '15

I have a question about the way that derived capabilities are handled in seL4. I'm posting here in the hope that somebody might be able to share some insights about this part of the design. As I understand it, early versions of seL4's Mint operation allowed multiple derived levels of capabilities. (I'm thinking, in particular, of the description of Capability Derivation Trees, or CDTs, on Pages 36-38 of Dhammika Elkaduwe's thesis.) This, for example, would make it possible to construct a system with multiple threads, A, B, and C, each holding a capability to the same object where the capability in C is a CDT child of the capability in B, which in turn is a CDT child of the capability in A. In this scenario, B would have authority to revoke the capability in C, including any further CDT children that C had created, but it wouldn't typically have authority over other children of the original capability in A. So far as I can tell, this is not possible in the current version of seL4. Specifically, the reference manual (API version 1.3, Page 11) indicates that "Ordinary original capabilities can have one level of derived capabilities" and that "Further copies of these derived capabilities will create siblings". In the scenario above, this suggests that the capabilities in B and C would be siblings and that there would be no easy way for B to track any additional sibling copies that C might have created. Can someone provide background about why this change was made? I've seen that Dhammika had a working implementation of the original design, and although it was still technically limited to 128 levels, this was not found to be an issue in practice. But perhaps there were security concerns or problems with verification? Or maybe people who worked with the original system found that it wasn't useful in practice, or that it was hard to use effectively? Or maybe I've just misunderstood some aspect of the above? Thanks and best wishes, Mark

4 5

imx6 + libethdrivers + lwip
by Andrea Sorbini 10 Oct '15

10 Oct '15

Hello, I have been experimenting on the SabreLite imx6 board and the network driver provided by libethdrivers. I've been successful in getting it to work "out of the box" and, testing with a simple UDP echo client running on Linux, I've verified that I can send and receive small UDP messages as long as they were not fragmented. I immediately noticed that the fragmentation performed by Linux was different than the one performed by lwip on seL4. Lwip was successfully reassembling a message fragmented in two, but it wasn't fragmenting it when sending it back out. The driver reports an MTU of 1536 and this is likely the reason for lwip not to perform output fragmentation. Hacking the driver slightly, I had it report an MTU of 1500 to lwip, while using the 1536 value internally to allocate buffers. This has allowed me to successfully receive and send UDP messages of up to ~2950 bytes (ie. under 3 frames). When size is increased above that amount, lwip starts behaving "suspiciously" and I can only see the two first two fragments going out, while the third one is never sent (causing the linux host to timeout on the IP reassembly). Debugging the driver, it seems the third fragment is never actually written Has anybody had any experience in getting bigger UDP messages across? Any suggestions on how to enable it if not? Thanks, -Andrea tl;dr: Got UDP working on imx6 with libethdrivers+lwip, can only send up to 2950 bytes, would like to send more, help needed. -- Andrea Sorbini Software Engineer asorbini(a)rti.com +1.408.990.7475 www.rti.com RTI - Your systems. Working as one.

1 0

Camkes MMIO Driver Failed to find device frame
by Jeff Hieb 03 Oct '15

03 Oct '15

I am working on a UART device driver in camkes for AM335x. When I load the image on the board I get this error: Creating object frame_drv_group_bin_42 in slot 596, from untyped 1f6... device frame, paddr = 0x48022000, size = 12 bits capDL-loader :: << Error: Failed to find device frame at paddr = 0x48022000 >> I am reasonably confident the address is correct, (https://github.com/seL4/libplatsupport/blob/master/plat_include/am335x/plat…) Looking at the source It seems capDL-Loader wants to find this device frame in bootinfo https://github.com/seL4/capdl-loader-app/blob/master/src/main.c#L731 Any help on how capDL-loader builds bootinfo would be appreciated. Jeff -- Jeffrey L. Hieb Department of Engineering Fundamentals University of Louisville Louisville Kentucky 40292 (502) 852 0465

4 4

We're hiring!
by Gernot Heiser 29 Sep '15

29 Sep '15

Want to be part of the seL4 team and be *paid* for having fun? We’re hiring: - proof engineers: https://ssrg.nicta.com.au/jobs/proof-engineers2015 - OS engineers: https://ssrg.nicta.com.au/jobs/OS-engineers2015 - researchers/postdocs: https://ssrg.nicta.com.au/jobs/OS-researchers2015 Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

libsel4cspace and IPC
by Will Korteland 27 Sep '15

27 Sep '15

Hi, I'm trying to implement a "create endpoint" syscall as a continuation of my AOS project last year. I'm using the following code to create and endpoint in the current threads's cspace (using libsel4cspace): https://gist.github.com/anonymous/8294aa47ad351e4d4066 When this code runs, seL4 prints the following during the cspace_ut_retype_addr call: <<seL4 [decodeUntypedInvocation/128 Tffeead00 @b330]: Untyped Retype: Invalid destination address.>> This error comes from inside libsel4cspace, specifically where it calls seL4_Untyped_RetypeAtOffset(). I've read the libsel4cspace documentation and enabled CSPACE_DEBUG, but nothing from the output looks amiss (I'm not an expert though, and I can post the relevant debug output). Have I done anything wrong in the code above? Thanks, - Will

1 0

How to modify timer server in refos
by ぷ风过无痕?? 27 Sep '15

27 Sep '15

I want to transplant the Refos into the ZYNQ board,Now everything is ok,except the timer server. Could you give me some advices about how to modify timer server's file device_timer.c . ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Thu, Sep 24, 2015 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 16, Issue 12 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Reminder: Developers Day registration closes Monday (Gernot Heiser) ---------------------------------------------------------------------- Message: 1 Date: Wed, 23 Sep 2015 05:58:01 +0000 From: Gernot Heiser <gernot(a)nicta.com.au> To: seL4 <devel(a)sel4.systems> Subject: [seL4] Reminder: Developers Day registration closes Monday Message-ID: <FD16E4F0-FD7A-494C-9432-AF1C4903E750(a)nicta.com.au> Content-Type: text/plain; charset="us-ascii" Details at https://sel4.systems/Community/Devdays/ Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 16, Issue 12 *************************************

2 1

Reminder: Developers Day registration closes Monday
by Gernot Heiser 23 Sep '15

23 Sep '15

Details at https://sel4.systems/Community/Devdays/ Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

1 0

Caught cap fault in send phase at address 0x0
by Andrew Shruhan 22 Sep '15

22 Sep '15

Hello, I am attempting to create a simple program opening up a serial port on the Sabrelight. Attached is the source code and below is the console output. On other sel4 blogs with this problem uboot may have been the issue. I have used the u-boot as discribed on the supported hardware->sabrelight page with the same outcome. Any help would be appreciated. Thanks, U-Boot 2009.08-dirty (Sep 17 2015 - 14:58:04) CPU: Freescale i.MX6 family TO1.2 at 792 MHz Temperature: 36 C, calibration data 0x56a4bc7d mx6q pll1: 792MHz mx6q pll2: 528MHz mx6q pll3: 480MHz mx6q pll8: 50MHz ipg clock : 66000000Hz ipg per clock : 66000000Hz uart clock : 80000000Hz cspi clock : 60000000Hz ahb clock : 132000000Hz axi clock : 264000000Hz emi_slow clock: 132000000Hz ddr clock : 528000000Hz usdhc1 clock : 198000000Hz usdhc2 clock : 198000000Hz usdhc3 clock : 198000000Hz usdhc4 clock : 198000000Hz nfc clock : 24000000Hz Board: MX6Q-SABRELITE:[ POR] Boot Device: I2C I2C: ready DRAM: 1 GB MMC: FSL_USDHC: 0,FSL_USDHC: 1 JEDEC ID: 0xbf:0x25:0x41 Reading SPI NOR flash 0xc0000 [0x2000 bytes] -> ram 0x276009b8 SUCCESS *** Warning - bad CRC, using default environment In: serial Out: serial Err: serial Net: got MAC address from IIM: 00:19:b8:01:fd:6d FEC0 [PRIME] Hit any key to stop autoboot: 0 mmc1 is current device -- Trying fat on SD 1, partition 1 reading sel4-image 344564 bytes read ## Starting application at 0x20000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10 paddr=[20000000..2004c01f] ELF-loading image 'kernel' paddr=[10000000..10031fff] vaddr=[e0000000..e0031fff] virt_entry=e0000000 ELF-loading image 'hello-1' paddr=[10032000..1003ffff] vaddr=[8000..15fff] virt_entry=803c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x0 with status 0x7 in thread 0xffdfd900 "rootserver" at address 0x804 -- -Andrew Andrew P. Shruhan Research and Development Engineer III DocBox, Inc. 320 Nevada St Newton MA, 02460 Work: 857-598-2819 ext. 117 www.docboxmed.com <http://www.docboxinc.com/>

2 1

Question about upstream
by Harish Pillay 9v1hp 20 Sep '15

20 Sep '15

Hi. I came across seL4 yesterday and have not spent too much time on it. I have not found anything specific to my question in the FAQ yet, so I am posing it here: has the work done by seL4 been accepted upstream? If not, any reason why it has not been accepted yet? Thanks. Harish

2 2

Roadmap and Developers Day announcements
by Gernot Heiser 16 Sep '15

16 Sep '15

Dear developers, Those of you who aren’t (yet) subscribed to announce(a)sel4.systems might have missed this: we announced - the seL4 roadmap: https://sel4.systems/pipermail/announce/2015/000007.html - the second Developers Day: https://sel4.systems/pipermail/announce/2015/000008.html Gernot ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

2 1

Mysterious Label Before sysenter
by Corey Richardson 16 Sep '15

16 Sep '15

For example, here: https://github.com/seL4/seL4/blob/master/libsel4/arch_include/x86/sel4/arch… What use is the label? Does it align the instruction or do other ABI-important things? -- /cmr

2 2

x86-64
by Raymond Jennings 14 Sep '15

14 Sep '15

Does seL4 support x86-64 with 64-bit virtual address spaces?

2 2

Adding a Rust kernel interface generator
by Corey Richardson 11 Sep '15

11 Sep '15

Hello, As part of the robigalia [0] project I must create a Rust interface to the kernel. I'm using the XML from kernel/libsel4 and have been creating a "new" generator by copying the existing Python scripts. Should I send a patch upstream once this is suitably complete, or should I maintain this completely externally? [0] - https://github.com/robigalia -- /cmr

2 2

how to detect the number of CPUs in the system
by 杰尔米 01 Sep '15

01 Sep '15

Hi all, i want to get the number of CPUs in the system and how many cores in one CPU. how to do that? Thanks! Jeremy Li

3 2

The pt/pd/as abstraction vs software TLBs
by Raymond Jennings 01 Sep '15

01 Sep '15

Hey, quick question. This is just hypothetical, but would making management of pagetables/pagedirectories a low level literal operation hurt seL4's portability to other architectures that might not even use page tables? I could be mistaken but I think there's some archs out there that only have software TLBs (openrisc IIRC among them) Please forgive me if I'm mistaken but my recent question about memory abstraction reminded me about this.

3 2

sharing memory between processes
by Raymond Jennings 01 Sep '15

01 Sep '15

Is there an easy way for one task to share address space with another task directly or does it have to go through the kernel/os and be emulated? I noticed that support for mapping memory is mostly low level assignment of physical frames to virtual frames via page tables, unlike Mach which uses memory objects.

6 7

virtual memory abstraction
by Raymond Jennings 31 Aug '15

31 Aug '15

I noticed that unlike mach, L4 does not directly manage virtual memory, but instead farms out address space, page directory, and page table capabilities to userspace and lets userspace decide what pages to map and where. Does this imply that virtual memory abstraction is userspace responsibility?

2 1

Port I/O - Permissions Question
by Josef M. 25 Aug '15

25 Aug '15

Hi, I'm experimenting with some x86 code that involves reading from I/O ports. I noticed--much to my surprise--that I don't have to use seL4_IA32_IOPort_In8() to read from a port; my program works just as fine using the "in" assembly statement directly, without any caps. The TSS segment limit is initialized with 0x67 https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L158 and the "I/O Map base address" is initialized with 0 (zero) https://github.com/seL4/seL4/blob/master/src/arch/x86/kernel/vspace.c#L43 I believe the result is that ring 3 programs can access I/O port addresses below 0x388 (0x67 * 8) without triggering a protection violation. So my question is: Shouldn't capabilities be required for all ports? Or what what is the reason or motivation behind this? Thanks, Josef

2 1

Running Linux atop sel4
by Sebastian Lau 24 Aug '15

24 Aug '15

On the sel4.systems website, it says that the site is served by the Apache web server on Linux atop sel4. How does that work and could you operate the Linux middleware just on top of sel4, maybe something like mer?

1 0

Roadmap?
by Raymond Jennings 22 Aug '15

22 Aug '15

I remember awhile ago that someone was going to post the roadmap in response to my accessed/dirty bit suggestion...but I haven't seen it yet.

2 1

Some questions about seL4 operating system
by Qing Wei 22 Aug '15

22 Aug '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

3 4

Some comments.
by Mehdi Amiri 17 Aug '15

17 Aug '15

Hi, Thank you for all your efforts and time. I believe the user community is the main success key for all open source projects. Many users and researchers, do not have enough time to read, download and evaluate all the source code in order to investigate a system to see if it is suitable for their research or usage. Usually they will go for clean systems which are easy to use, simple to understand, well documented and have a strong community beside the commercial support to ask and get help in case they had a problem. Here are some comments which may help to increase the number of users and developers for seL4: A) I suggest to add some howtos to the website. It's better to be a wiki like system so other individuals, researchers and students can help in writing some titles. Some interesting topics (at least for me as a beginner in micro-kernel) could be: 1- Running Linux/Android on top of seL4. 2- Writing a simple user application with a use case (not just the SOC). 3. Examples on real-time application. 4- Writing a service (could be a device driver, file-system, etc) for seL4. 5- Documents on using possible run-times like Genode. 6- Documents or case studies on porting an opensource software from Linux or POSIX based system to directly run om seL4. B) Providing ready to use download binary images for supported platforms can also accelerate growth of community. C) A research areas page which can suggest researchers some ideas to chose a title and do their research to expand seL4 could also be useful. Ideas like rump-kernels, lib-OS, visualization (x86/ARM), etc seems to be possible research titles on seL4. I have seen the https://sel4.systems/GettingStarted/ page and I think other than CAmkES, ports and Qubes there could be many more titles. D) I know the major development platform of seL4 has been the Arm architecture, but optimizing the code to utilize the x86 architecture including virtualization can also bring a lot of attention to this project to use seL4 as a replacement for Linux-KVM and Xen in the cloud, IoT or real time systems when stability and security is a matter. Also please note, the archive of both development ( https://sel4.systems/pipermail/devel/) and announcements ( https://sel4.systems/pipermail/announce/) mailing lists are not accessible trough the website. I'm an OS researcher and a senior system engineer (mostly Linux) with a limited time, but I can help in some parts if you think it may be useful. Thank you again! Best Regards, Mehdi

2 1

other communications
by Raymond Jennings 17 Aug '15

17 Aug '15

Is there a mailinglist or forum anywhere for people interested in using seL4? I realized this is a dev list and may not be the right place to ask technical supportr questions.

2 1

Detecting dirty/accessed page tables
by Raymond Jennings 15 Aug '15

15 Aug '15

Hey I'm just curious...how do you detect if a memory page mapped by a page table has been written to or accessed? I imagine if you're writing a filesystem task, such information would help you know when to flush data back to disk or which pages to keep around if things get tight. I hope this isn't a stupid question.

5 16

U-boot help sabrelite
by Andrew Shruhan 12 Aug '15

12 Aug '15

Hi, I am attempting to follow the tutorial booting from SPI for the sabrelite https://sel4.systems/Hardware/sabreLite/ when booting I obtain this output and am not able to run "run bootsel4_mmc" U-Boot 2009.08-dirty (Jun 27 2013 - 16:26:46) CPU: Freescale i.MX6 family TO1.2 at 792 MHz Temperature: 36 C, calibration data 0x56a4bc7d mx6q pll1: 792MHz mx6q pll2: 528MHz mx6q pll3: 480MHz mx6q pll8: 50MHz ipg clock : 66000000Hz ipg per clock : 66000000Hz uart clock : 80000000Hz cspi clock : 60000000Hz ahb clock : 132000000Hz axi clock : 264000000Hz emi_slow clock: 132000000Hz ddr clock : 528000000Hz usdhc1 clock : 198000000Hz usdhc2 clock : 198000000Hz usdhc3 clock : 198000000Hz usdhc4 clock : 198000000Hz nfc clock : 24000000Hz Board: MX6Q-SABRELITE:[ POR] Boot Device: I2C I2C: ready DRAM: 1 GB MMC: FSL_USDHC: 0,FSL_USDHC: 1 JEDEC ID: 0xbf:0x25:0x41 Reading SPI NOR flash 0xc0000 [0x2000 bytes] -> ram 0x276009b8 SUCCESS In: serial Out: serial Err: serial Net: got MAC address from IIM: 00:19:b8:01:fd:6d FEC0 Hit any key to stop autoboot: 0 AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! Unknown command 'load' - try 'help' SATA device 1: unknown device Unknown command 'load' - try 'help' Card did not respond to voltage select! mmc0(part 0) is current device Unknown command 'load' - try 'help' mmc1 is current device Unknown command 'load' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'load' - try 'help' Unknown command 'usb' - try 'help' Unknown command 'load' - try 'help' 6x_bootscript not found serial console at 115200, 8N1 details at http://boundarydevices.com/6q_bootscript AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! AHCI 0000.0000 1 slots 1 ports ? Gbps 0x0 impl SATA mode flags: No port device detected! Card did not respond to voltage select! mmc0(part 0) is current device expose mmc drive 0 over USB Unknown command 'ums' - try 'help' Card did not respond to voltage select! no block devices found ERTOS MX6Q SABRELITE U-Boot > -- -Andrew Andrew P. Shruhan Research and Development Engineer III DocBox, Inc. 320 Nevada St Newton MA, 02460 Work: 857-598-2819 ext. 117 www.docboxinc.com

2 2

Upstream seL4/RISC-V work?
by Hesham ALMatary 10 Aug '15

10 Aug '15

Hi, The seL4/RISC-V port is now working on Spike (emulator), Rocket Chip (FPGA), and jor1k (online emulator). I've also written a recent blog post how to build/run the port with SOS project [1] from my repos). The code is pretty much like the ARM port, and following the same bootstrapping procedure (more on this on my blog). MMU code provides 4KiB and 4MiB pages (like IA-32). I'd like to ask if there are special requirements to upstream this work: * All libraries that are target-dependant. * seL4 microkernel. * Tools (elf loader, build system). * SOS project? I understand it won't be an easy process because this work is the first "foreign" code that big, of course apart from formal verification. But it wouldn't hurt to ask. [1] http://heshamelmatary.blogspot.co.uk/2015/07/howto-build-and-run-sel4-on-ri… Best, -- Hesham

4 4

Porting Linux driver into Sel4
by Shabnam Engineer 09 Aug '15

09 Aug '15

HiI have a question about porting Linux drivers in Sel4.Can I port Linux drivers into Sel4? I know that DDEKit provides such functionality for L4-based systems and I could find the implementation of that in fiasco.OC microkernel, but I can not find same works for Sel4. I want to implement Sel4 on a board and test some features, At first I want to be sure that if I need a driver for our special tests and the Sel4 does not support that, Could I choose it from Linux drivers and port it to Sel4 microkernel? Thank you for your considering my question.Regards,Shabnam

1 0

Wandboard Port
by Robert Kaiser 30 Jul '15

30 Jul '15

Hello, in an attempt to familiarize myself with the seL4 code, I am trying to "port" it to the Wandboard (see www.wandboard.org) This should be an easy task for a beginner (thought I) since the board is very similar to the SabeLite, and seL4 is already running well on that board. I have access to a SabreLite and a Wandboard Quad, both (according to U-boot) have the same revision of the iMX6 SoC installed. Differences between the Sabre and the Wand I have noticed so far are: - 2GB of RAM from (0x10000000 to 0x90000000) on the Wand (Sabrelite has 1GB) - Wand uses UART1 for debug output, Sabrelite: UART2 I compiled an sel4test project where I adapted the UART port in kernel/include/plat/imx6/plat/machine/devices.h and elfloader/src/arch-arm/plat-imx6/platform.h and the RAM size in kernel src/plat/imx6/machine/hardware.c. When I boot this system, I get: Jumping to kernel-image entry point... Bootstrapping kernel Caught cap fault in send phase at address 0x0 while trying to handle: vm fault on data at address 0x9f11c2e0 with status 0x1c06 in thread 0xffdfad00 at address 0x13294 (Needless to say, "all is well in the universe" on the SabreLite... ) What is not shown here are a ton of other debug messages which I have added to convince myself that kernel initialization completes as expected. The crash seems to happen upon entry into user code. The address 0x13294 is the virtual address of the entry point: $ nm build/arm/imx6/sel4test-driver/sel4test-driver.bin | grep 13294 00013294 T _sel4_start I suspect that this fault happens on opcode fetch, because the user code is not properly mapped when invoked. Does "status 0x1c06" confirm this? If so, *should* the code be mapped at this point or are these mappings expected to be installed "on demand", i.e. through page fault handling? Thanks for any help... Robert -- Robert Kaiser Computer Engineering RheinMain University of Applied Sciences

3 14

Happy Birthday, Developers!
by Gernot Heiser 29 Jul '15

29 Jul '15

Hi everyone, Today is the anniversary of the open-sourcing of seL4. At NICTA we’re celebrating, I hope you’ll virtually join us ;-) Let me add that I quite enjoy this mailing list. Traffic has a high signal-noise ratio (apologies for degrading it with this message ;-) people generally seem to know what they are doing, and the community is clearly growing. Presently there are over 300 addresses on the list. Many thanks from all of us at NICTA, and keep it up! Gernot [cid:1374281D-B193-431C-AA3F-D6EE049C461A@keg.ertos.in.nicta.com.au] ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

2 1

CMake and seL4
by Wink Saville 29 Jul '15

29 Jul '15

In my opinion the edit/compile/test loop with the standard build system seeed slow, so I thought I'd try to see if CMake might be any better. Here <https://github.com/winksaville/sel4-newlibs-manifest> is repo manifest which uses CMake for building my sel4-newlibs helloworld application and I'm happy to report there is some improvement. For a "clean" build it is about 2x faster, 8 seconds as compared to 14 seconds. And for a small change to apps/helloworld/src/main.c it is 20x faster, 0.3 seconds as compared to 7 seconds. Is there any interest in using CMake or other build system to reduce the builds times for seL4? -- Wink

2 2

seL4 runs on Rocket Chip (RISCV/FPGA)
by Hesham ALMatary 18 Jul '15

18 Jul '15

Hi all, This is a status update of the seL4/RISC-V project. It can run now on Rocket Chip (FPGA) and jor1k (online emulator), for more details have a look at this link [1]. [1] http://heshamelmatary.blogspot.co.uk/2015/07/sel4-runs-on-rocket-chip-riscv… Thanks, -- Hesham

1 0

Some questions about seL4 operating system
by Qing Wei 16 Jul '15

16 Jul '15

Hi, I am a beginner to seL4 as well as microkernel, and very interested in it. I think it is great in terms of its minimality and formally verified security. However, I have some questions about it, (1) How is its performance compared to other monolithic kernel, say, Linux. Could it make use of multicore, multiprocessor to enjoy the performance scalability? (2) How is its ecosystem, fox example, how to support new hardware, does it need write the driver from scratch or could it make use of Linux driver? And how to write application on it, or, could it run Linux application without modification? (3) How is its virtualization support, could it run Linux vm, and does it need any modification to the guest os? Cheers, Qing Wei

1 0

what are these comments meaning
by Pei.XiLong(裴喜龙) 15 Jul '15

15 Jul '15

Hi, In recent seL4 commit https://github.com/seL4/seL4/commit/67d8d041de0c435a1cc59ef8c237be6e39beb1c6 , A lot of comments like these: /** AUXUPD: "(True, ptr_retyps (2 ^ (unat \<acute>userSize)) (Ptr (ptr_val \<acute>regionBase) :: cte_C ptr))" */ /** GHOSTUPD: "(True, gs_new_cnodes (unat \<acute>userSize) (ptr_val \<acute>regionBase) (4 + unat \<acute>userSize))" */ have been added into source code, What is their meaning? I don't know isablle, and just know a little about haskell. thanks! Xilong Pei Tongji University 2015/7/14

2 1

Raspberry Pi version for learning about seL4
by Simon Apperley 14 Jul '15

14 Jul '15

Hi, I wondered if there was any news on the Raspberry Pi 2 port of seL4 which I saw mentioned when I did a search? I am interested in using the Raspberry Pi to learn about seL4 - not as a target for a full system (as I know there is an issue with trusting the boot mechanism). I just thought it would be a nice platform to use to get my head around seL4 and experiment with virtualising Linux and maybe Android? Simon Sent from my iPad

2 1

reply: This checkin cause a build error
by XilongPei(裴喜龙) 13 Jul '15

13 Jul '15

Hi, Adria, I have fix this build error, it is because I use an old version of apps/sel4test-driver/scripts/extract-test-names.sh I am developing an operating system which can support Microsoft COM like component programing module based on seL4, so I have to sync every repository manually. Xilong Pei Tongji University 2015/7/13

1 0

This checkin cause a build error
by XilongPei(裴喜龙) 13 Jul '15

13 Jul '15

Hi, This checkin cause a build error: Drop static qualifier from tests so that C++ compilers will use extern C linkage instead of name mangling https://github.com/seL4/libsel4test/commit/930744eaf43260ceb37ce2793eefbe77c d808ff0 the error information: .../libs/libsel4test/src/test.c:161: undefined reference to `__start__test_case' .../libs/libsel4test/src/test.c:161: undefined reference to `__stop__test_case' Xilong Pei Tongji University 2015/7/13

2 1

Streamline seL4/libsel4 and make it not depend on libc
by Wink Saville 10 Jul '15

10 Jul '15

I've got sel4test running with libsel4 not having a dependency on libc. I've pulled out libsel4assert, libsel4benchmark, libsel4printf and libsel4putchar from libsel4 and they are separate libraries The biggest change is to seL4/libsel4 and sel4/tools/bitfield_gen.py. The changes to bitfield_gen.py allow it to generate the same code as before for the kernel but uses the new names for entities in user space. Please let me know what you think. -- Wink https://github.com/winksaville/seL4/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4test/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4allocman/tree/libsel4-no-libc-depende… https://github.com/winksaville/libsel4utils/tree/libsel4-no-libc-dependency https://github.com/winksaville/sel4test/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4assert https://github.com/winksaville/libsel4benchmark https://github.com/winksaville/libsel4printf https://github.com/winksaville/libsel4putchar

4 11

can IPC be concurrent running?
by Pei.XiLong(裴喜龙) 07 Jul '15

07 Jul '15

Hi, We can get the definition of IPCBuffer from here https://github.com/seL4/seL4/blob/master/libsel4/arch_include/arm/sel4/arch… enum { seL4_GlobalsFrame = 0xffffc000, }; It is fixed in one virtual space, that means the IPC in seL4's thread cann't be concurrent, we can't prepare more than 1 IPC request at the same time, for we call these function: seL4_SetTag, seL4_SetMR, seL4_SetUserData wil use this buffer, but there is no locker to protect the buffer. Is my understanding correct? Xilong Pei Tongji University 2015/7/6

1 0

Where is the definition of seL4_TCB_BindAEP and seL4_TCB_UnbindAEP?
by XilongPei(裴喜龙) 07 Jul '15

07 Jul '15

Hi, In test program binding.c https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/b inding.c , there are two functions, seL4_TCB_BindAEP and seL4_TCB_UnbindAEP, where can I get their definitions? Xilong Pei Tongji University 2015/7/6

2 1

Try two for libsel4 not having a dependency on libc
by Wink Saville 04 Jul '15

04 Jul '15

Here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs> is a different approach for removing the libc dependency, it seemed like people thought libsel4 was to big and that as part of the effort of breaking the dependency it should be made smaller. Basically libsel4 does nothing expect satisfy dependency needed for the kernel for some xml files. And I've broken libsel4 into basically 8 other libraries. see here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs/libs>. This maybe taking things to far, but it does mean people can use only what they need, which I like. The smallest example is app/min-hw which only uses libsel4_gen, libsel4_startup. libsel4_bootinfo and libsel4_putchar. At the other extreme apps/test-newlibs uses everything. Anyway other organizations are certainly possible. Currently there is at least one known problem, I modified bitfield_gen.py so types_gen.h has no asserts since at the moment the kernel uses assert and userspace is libsel4_assert. We could either do something like I've done and remove them or change the kernel to use libsel4_assert or something else. Anyway, before creating a pull request I'd like to know what people think. -- Wink

4 12

Who can give me a sample program using sel4platsupport_new_io_ops
by XilongPei(裴喜龙) 01 Jul '15

01 Jul '15

Hi, sel4platsupport_new_io_ops is defined in libsel4platsupport/include/sel4platsupport/io.h , it creates a new implementation of the platsupport io_ops interface using a provided simple, vspace and vka, Here is its protocol: /* * @param simple Simple interface for getting the physical frames * @param vspace VSpace interface to use for mapping * @param vka VKA interface for allocating any extra objects or cslots * @param io_ops Interface to fill in * * @return returns 0 on success */ int sel4platsupport_new_io_ops(simple_t simple, vspace_t vspace, vka_t vka, ps_io_ops_t *io_ops); Who can give me a sample program using this function? I guess it will be used in I/O DMA program, but I don't know much about DMA program. Xilong Pei Tongji University 2015/7/1

1 0

Make seL4/libsel4 not depend upon libc
by Wink Saville 29 Jun '15

29 Jun '15

I noticed that seL4/libsel4 was dependent upon libc and so I created a patch ( https://github.com/winksaville/seL4/commit/fc91a1f68c054fdb41aaa42a7b56a80f…) which removes the dependency. If there is interest I can submit a pull request, and of course will make any changes deemed necessary to make it suitable for acceptance. Please advise, Wink

6 11

How to edit RefOS libs c file
by ぷ风过无痕?? 22 Jun '15

22 Jun '15

Hi, I am using RefOS to develop a small applicaiton(interprocess comunicaion).I need to edit some c files in RefOS/libs/librefos directory,But comments say that do not edit these files,these files were generated by CIDL.CIDL is a simple C IDL compiler which is made to save the trouble of manually implementing RPC interface stubs to marshal C style arguments and return value. It uses a simple XML-based IDL language. I search on the google，but just got some introduction. So where can I got some useful infomation about CIDL? Can you recommend some books or websites? ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Sun, Jun 21, 2015 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 13, Issue 11 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC (da Tyga) ---------------------------------------------------------------------- Message: 1 Date: Sat, 20 Jun 2015 16:26:46 +1000 From: da Tyga <cyberfonic(a)gmail.com> To: devel(a)sel4.systems Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC Message-ID: <CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" > > > Hi Yuxin, I don't think you need to modify GCC, it is the compiler that you can use to generate required executables. Making changes to it is a massive undertaking. Instead of trying to reinvent stuff that has already been done, you really should read the Genode documentation and download and read the source code referenced by Norman Feske's suggestions. >From my reading of the Genode documents and source code, I would expect that you would find a considerable amount of code that you could you re-purpose for your specific requirements. Cheers, Tyga > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Jun 2015 22:46:40 +0800 > From: Yuxin Ren <ryx(a)gwmail.gwu.edu> > To: Norman Feske <norman.feske(a)genode-labs.com> > Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] Does sel4 support c++ > Message-ID: > <CAAKbDrcbyh0YV+nHzhziiiXavn-= > P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you all! > > If modifying the tool chain is the easiest way, I want to try it. > But I definitely want to avoid creating the tool chain from "bare metal". > I still prefer to reuse the existing tool chain like gcc > with minimal modification. > > Could you give me some guidance how to create a custom tool chain, which > part I need to modify? > I am not familiar with gcc. So if I have to modify gcc, where can I get > more information or documentation? > > Thanks a lot!! > Yuxin > > On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske < > norman.feske(a)genode-labs.com> > wrote: > > > Hello, > > > > > The easiest approach is possibly to create a custom tool chain, and > port > > > the GCC C++ library that way. I know the people behind Genode did some > > > of this (http://genode.org/download/tool-chain) although I'm not sure > > > how much of the C++ standard library they actually support. > > > > more in-depth information about Genode's tool chain are provided by > > Section 7.2 of the documentation [1]. In short, the tool chain is a > > "bare metal" tool chain that does not depend on a C library, yet it > > still supports C++ (including exceptions and runtime type information). > > > > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas > > the STL depends on the libc. The libc is based on FreeBSD's libc. The > > STL is GCC's version. Both libraries are available via Genode's ports > > mechanism. > > > > That said, as both the libc and stdcxx are shared libraries, they cannot > > be used on the seL4 version of Genode as of now. Shared libraries don't > > work on seL4 (at least on x86_32) because the system-call bindings > > cannot be compiled with -fPIC. > > > > [1] http://genode.org/documentation/genode-foundations-15-05.pdf > > > > 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 > > > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://sel4.systems/pipermail/devel/attachments/20150619/5b4ce704/attachmen… > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 13, Issue 10 > ************************************* > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20150620/c72cfc07/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 13, Issue 11 *************************************

4 3

Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC
by da Tyga 22 Jun '15

22 Jun '15

> > > Hi Yuxin, I don't think you need to modify GCC, it is the compiler that you can use to generate required executables. Making changes to it is a massive undertaking. Instead of trying to reinvent stuff that has already been done, you really should read the Genode documentation and download and read the source code referenced by Norman Feske's suggestions. >From my reading of the Genode documents and source code, I would expect that you would find a considerable amount of code that you could you re-purpose for your specific requirements. Cheers, Tyga > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Jun 2015 22:46:40 +0800 > From: Yuxin Ren <ryx(a)gwmail.gwu.edu> > To: Norman Feske <norman.feske(a)genode-labs.com> > Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] Does sel4 support c++ > Message-ID: > <CAAKbDrcbyh0YV+nHzhziiiXavn-= > P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you all! > > If modifying the tool chain is the easiest way, I want to try it. > But I definitely want to avoid creating the tool chain from "bare metal". > I still prefer to reuse the existing tool chain like gcc > with minimal modification. > > Could you give me some guidance how to create a custom tool chain, which > part I need to modify? > I am not familiar with gcc. So if I have to modify gcc, where can I get > more information or documentation? > > Thanks a lot!! > Yuxin > > On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske < > norman.feske(a)genode-labs.com> > wrote: > > > Hello, > > > > > The easiest approach is possibly to create a custom tool chain, and > port > > > the GCC C++ library that way. I know the people behind Genode did some > > > of this (http://genode.org/download/tool-chain) although I'm not sure > > > how much of the C++ standard library they actually support. > > > > more in-depth information about Genode's tool chain are provided by > > Section 7.2 of the documentation [1]. In short, the tool chain is a > > "bare metal" tool chain that does not depend on a C library, yet it > > still supports C++ (including exceptions and runtime type information). > > > > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas > > the STL depends on the libc. The libc is based on FreeBSD's libc. The > > STL is GCC's version. Both libraries are available via Genode's ports > > mechanism. > > > > That said, as both the libc and stdcxx are shared libraries, they cannot > > be used on the seL4 version of Genode as of now. Shared libraries don't > > work on seL4 (at least on x86_32) because the system-call bindings > > cannot be compiled with -fPIC. > > > > [1] http://genode.org/documentation/genode-foundations-15-05.pdf > > > > 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 > > > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > >

2 1

Does sel4 support c++
by Yuxin Ren 20 Jun '15

20 Jun '15

Hi, Can I run C++ programs on sel4? I am not familiar with programming language. I do not know the relationship between the OS and the C++ language. In order to run C++, does the OS need to provide some support or what user level library are needed? Thanks a lot. Yuxin

4 6

Virtualization extensions
by Nick Betteridge 16 Jun '15

16 Jun '15

Hi I'm very interested in working with the virtualization extensions on sel4 - is there any rough timeline for when these will be available. Thanks Nick

1 0

high-availability system should have these software services
by XilongPei(裴喜龙) 15 Jun '15

15 Jun '15

Hi, In general, a high-availability system should have the following software services http://electronicdesign.com/boards/high-availability-rtoss-deliver-five-nine s-reliability : - Heartbeat support for each server and each application. - Event management capability for change notification. - Alarm management for error handling. - Transactions capability for check-pointing and rollback/restart. - Clustering for server management and applications links. - Reliable storage support for RAIDs and for journaling file systems. I want to develop a high-availability system on seL4, can anyone give me some suggestions? QNX has high availability support http://www.qnx.com/developers/docs/6.3.0SP3/neutrino/sys_arch/ham.html , can we learn something from them? Xilong Pei Tongji University 2015/6/11

6 7

[sel4] seL4 on RISC-V is running SOS (Simple Operating System)
by Hesham ALMatary 09 Jun '15

09 Jun '15

Hi all, This is the second status update of the project (Porting seL4 to RISC-V). Please have a look at the blog post [1] for more details, and feel free to ask and/or comment. You feedback would be appreciated. [1] http://heshamelmatary.blogspot.co.uk/2015/06/sel4-on-risc-v-is-running-sos-… Thanks, -- Hesham

2 1

Sel4 and Network
by Haselauer Lukas - S1410304006 03 Jun '15

03 Jun '15

Hello, My name is Lukas and I am currently studying in Austria. I am currently using sel4 in a student's project. We are using CAmkES to develop a small application (on the imx6-platform), and some things already work fine :-) But when it comes to networking, we are totally without results. We tried using some of the excisting libraries (libethdrivers + libplatsupport + liblwip) - but without success. My question is: Which way can I go if I want my CAmkES Apps to communicate via ethernet? Do I have to implement a driver as part of the App? As an additional library? Or somewhere else? I really couldn't figure out how to do it properly... Is there some sort of documentation or example on how to get a IP-stack up and running on sel4? Thank you for reading and helping! Lukas

2 1

Hello world - simple example thread creation
by Piotr 31 May '15

31 May '15

I would like to start from scratch - simple thread or process creation helloworld in seL4. I saw there are some examples in "sel4test/app" of seL4 application, but I am looking for something smaller. I have found here on page 39 "Creating a Thread in Own AS and cspace_t" http://www.cse.unsw.edu.au/~cs9242/14/lectures/01-intro.pdf example of thread creation. Unfortunetly I cannot find header file with " cspace_ut_retype_addr" or "ut_alloc". Are they obsolete, any replacements? Are there any small and simple hello-world tutorials or examples avaliable?

1 0

why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys
by Pei.XiLong(裴喜龙) 29 May '15

29 May '15

Hi, Siwei Zhuang, Why do there are some differences between camkes branch and master branch in lib seL4/libsel4muslcsys? The lib seL4/libsel4muslcsys is the foundation of libmuslc, it shoud be a libc for any seL4 program, and there should be no diference among any branches. https://github.com/seL4/libsel4muslcsys/commits/camkes Xilong Pei Tongji University 2015/5/29

3 3

[sel4] Porting seL4 to RISC-V - Status Report 1
by Hesham ALMatary 26 May '15

26 May '15

Hi all, As a warm up, I've written a blog entry [1] of the project giving some introductory details for both RISC-V and seL4 microkernel and what has been done so far. Open to questions/suggestions. [1] http://heshamelmatary.blogspot.co.uk/2015/05/porting-sel4-to-risc-v-status-… Thanks, -- Hesham

2 3

Progress of bringing Genode to seL4
by Norman Feske 26 May '15

26 May '15

Hello, I have written up the first of a series of articles about using seL4 as base platform for the Genode OS framework: http://genode.org/documentation/articles/sel4_part_1 I hope that it contains useful bits of information for novices of seL4 and Genode alike. Even though the article outlines a few hurdles, the overall experience of using the kernel had been overly positive so far. For those of you interested in tracking the progress of the ongoing work, here is the corresponding topic branch: https://github.com/nfeske/genode/commits/sel4 Cheers 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

Virtual address space (kernelBase) restriction
by Hesham ALMatary 23 May '15

23 May '15

Hi all, Is it a must that every platform/architecture mapped to virtual addresses higher than 0xF0000000? Thanks -- Hesham

1 0

lowRISC Google Summer of Code
by Stefan Wallentowitz 19 May '15

19 May '15

Hi all, I just wanted to take the chance to introduce Hesham ALMatary and myself. Hesham participates in Google's Summer of Code in the lowRISC organization and I am his mentor. During summer, Hesham will port seL4 to the RISC-V architecture, specifically for the lowRISC project. Please find more details here: http://www.lowrisc.org/blog/2015/05/summer-of-code-students-for-lowrisc/ Hesham and I will keep you updated about the progress, I believe he will also give updates in his blog: http://heshamelmatary.blogspot.it/. Best Regards, Stefan

2 1

sel4 example compilation - cygwin
by Piotr 12 May '15

12 May '15

Hi, I am trying to compile example from 'Download' tutorial under Cygwin. http://sel4.systems/Download/ What I get is: [KERNEL] [BF_GEN] arch/object/structures_gen.h [BF_GEN] plat/machine/hardware_gen.h [BF_GEN] api/types_gen.h [CPP] src/arch/ia32/machine_asm.s [AS] src/arch/ia32/machine_asm.o /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S: Assembler messages: /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:15: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:20: Error: junk at end of line, first unrecognized character is `o' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:22: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:26: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:30: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:34: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:36: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:41: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Warning: .type pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:43: Error: junk at end of line, first unrecognized character is `i' /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Warning: .size pseudo-op used outside of .def/.endef ignored. /home/user/seL4test/kernel/src/arch/ia32/machine_asm.S:49: Error: junk at end of line, first unrecognized character is `i' .......... What to do with it?

4 3

CSpace: resolveAddressBits
by Norman Feske 04 May '15

04 May '15

Hello, I am trying to construct a custom CSpace for my root task using seL4's guarded page-table concept. At the 1st level, there is a CNode with a radix of 12 and a guard of 0. At the 2nd level, there is a CNode with a radix of 14 and a guard of 6. After copying the initial capabilities to the 2nd-level CNode, switching to this CSpace, and invoking a system call that takes a capability as argument (seL4_TCB_Suspend), the kernel tells me: <<seL4 [decodeInvocation/609 Te3ffa880 @10245c2]: Attempted to invoke a null cap #1.>> The problem seems to be a failed 'lookupCapAndSlot', which internally calls 'resolveAddressBits': https://github.com/seL4/seL4/blob/experimental/src/kernel/cspace.c#L138 While inspecting the function, it does not appeared to me why it does not consider any guard bits within the while loop. The 'levelBits' variable is simply set to 'radixBits'. Interestingly, the same function in the master branch looks different. Here, the 'guardBits' are taken into account, which is consistent with the documentation. I wonder, why differs the experimental branch to the master branch in this respect? Is there a way to construct the scenario above with the experimental branch? The only work-around I see is to allocate an intermediate CNode with a size of 2^6 that sits between the 1st and 2nd level. Or is there a better way? 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

2 2

Does sel4 support pthread?
by 小健 24 Apr '15

24 Apr '15

I am using sel4 to develop a multi-thread program on ARM platform. I know that sel4 support musl libc. But when I call __pthread_create the program returns an error. Does sel4 support pthread on ARM platform? By the way, I get the libmuslc from seL4test. So if there is a musl libc which has pthread inside that can be used by sel4, please tell me where I can get it. Thank you.

2 1

Port seL4 to allwinnerA20
by Jensen Zhang 20 Apr '15

20 Apr '15

Hello everyone, We have ported seL4 to allwinnerA20, although the cache cannot still work well. All tests passed, except for CACHEFLUSH0001 and CACHEFLUSH0002. A git clone can be gotten from here [1]. And the 'zener' directory in this project has a similar structure to sel4test. But there is a problem about TIMER API. For allwinnerA20, there are several registers (Timer IRQ Enable/Status Register) used by all timers. Both kernel and libsel4platsupport will use timers, and they have to use different timers. But some registers can be accessed by both kernel and libsel4platsupport. That's very dangerous! Because libsel4platsupport can disable the timer of kernel by modifying the register. How to solve this problem? [1] git clone http://elastos.org/review/HD-Elastos -- Jensen Zhang Tongji University

2 1

am335x patches - refos working
by Tim Newsham 14 Apr '15

14 Apr '15

RefOS is now working fine on am335x / beaglebone black. Patches attached. Tim

4 3

How to get a helper thread's TCB?
by Kun Cheng 11 Apr '15

11 Apr '15

Hi guys, Currently I'm working on something that requires threads can be moving between domains. I can run two domains now (trying to run more) and I'm trying to understand the content of domain.cxx in sel4-test. Each thread has TCB which contains the domain id of it. But after running through *struct helper_thread* and relevant data structures, I'm curious about how to retrieve a helper thread's domain id, which could help me verify that they're indeed moved to another domain. Best regards, Kun Cheng

1 0

Regarding Bootstrapping the Kernel
by Sebastian Lau 08 Apr '15

08 Apr '15

On the http://sel4.systems website, it says that like qnx, sel4 expects to be elf-loaded. Could you please explain what that means?

2 1

SeL4 As Hypervisor
by CACook＠quantum-sci.com 03 Apr '15

03 Apr '15

After weeks trying to make Xen pass through an Intel IGP to the VM, I've finally found that it simply doesn't work. That's enough time spent on that.... My goal is to use a microkernel for hypervisor, which supports up to 10 VMs that perform various functions. The most challenging one is a VM which plays video using hardware accel of the integrated graphics processor, and sends and receives commands over a USB device. All my VMs will be CentOS. >From the FAQ I infer that it requires coding skills to do anything more than install base seL4. True? If not, have others set up an seL4 machine with multiple VMs and written how they did it and how it went? I should note that I am not a coder, although I am well experienced with Linux admin and scripting.

3 3

libsel4cspace?
by Ted Cooper 27 Mar '15

27 Mar '15

I'm adapting the aos-2014 exercises from http://www.cse.unsw.edu.au/~cs9242/14/project/index.shtml so I can run them under IA32 qemu. Milestone 0's sos project depends on stuff from libsel4space, e.g. cspace_root_task_bootstrap(). From a cursory search, it seems like this library isn't on the seL4 github account. Is this because its functionality has been rolled into one of the other libsel4*, or because it's a course-specific library not intended to see the light of day?

2 1

Cannot run on more than 1 domian?
by Kun Cheng 26 Mar '15

26 Mar '15

Hey guys, It seems that sel4test can only run on 1 domian (with CONFIG_NUM_DOMAINS=1 in .config), I tried to set it to 4 or a larger one (<=16) but when I ran the image with qemu it gave me an error "seL4 failed assertion '_ndks_end - _ndks_start <= NDKS_SIZE' at /home/kenneth/sel4/sel4current/kernel/src/arch/ia32/kernel/boot_sys.c:447 in function try_boot_sys". Is there any other configurations or code that I have to change? PS: I've been suffering a problem that I can only receive devel digests recently but none of your emails could reach me. This is weird because I set no filter in gmail. Best regards, Kun Cheng

1 0

Getting Started
by Fred 25 Mar '15

25 Mar '15

>From the main page. "If you would like to learn how to build a system on seL4, you might want to follow the lectures and especially the seL4-based project of UNSW's Advanced Operating Systems course <http://cs9242.web.cse.unsw.edu.au/>." Request: Is it possible to obtain access to the recorded lectures as well as the notes? Also assignment templates appear to be only available to enrolled students. I understand that publicly posting solutions to the assignments may be a problem. e.g. git clone ssh:// YOURLOGIN@login.cse.unsw.edu.au//home/cs9242/public_html/current/project/files/aos-2014 Background: Our project is in the internally funded phase of an open-source platform for medical simulation and training (similar to SimMan). The system consists of intercommunicating modules where each module runs a minimal OS. Thanks

4 5

beagle bone docs on page?
by Tim Newsham 21 Mar '15

21 Mar '15

Now that sel4, sel4test and refos work on beaglebone, perhaps it could be mentioned on the sel4 web page? If there's anything I can do to help make that happen, please let me know. Tim

2 1

seL4 + Qubes OS Project
by WhonixQubes 21 Mar '15

21 Mar '15

Hello, I am the maintainer of the Qubes + Whonix project... https://www.whonix.org/wiki/Qubes Which is the port of Whonix OS (think a more secure Tor proxied VM) to Qubes OS, which has upstream integration into the Qubes codebase now. I am very interested in secure minimal kernels and hypervisors, and have been discussing these topics publicly and privately with other interested developers and investors recently. And I am also positioning to bring development resources to low-level projects that can achieve a more optimal (and verifiable) secure TCB than bloated Linux-based systems, as Qubes Dom0 is currently based upon. Actually being able to read through and know all the code that is running on a mission critical machine, a novel thought, huh. ;) I am most interested in this Qubes blurb on the seL4 website... https://sel4.systems/GettingStarted "Qubes is an open source operating system designed to provide strong security for desktop computing using virtualisation to provide isolation. Qubes is based on Xen. seL4 is a much better fit for Qubes. The project is to port Qubes to seL4 (or develop an alternative Qubes-like system for seL4)." I absolutely agree with this and would like to know more about what Qubes development project might already underway be in the seL4 community in order to consider the opportunity of providing some real assistance in the future. What's the status of this seL4 Qubes port project and who can I get in touch with to talk more about accomplishing it? Thanks! :) WhonixQubes

7 7

Emit debugging info
by Hesham ALMatary 19 Mar '15

19 Mar '15

Hi all, This is most likely a straight forward question: how can I get debugging symbols for the final image (if possible)? I am configuring/compiling seL4tests for example with "make kzm_simulation_debug_xml_defconfig", etc. And when I try to dump the generated "sel4test-driver-image-arm-imx31" content with "arm-none-eabi-objdump" command, I can't find any debugging symbols (function/variable names) although debugging flags are set. If the previous question is not valid, then how can I debug the generated image using QEMU/gdb if possible? and trace the program execution beginning from _start? Other solutions for debugging are appreciated. Thanks in advance. -- Hesham

2 2

About the latest commit of seL4 kernel
by Jensen Zhang 16 Mar '15

16 Mar '15

Hello, I found there are several little changes on the latest commit of seL4 kernel [1]. And you just changed the define of function "map_it_frame_cap" for arm, but not for ia32. I just wonder whether there are any further considerations, or it's just a mistake :) Thanks, [1] https://github.com/seL4/seL4/commit/4f12acd2703183c9f44fe097589b53eb53c599eb -- Jensen Zhang Tongji University

2 1

refos and sel4-test questions
by Tim Newsham 16 Mar '15

16 Mar '15

Is it possible to build and run sel4-test against the "experimental" kernel tree? if so, whats the process? On RefOS for my port, I'm seeing a weird problem with the timer code. It is mapping in the right phys addr for my timer device, and I can read the right ID register out, so it appears to be mapping the right memory, but the code to do a timer reset, which sets a reset bit then polls for the bit to return to zero, is getting stuck in an infinite loop. I verified that the loop isn't being altered by the compiler, and I verified that the same code runs fine in sel4 test. At this point I suspect one of two things 1) refos is allowing the mapping to happen with caching on (even though I asked it not to) or 2) something is wrong elsewhere with the "experimental" kernel (sel4-test is running on the "master" tree, and refos is using the kernel from the "experimental" tree). is there anything else I could be missing? any thoughts? -- Tim Newsham | www.thenewsh.com/~newsham | @newshtwit | thenewsh.blogspot.com

3 2

Porting seL4 to RISC-V
by Hesham ALMatary 15 Mar '15

15 Mar '15

Hi all, I'm Hesham ALMatary a computer science research student at the University of York. I am considering porting L4 microkernel variants to RISC-V [2] (for both my research and Google Summer of Code), and Fiasco.OC is one of these variants, but I want to extend the options here by asking about seL4. Is this project would be: first applicable, and second of interest to you? And if yes, would you offer some help (guidance)? I am sending this message as suggested here [1] that I should contact you if I'm willing to port seL4 to a new platform. [1] http://sel4.systems/GettingStarted/ [2] http://riscv.org/ Thanks, -- Hesham

4 4

seL4 on Raspberry Pi
by da Tyga 11 Mar '15

11 Mar '15

> > IMHO, the biggest problem with the Raspberry Pi is that most of its I/O > (even the NIC) is connected through USB. A serial port is available > (albeit without level shifters). So, running the seL4test should be > possible without a USB stack, but as soon as you want to access a > keyboard, network or filesystem, you'll need one. You should keep in mind that seL4 is a microkernel. So the USB stack and drivers that depend on that stack should all be implemented as processes/tasks running on top of seL4. I know it is not cool to mention Minix here, but it and Plan9 suggest ideas as to how the layers above seL4 could be structured. As far as I can understand, seL4 is not an operating system, it is a microkernel upon which one or more operating systems could be built. The key reason to use seL4 would be due to it providing capabilities based isolation between the layers that run on top of it and thus preventing rogue processes from interfering with other processes.

3 2

A port to the Raspberry Pi 2?
by Sebastian Lau 10 Mar '15

10 Mar '15

Would a port of seL4 to the raspberry pi 2 be welcome because I'm interested in buying a raspberry pi 2 and building sel4 for it?

5 9

docker compatible? (was Re: MySQL - seL4)
by Raoul Duke 07 Mar '15

07 Mar '15

> wouldn't provide you much. What sel4 could buy > you is isolation between mysql and other applications > if you chose to run several processes on the same > machine. The processes themselves, including mysql, > would still be vulnerable to any internal vulnerabilities > they might have (sel4 is not a magic bullet). There's a lot of noise around Docker. I find it annoying for many reasons, including security -- although I do understand some of the attraction. It would be super keen in my mind if seL4 could offer something in that vein, could present itself as a nice alternative.

5 6

MySQL - seL4
by André Bispo 06 Mar '15

06 Mar '15

Hello guys,Do you think it is feasible to have MySQL running on top of seL4 and take advantage of the isolation mechanisms?I was looking into the microkernel, the CamKES project and the mailinglist, to find some answers but i think it would be very difficult, if not impossible to run MySQL on seL4.I'm trying to explore this possibility and i want to know your opinion before continue. Best regards,André Bispo.

3 2

USB booting problem
by André Bispo 05 Mar '15

05 Mar '15

Hello guys, i'm building myself a system for my thesis and i'm currently testing out the seL4.I was trying to boot the sel4test by USB following the tutorial described in another question on this mailing list.But syslinux seems to load the kernel and the test but nothing appears afterwards.This is the message shown: MBRLoading sel4kernel... okLoading rootserver... ok _ If anyone could help me out i'd be very grateful. Best regards,André Bispo.

3 3

am335x - configs and refos
by Tim Newsham 04 Mar '15

04 Mar '15

Attached are some patches for am335x support. I've started to play with refos, and can build it for am335x and run some of the startup (with release mode) but it hangs at some point.. still a work in progress. Also there's a few minor proofread tweaks on the refos doc. By the way, sel4test runs pretty well now in debug and release modes. Instructions are pretty straightforward: - build the project using the debug or release config - use objcopy to extract a raw binary from the ELF image - load the binary with uboot (I use "tftp", it defaults to the proper load address) - run it in uboot with "go 82000000" Tim

2 1

Joint a formally verified C compiler with seL4?
by Grissiom 02 Mar '15

02 Mar '15

Hi all, I've heard a formally verified optimizing C compiler: CompCert recently: http://www.absint.com/compcert/ HN: https://news.ycombinator.com/item?id=9130934 . So what benefit will there be if some one use CompCert as the compiler for seL4? -- Cheers, Grissiom

3 2

Re: [seL4] How are capabilities assigned
by Sebastian Lau 02 Mar '15

02 Mar '15

Hi, sorry if this sounds stupid but are address spaces and threads directly managed by the kernel as in are they allocated and identified by the kernel or is there another that helps the kernel?

2 2

ifc6410 loading instructions
by Joel Nider 26 Feb '15

26 Feb '15

Hi, I'm trying to follow the instructions for loading the test image for ifc6410 on this page: http://sel4.systems/Hardware/IFC6410/ I'm not clear about the second instruction "> ramdisk". It looks to me like this is a redirection with some missing parts. Can you please help me fill in the blanks? Thanks, Joel

2 2