Now, Linux4.3 kernel can work well on camkes-arm-vm, does that mean we can run an Android system based on this kernel?
I have tried to replace the roofs with an Android ramdisk, but Linux can not excute the Init program. The error is showing below:
[ 10.598871] Freeing unused kernel memory: 4168K (c0a74000 - c0e86000)
[ 10.761443] Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004
[ 10.770568] CPU: 0 PID: 1 Comm: init Tainted: G W 4.3.0-rc5-00024-gec4c02c-dirty #122
[ 10.779510] Hardware name: NVIDIA Tegra SoC (Flattened Device Tree)
[ 10.785795] [<c00167ec>] (unwind_backtrace) from [<c0012958>] (show_stack+0x10/0x14)
[ 10.793537] [<c0012958>] (show_stack) from [<c008f054>] (panic+0x94/0x220)
[ 10.800407] [<c008f054>] (panic) from [<c0025b9c>] (do_exit+0x7fc/0x8f4)
[ 10.807101] [<c0025b9c>] (do_exit) from [<c0025d70>] (do_group_exit+0x3c/0xf0)
[ 10.814318] [<c0025d70>] (do_group_exit) from [<c002f3ec>] (get_signal+0x1a4/0x754)
[ 10.821971] [<c002f3ec>] (get_signal) from [<c001a748>] (do_signal+0x84/0x61c)
[ 10.829188] [<c001a748>] (do_signal) from [<c0012604>] (do_work_pending+0xa4/0xb4)
[ 10.836750] [<c0012604>] (do_work_pending) from [<c000f6b4>] (slow_work_pending+0xc/0x20)
[ 10.844919] ---[ end Kernel panic - not syncing: Attempted to kill init! exitcode=0x00000004
Is this a problem that current VMM does not support FPU? or other reasons caused the problem？
I would like to use network (TCP) on seL4, I know that I should probably be
using lwip, however I have no idea how to properly initialize it (this is
the first time I'm working in such a hardware close environment), so I need
some help or some kind of example, but I don't know where to look. I'm
working on ia32.
I also tried to run the rumprun hello world, the compillation finishes,
however I get the following output when I try to run it:
Is there any documentation on how the VMM works? If I wanted to start
hacking on the VMM and extend its capability, where should I start
looking to learn how it works, etc?
That might be a pretty broad topic, because there are lots of ways the
VMM can be extended, I'm sure. Broad is fine, until I get things more
I was curious why the ARM VMM for the TK1 only seems to support the use of
armel based distributions? Does special care need to be taken in the VMM to
handle guest floating point instructions if the OS is armhf based?
I was wondering when we call seL4_cnode_delete on a (mapped) frame cap,
does the kernel also handle unmapping the frame (in addition to withdrawing
authority) as well?
Or the user-space has to ensure that the frame is unmapped first before
I tried my code without unmapping that frame when deleting the cap and it
seems to work fine.
So I guess the kernel handles that?
Norrathep (Oak) Rattanavipanon
M.S. in Computer Science
University of California - Irvine
I've been able to build and run the hello-camkes-mcs example app from the camkes-mcs-tutorials.xml manifest both on a SabreLite board and in QEMU. However, when I try to run the app with the budget and period values given in the solution file, the client tasks don't appear to be running as they should.
See the output from running on the SabreLite here: https://pastebin.com/RM0aisyF
After that point it seems to hang. I tried smaller budget & period values and have been able to get one client task running, but the second task doesn't appear to be running.
Has anyone been able to run this example with different results?
I am facing an issue with our existing project (currently based on seL4
I am in the process of migrating our project to the latest version of seL4.
After all the required changes I am facing a problem I need some help.
In our code, we use libplatsupport for timer & serial I/O as well as the
libethdriver in order to use the network interface of the IMX6 board.
The problem appears that the IOMUX device registers are mapped twice. A
first time from libplatsupport (and never released):
-> calls: mux_sys_init()
-> calls the macro: MAP_IF_NULL(io_ops, IMX6_IOMUXC, _mux.iomuxc);
This end up mapping the device region IMX6_IOMUXC: 0x20e0000 - 0x20e100
So far so good...
but then they are mapped again from the ethernet driver:
-> call my initialization fn
-> call ethif_imx6_init()
-> call setup_iomux_enet()
that end up mapping again the region @ IOMUXC_PADDR = 0x20e1000
This second time, the mapping function _utspace_split_alloc fails because
apparently the region 0x20e000 has been already mapped (and is not in the
If I comment out the call to mux_sys_init() in
libsel4platsupport_new_io_ops() my ethernet driver successfully initialize
(but clearly that's not the correct workaround).
Real-Time Innovations, Inc.
Thank you very much for your explain. I might have some misunderstanding about the source code. First may I ask what the kernel window means? Does it means the virtual memory space kernel can access (through pptr_t)?
I can see the dev_p_regs (kernel/src/plat/tk1/machine/hardware.c) has multiple parts: the first is the RAM part, VM_HOST_PA_START - VM_HOST_PA_START + VM_HOST_PA_SIZE (0xb0000000 — 0xf0000000), the rest are real device region from 0x01000000 - 0x7c000000 approximately. I guess my question is why put the second half as a “device” instead of putting it together in avail_p_regs? Is it somehow due to the support of virtualization?
Here is the booting procedure according to my understanding, could you take a look and see if I got it right?
1. the code start at the ELF-loader main() (tools/elfloader/src/arch-arm/boot.c) which is loaded in physical memory 0x82000000 for TK1 (tools/elfloader/gen_boot_image.sh)
2. the boot code unpack the ELF and find the kernel image and the user-land image, the kernel is loaded at 0x80000000 the user land image is loaded at 0x80037000 approximately
3. MMU is enabled and a “boot" page directory is created that maps physical 0x80000000 to (0xe0000000 - 0xf0000000)
4. enter the kernel code _start, which setup up vector table and kernel stack; then init_kernel(); then try_init_kernel() calls map_kernel_window()
I’m not sure why map_kernel_windows() remap the virtual address kernelBase (start from 0xe0000000) to physical address physBase (0x80000000) again or did I miss anything?
Also I’m not sure what those armHSGlobalPGD, armHSGlobalPD for, I assume it is for context switch?
(deleted diagram due to size limit)
I want to know more about the mechanism of device driver in seL4.
How does seL4 support userspace drivers?
if I want to write a driver(e.g. serial port) base on seL4, how to do that?
can any one help?