Hello,
I am at the George Washington University working on benchmarking the seL4
system. I am new to systems, and I am having a hard time building a
bootable USB image On Ubuntu 14.04 x86. I understand that there is a Grub2
stanza on the Downloads page <https://sel4.systems/Download/> on the SeL4
website, but I cannot find the sel4kernel and sel4rootserver files in the
system to build into a boot image.
I would like to build an image using a process similar to the one in
Pistachio (see https://www.l4ka.org/120.php) except for using Grub2 of
course.
Are there instructions for booting on full hardware such as a PC?
Regards,
Matthew Scaperoth
Jr. Programmer Analyst
The George Washington University
Academic Technologies
Tel: 202-994-6907
Hi
I am new in seL4. It is really interesting OS.
I would like to ask some questions even though the FAQ explains many things.
1. How different is seL4+VMM with OKL4 or codezero?
If there is some performance gap between them, I am curious where the
overheads are for?
2. I am wondering how well seL4 can support virtualization services.
Can seL4 supports more than two linux simultaneously on the VMM layers?
Moreover, can it execute different kind of guest OSes at the same time?
What about RTOS? A RTOS can be executed with keeping their real time
property on the seL4+VMM??
Lastly, I would like to know when new version of the VMM for A15 support
will be released.
3. Did you use a code generator when you hit the steps for
“Specification”, “Haskell Prototype” and “C code” In the Proof Processing?
If you did it using any automatic tool, I am so curious how you verified
and validated the codes.
4., According to the FAQ, current multicore support is through a
multikernel configuration.
Do you have any plan for one seL4 kernel to manage several processors?
Thank you much in advance.
Regards,
Joe.
Hello All,
First I wanted to say thank you for this dev forum. The more I learn about
SeL4 the more I am amazed with how well it is written.
I am working on a 32-bit Ubuntu 14.04 and I would like to run your
individual test suites in the sel4-manifest with a 32-bit build.
Specifically some of the tests from the
https://github.com/seL4/sel4test/tree/master/apps/sel4test-tests/src
directory. For example, I'd like to alter the code a little bit and run
qemu to output cycle time for IPC or memory mapping. So potentially I would
boot up the image, the files would load and I would get an output saying
"Intra-as IPC 151 cycles" or something along those lines after the test was
automatically run.
I was reading through the files and noticed that the main.c accepts
arguments to say which test I'd like to run using the find_test() method
with the argv passed in. I am now trying to find a way to use the main.c
file in sel4test-tests to achieve the build I am after.
I also noticed that a .bin file and a another file in
stage/ia32/pc99/bin/sel4test-tests are generated when you run the first
top-level make after the configuration. So I have tried booting the
sel4test-tests file in qemu with
qemu-system-i386 -m 512 -serial stdio -kernel images/kernel-ia32-pc99
-initrd stage/ia32/pc99/bin/sel4test-tests
but nothing happens. My thought process was that it could replace the
driver image for ia32 pc99 (sel4test-driver-image-ia32-pc99) .
So I am missing a piece here (or pieces?). I am not sure if there is a
Makefile that I can alter to include only a specific test, or if it's
something else entirely. I'd be happy to clarify what I aim to achieve or
details about my system if necessary.
Also, I am really enjoying the code that generates these tests in the
main.c file mentioned earlier. I feel like it is a much more graceful
solution to running these tests than other l4 systems I've worked with.
Thanks again,
Matt
>
> Date: Thu, 18 Sep 2014 15:58:29 +0800
>> From: XilongPei(???) <pei_xilong(a)tongji.edu.cn>
>> To: "'Aniruddha Bhide'" <aniruddha.360(a)gmail.com>, "'Peter Chubb'"
>> <peter.chubb(a)nicta.com.au>
>> Cc: devel(a)sel4.systems
>> Subject: [seL4] ??: x86 Bootable USB install
>> Message-ID: <007c01cfd316$565647b0$0302d710$(a)tongji.edu.cn>
>> Content-Type: text/plain; charset="utf-8"
>> Hi,
>> I am at Tongji University (China, http://www.tongji.edu.cn/english/ ), I
>> want to build a Fault Tolerant Operating System for high speed railway.
>>
>> The seL4 is just a micro-kernel operating system, there is still no
>> centre-service to let it work as a PC operating system, and it still can?t
>> work as a virtual-machine, such as VirtualBox. There are a lot of works
>> should be done before seL4 used as a really operating system.
>>
>> Xilong Pei
>> 2014/9/18
>
>
>
> You are correct. seL4 is a microKernel upon which an operating system
could be built. Instead of writing a proprietary OS for your high speed
railway (of which there are several already in operation, e.g in France,
Germany) you might want to consider porting an existing OS to run on top of
seL4, or even better build your specific requirements on top of a robust OS
such as those found at http://cog.systems/products.shtml.
Hello,
I have noticed certain fail() calls include newline. This does not seem
necessary since fail() is defined as
printf(
"seL4 called fail at %s:%u in function %s, saying \"%s\"\n",
file,
line,
function,
s
);
Which causes affected error messages to contain a single " character on a
new line.
Patch attached.
Regards,
Eduard Nicodei
Hi All,
I am all new to this raspberry pi.I was trying to port sel4 (
https://github.com/seL4/seL4) on raspberry pi but the build instruction (
http://sel4.systems/Hardware/General/) are only for another board.
Has anyone successfully ported sel4 on pi.
Please guide me
Another query does sel4 has networking stack?
Regards
