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