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.
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…
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
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.
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
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.
= 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.
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
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
