I have a question about standard output. I have a camkes component than can
write into text-mode VGA buffer (basically it follows this simple example
http://wiki.osdev.org/Bare_Bones#Writing_a_kernel_in_C ) but I would like
to be able to redirect the kernel messages during startup to be printed on
screen using VGA buffer.
Once another component (either Linux in a VM, or some other camkes app)
will initialize, it will be able to take control over the screen output
(and for example show login window etc).
My questions is - is this possible with seL4? And if so, what would it
I guess in the minimal version, I would have to provide a different
implementation of seL4_DebugPutChar, is that correct?
The VGA standard seems to define the buffer to be at 0xB8000, so it should
be consistent between x86 platforms.
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:
A couple of issues building the latest seL4 NetBSD rumpkernel demoapps,
hello-ia32-x86_64_qemu_defconfig / hello-x86_64-x86_64_qemu_defconfig.
(Ref: https://github.com/SEL4PROJ/rumprun-sel4-demoapps )
1. In libsel4muslcsys sys_morecore.c:
> /host/libs/libsel4muslcsys/src/sys_morecore.c:248:16: error: ‘vaddr’ undeclared (first use in this function)
> return vaddr;
Speculatively, should it return: (long) placement_vaddr ?
2. In rumprun/platform/sel4/entry.c
> entry.c:91:9: error: implicit declaration of function 'allocman_add_untypeds_from_timer_objects' [-Werror=implicit-function-declaration]
> allocman_add_untypeds_from_timer_objects(allocator, env->custom_simple.timer_config.hw.to);
Not sure where this function should be found...
Same results in native build (Xenial) and in docker build container.
Any suggestions warmly appreciated.
I have a system configured to use dynamic heap through the vspace. I'm
working with 5.2.0 and using pc99 simulator through qemu.
Everything is occurring in the root task, as I haven't even completed my
In this configuration, whenever my code calls malloc() and there is a low
memory condition (where there is not enough space on the heap to fulfill my
request), malloc() end up calling __expand_heap().
Here it first attempts to expand the heap through brk syscall, then if
fails uses mmap() to attempt to get more pages from the virtual memory.
In both cases (brk and mmap) end up calling a function in the vspace that
attempts to make available new pages.
Unfortunately the code in the libself4utils/src/vspace/vspace.c, end up
calling malloc() for the sel4utils_res structure.
As you expect, we are already in a no-memory condition, so a subsequent
call to malloc() might end up calling __expand_heap() and so on...
(depending on the bytes left on the heap, this nested malloc might
succeed if the initial block was larger than the size of sel4utils_res
So, everything loops until the whole system crash because of stack overflow.
Why vspace uses malloc() to dynamically allocate those structures, causing
the whole system to fail?
To test, I have changed the implementation in vspace.c to use a static
buffer pool, and it seems it solve my issue, but am I doing something wrong
in the bootstrap code ?
Any help is appreciated,
Real-Time Innovations, Inc.
Another problem when making sel4. The make program complains Invalid package ID: "array-0.5.1.1 base-184.108.40.206 binary-0.8.3.0 bytestring-0.10.8.1".
make: Entering directory '/path/to/sel4/projects/capdl/capDL-tool'
stack will use a locally installed GHC
For more information on paths, see 'stack path' and 'stack exec env'
To use this GHC and packages outside of a project, consider using:
stack ghc, stack ghci, stack runghc, or stack exec
stack build --only-dependencies
Invalid package ID: "array-0.5.1.1 base-220.127.116.11 binary-0.8.3.0 bytestring-0.10.8.1"
Makefile:39: recipe for target 'sandbox' failed
make: *** [sandbox] Error 1
How can I fix this? Thank you.
Ubuntu 16.04 LTS
GNU Make 4.1
gcc version 5.4.0 20160609
Next January 22--26, linux.conf.au will be in Sydney, Australia.
We're planning on submitting a proposal for a one-day miniconference
to be held in conjunction with the main conference. We'd like to
line up potential speakers now, before submitting.
If you are doing something cool and open source with seL4, and
would like to speak at that miniconference, please let me know.
linux.conf.au is one of the best grass-roots open-source and Linux
conferences around; if you're doing anything cool that's open source
with seL4 (or with Linux), then I'd encourage you to submit a proposal
to the main conference as well, at https://linux.conf.au/
Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/
Trustworthy Systems Group Data61 (formerly NICTA)
in the 6.0 manual section 3.1.4 the table shows that Write permission on
an endpoint cap permits sending to the endpoint.
however, in section 4.2.2 it says without the Write permission on the
RECEIVING endpoint cap, any cap sent over IPC gets diminished.
Am I missing something? It seems the Write permission is overloaded to
mean two different things.
This would seem to imply that to receive an undiminished capability via
IPC you must have both send and receive permission to the endpoint you
are receiving against.
Which would mean if you wanted to limit someone to only receiving and
never sending against an endpoint by giving them an endpoint cap with
only Read permission, they would necessarily also NEVER be able to
receive an undiminished capability.
I want to share a file in one Linux filesystem and be visible to other Linuxes that all run on top Fiasco.OC. It seems an IPC communication between L4re vm tasks. And access a file in Linux filesystem is a mechanism with kernel block device driver. But I only notice two char device drivers that use L4re library l4shmc in L4linux. It is l4ser_shm and l4shmnet. May you give some information about this work how to work. Thanks.