Devel

devel@sel4.systems

9 participants
1390 discussions

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

seL4 test on x86
by Yevgeny Lavrov 14 Jun '16

14 Jun '16

Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm trying to run seL4 test suite or simple hello world task from seL4 tutorials on the real hardware. So far I had no problems compiling seL4 test suite and running via QEMU for both x32 and x64 platforms. However, when I try to run it on the actual hardware following Running on real hardware tutorial for x86 I end up with no output at all and no error msgs that can give me a clue on where something went wrong. After compiling seL4test for x86, I ended up with two images in sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created a new GRUB2 entry that looks like this menuentry “seL4 test suite” --class os { load video insmod gzio insmod part_msdos insmod ext2 set root=’(hd0,msdos5)’ multiboot /boot/sel4/kernel-ia32-pc99 module /boot/sel4/sel4test-driver-image-ia32-pc99 } update grub, restart and select the new entry from GRUB menu. I end up with blinking cursor on the top-left side of the screen. Please advise.

3 2

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

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel