Hi,
I am a student fron Nanjing university, a fresh man of microkernel,
specially,
know very little about the seL4.
Recently I accept a chellange about porting the lwip to sel4, on arch
of imx6,
does any one could give me a clue?
I found the source of camkes does have this code, could I do something
to port,
to make the lwip work? What my aim is make a tcp echo server.
Thank you for all of you help.
Best regards
from Xuguo Wang
For UX/RT <https://gitlab.com/uxrt/>, the seL4-based OS I am writing, I
have patched seL4 to support for booting from an in-memory execute-in-place
filesystem image that contains the kernel and all user-mode programs
required to mount the root filesystem (similar to that of QNX, but
with more of the
functionality in the bootloader rather than the root server). The existing
seL4 boot process may be OK for static embedded systems that are always
cross-compiled, but UX/RT is going to be a dynamic general-purpose OS with
a boot image that will include files from multiple
separately-installed packages and
will possibly be customized to the system it is installed on.
Requiring any image
filesystem to be linked into the root server makes updating boot images
more complex than being able to use a simple filesystem builder to make an
image containing the kernel, root server, and everything else that is
required (the main special considerations being placing the kernel and root
server at fixed physical addresses and padding the image to allow for bss
sections, which are easy enough). Also, I want it to be easy to manually
boot UX/RT images, so you can just type something like "boot
(hd0,0)/uxrt.boot" (much like manually booting NetBSD, OpenBSD, or most
older Unices), and the bootloader will automatically load the kernel and
all required modules from within the image as opposed to having to type a
lot of boilerplate to load the kernel and root server (and anything else
that may be required). In addition I don't think that the root server
should need to have any support for parsing image filesystems and
should be able to obtain all the files required for early boot from
the MBI.
I am using Multiboot2 with a few custom tags added and a few extra
requirements regarding placement of modules. I currently have an
in-memory loader that implements my variant of Multiboot2, and
eventually want to
implement a full disk-based bootloader. I have also implemented a
page-oriented in-memory filesystem called XRFS (originally based on
Linux romfs) with support for placing files at fixed addresses. The
in-memory loader was parsing the filesystem and using a script to
locate the modules within the image, although I have decided that it
is overkill to do that, and it would allow the loader to be simpler if
the filesystem image has its own MBH separate from that of the kernel
(the magic number will be different from the kernel MBH as well), with
tags for the kernel and each module, so that the loader's existing
MBH-parsing code can be used to locate files in the image.
As far as my kernel patches go, they extend the existing Multiboot2
code and do not interfere with the existing boot code. Right now they
are x86-only, but I am planning to add Multiboot2 support to other
architectures eventually as well. They do not introduce any dependency
on my filesystem format in the kernel (it does know that there is an
FS image and that there are modules contained within it, and assumes
that modules are contiguous). Relocation of the root task is disabled
when an FS image is present, since it will already be placed in a
usable location in the image. Kernel-level ELF loading of modules is
also disabled when using my Multiboot2 extensions, since my loader is
capable of parsing ELF modules, loading them, and passing information
on module sections and addresses to the kernel through tags. The part
of the image containing the kernel is inaccessible to the root task
for obvious reasons, so an additional requirement is that the kernel
is the first file in the image, followed by the root server, and then
all other files (XRFS is structured to allow the remainder of the
image to be read even though the beginning is inaccessible). There is
also support for passing the MBI through to the root task, which
requires that the MBI is allocated immediately after the end of the
filesystem image (a new structure is added to the bootinfo to provide
the root server with the address of the MBI).
>From what I've said, would there be any problems with including my
patches in the mainline seL4 repository? Only the boot code is
modified. Loading the root server works, but I haven't yet tested the
MBI passthrough, so I am not quite ready to submit anything (currently
I am working on converting my bootloader from parsing the filesystem
itself to parsing an MBH in the FS image, like I said before).
DornerWorks is looking at working with the CAmkES-VM. In previous work with ARM, we've only used a non-camkes VMM, since the hypervisor pieces were more important (and 64-bit ARM CAmkES hadn't been developed).
Out of curiosity, has Data61 ever worked with a non-CAmkES VM on x86 similar to how the old ARM VMM worked? If so, is that something that could be released?
Thanks,
Chris Guikema
I am investigating the use of seL4 on heterogeneous architectures such as
the Zynq UltraScale+ MPSoCs. I have a non-trivial use-case I'm
investigating that involves utilising both the Cortex-R5 cores and Core-A53
cores for different applications. I'm rather new to seL4 development so I'm
a bit stuck and need some advice.
It's easiest if I just list my requirements and assumptions for my
architecture design:
a) I am targeting the Zynq US+ platform and wish to use seL4 as the OS
Kernel to manage system resources and run virtual machines.
b) I require the use of the Cortex R5 cores in DCLS mode for trusted code
with high fault tolerance requirements.
c) I require the use of the Cortex A53 cores for running unsafe Linux VMs.
d) It's my understanding that seL4 lacks 64-bit multicore support for its
own scheduler, but VMs running on seL4 could be provided with access to all
the cores? (Eg: Linux)
e) It's my understanding that seL4 lacks heterogeneous task scheduling, and
cannot manage both the Cortex R5 and Cortex A53 cores.
This leads me to make the following architectural conclusions:
[1] It's not possible to boot an seL4 kernel on one processor and have it
manage the other.
[2] Use TrustZone to create vCPUs for the Cortex R5 and A53 modules and
boot an seL4 kernel on each.
[3] Some domain specific protocol is required for the CPU modules to
communicate and share resources.
Any help or advice would be appreciated.
Regards,
Robbie
Hi all,
I got a question, how can I pass the network communication to Linux virtual machine? Following the work of seL4-ARM-VMM with TK1-SOM board, i run seL4 as the microvisor that hosts the buildroot Linux as a user-land process, I was able to mount the MMC storage in the virtual machine, but I cannot get the NIC works. I’m wondering has anyone tried it that can give me some hint?
Best Regards
-Daniel Wang
Hi all
I am new comer to sel4 community. I knew a little bit virtualisation
infrastructe(kvm/qemu), but I know little about sel4/docker.
I am investigating the proper implemenatation for running docker on sel4 on
arm64.
There might several ways I can figure out.Any suggestions are welcome :-)
1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might
be the
easiest way. It might have worked well on X86
2. porting l4linux to sel4. Don't know whether it is feasible?
3. run docker as sel4 service without linux. On this way, golang and its
library should be ported to sel4. Some missed syscalls which are needed by
docker should be implemenated.
Is there any other ways or anything else to make the implatation more
feasible?
---
Cheers,
Justin
HI, I have a question about IPC and SMP.
I ran sel4bench on sabre lite(i.mx6, arm v7).
1. I want to confirm performance difference between Lazy Scheduling and
Beno Scheduling. Can I configure scheduler?
2. Can you explain the difference when thread state is
"ThreadState_Running" and "ThreadState_Restart"?
3. I tried "SMP Benchmark" but I can't understand what this benchmark
exactly means.
What "Cycles" means in this benchmark?
smp : This is an intra-core ipc round-trip benchmark to check overhead of
the kernel synchronization on ipc throughput.
4. I try to measure IPC performance with SMP is on.
I used "seL4_TCB_SetAffinity" function so server executed in Core1 and
client executed Core2.
But performance results are too excessive.
seL4_Call(same vspace, ipc length is 0)' result is 129331186 cycles.
Are these results are available?
Hello,
We are having issues being able to get the seL4test userland image to boot on x86 hardware. We have attempted to boot with syslinux off a USB, with PXELINUX, and with grub and see the same userland image loading issue across boot methods.
Build steps:
- Following https://docs.sel4.systems/Hardware/IA32
- Using "-DPLATFORM=x86_64"
o Does not appear to boot (no serial output)
- Using "-DPLATFORM=ia32"
o Kernel boots but is unable to load userland image
The manifest commit hash is:
01c11cfcd881c1da5b7520162fae40f6eae1c16b
Hardware:
- DELL Optiplex 980 with an Intel Core i7 860 processor
We are seeing the following serial output:
SYSLINUX 6.03 20171017 Copyright (C) 1994-2014 H. Peter Anvin et al
Loading sel4kernel... ok
Loading rootserver... ok
Boot config: parsing cmdline 'sel4kernel'
Boot config: console_port = 0x3f8
Boot config: debug_port = 0x3f8
Boot config: disable_iommu = false
Detected 1 boot module(s):
module #0: start=0x1d6000 end=0x4abdf4 size=0x2d5df4 name='rootserver'
Parsing GRUB physical memory map
Physical Memory Region from 0 size 9e400 type 1
Physical Memory Region from f0000 size 10000 type 2
Physical Memory Region from 100000 size df5cfc00 type 1
Adding physical memory region 0x100000-0x1fc00000
Physical Memory Region from df6cfc00 size 54000 type 4
Physical Memory Region from df723c00 size 2000 type 3
Physical Memory Region from df725c00 size 8da400 type 2
Physical Memory Region from f8000000 size 4000000 type 2
Physical Memory Region from fed00000 size 400 type 2
Physical Memory Region from fed20000 size 80000 type 2
Physical Memory Region from fec00000 size 100000 type 2
Physical Memory Region from fee00000 size 100000 type 2
Physical Memory Region from ffb00000 size 500000 type 2
Physical memory region not addressable
Physical memory region not addressable
Multiboot gave us no video information
ACPI: RSDP paddr=0xfec00
ACPI: RSDP vaddr=0xdfcfec00
ACPI: RSDT paddr=0xfc790
ACPI: RSDT vaddr=0xdfcfc790
***WARNING*** SKIM window not enabled, this machine is probably vulernable to Meltdown (https://www.meltdownattack.com), consider enabling
Kernel loaded to: start=0x100000 end=0x13a000 size=0x3a000 entry=0x100076
ACPI: RSDT paddr=0xfc790
ACPI: RSDT vaddr=0xdfcfc790
ACPI: FADT paddr=0xfc85c
ACPI: FADT vaddr=0xdfcfc85c
ACPI: FADT flags=0xa5
ACPI: DMAR paddr=0xfcdde
ACPI: DMAR vaddr=0xdfcfcdde
ACPI: IOMMU host address width: 36
ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1d fun=0x0
ACPI: registering RMRR entry for region for device: bus=0x0 dev=0x1a fun=0x0
ACPI: 1 IOMMUs detected
ACPI: MADT paddr=0xfc9c4
ACPI: MADT vaddr=0xdfcfc9c4
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_APIC apic_id=0x2
ACPI: Not recording this APIC, only support 1
ACPI: MADT_APIC apic_id=0x4
ACPI: Not recording this APIC, only support 1
ACPI: MADT_APIC apic_id=0x6
ACPI: Not recording this APIC, only support 1
ACPI: MADT_APIC apic_id=0x1
ACPI: Not recording this APIC, only support 1
ACPI: MADT_APIC apic_id=0x3
ACPI: Not recording this APIC, only support 1
ACPI: MADT_APIC apic_id=0x5
ACPI: Not recording this APIC, only support 1
ACPI: MADT_APIC apic_id=0x7
ACPI: Not recording this APIC, only support 1
ACPI: MADT_IOAPIC ioapic_id=8 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: 1 CPU(s) detected
ELF-loading userland images from boot modules:
BOOT MODULE:
0x1d6000: 0x0
0x1d6010: 0x0
0x1d6020: 0x0
0x1d6030: 0x0
0x1d6040: 0x0
0x1d6050: 0x0
0x1d6060: 0x0
0x1d6070: 0x0
0x1d6080: 0x0
0x1d6090: 0x0
0x1d60a0: 0x0
Boot module does not contain a valid ELF image
seL4 called fail at /host/sel4test/kernel/src/arch/x86/kernel/boot_sys.c:813 in function boot_sys, saying "boot_sys failed for some reason :("
halting...
Kernel entry via Interrupt, irq 0
Thanks,
Alex
Hi,
I am using Ubuntu 16.04 on 64 Bit, i7 machine and running the CAmkES
x86 VM instructions available at:
https://docs.sel4.systems/CAmkESVM
After running:
../init-build.sh -DCAMKES_VM_APP=minimal
I am getting the following error:
--------------------------------------------------------------------------------------------------------------------------------
camkes-gen.cmake is out of date. Regenerating...
CMake Error at tools/camkes/camkes.cmake:593 (message):
Failed to generate camkes-gen.cmake: Traceback (most recent call
last):
File "/usr/lib/python2.7/runpy.py", line 174, in
_run_module_as_main
"__main__", fname, loader, pkg_name)
File "/usr/lib/python2.7/runpy.py", line 72, in _run_code
exec code in run_globals
File
"/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py",
line 678, in <module>
sys.exit(main(sys.argv, sys.stdout, sys.stderr))
File
"/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py",
line 515, in main
instantiate_misc_templates(renderoptions)
File
"/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/__main__.py",
line 509, in instantiate_misc_templates
outfile_name=outfile.name, imported=read, options=renderoptions)
File
"/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/Renderer.py",
line 109, in render
self.templates, **kwargs)
File
"/home/goyal/sel4/camkes_vm/tools/camkes/camkes/runner/Context.py", line
261, in new_context
}.items()) + list(kwargs.items()))
AttributeError: type object 'ObjectType' has no attribute
'__members__'
Call Stack (most recent call first):
CMakeLists.txt:35 (GenerateCAmkESRootserver)
-- Configuring incomplete, errors occurred!
See also
"/home/goyal/sel4/camkes_vm/build_vm/CMakeFiles/CMakeOutput.log".
-------------------------------------------------------------------------------------------------------------------------------
I also tried to run the same instructions on a different machine
(Ubuntu 16.04, 64 Bit, i5 machine) on which ../init-build.sh
-DCAMKES_VM_APP=minimal is run successfully.
It gets stuck on running ninja.
I am getting the following error:
--------------------------------------------------------------------------------------------------------------------------------
ghc-8.0.2: 106.97 MiB / 107.55 MiB ( 99.47%) downloaded...
ghc-8.0.2: 107.24 MiB / 107.55 MiB ( 99.71%) downloaded...
ghc-8.0.2: 107.50 MiB / 107.55 MiB ( 99.96%) downloaded...
ghc-8.0.2: 107.55 MiB / 107.55 MiB (100.00%) downloaded...
/home/akshat/.stack/programs/x86_64-linux/ghc-8.0.2.tar.xz.tmp:
renameFile:renamePath:rename: does not exist (No such file or directory)
Makefile:45: recipe for target 'parse-capDL' failed
make: *** [parse-capDL] Error 1
ninja: build stopped: subcommand failed.
--------------------------------------------------------------------------------------------------------------------------------
Can someone suggest a way out for both the problems.
--
Thanks and Regards,
Amit Goyal
good day. I can no longer build tutorials. These used to build a month ago.
My system hasn't changed and I can still build the older ones with no
issues. I get lost trying to debug this cmake/python stuff.
./init --verbose --plat pc99 --tut hello-camkes-1
INFO:sh.command:<Command u'/sandbox/bin/cmake
-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc
-DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>: starting process
DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake
-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc
-DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525
['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G',
'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64',
'-DTUTORIAL_DIR=hello-camkes-1', '..']>: started process
INFO:sh.command:<Command u'/sandbox/bin/cmake
-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc
-DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..', pid 17525>: process
started
DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake
-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc
-DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525
['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G',
'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64',
'-DTUTORIAL_DIR=hello-camkes-1', '..']>: acquiring wait lock to wait for
completion
DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake
-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc
-DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525
['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G',
'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64',
'-DTUTORIAL_DIR=hello-camkes-1', '..']>: got wait lock
DEBUG:sh.command.process:<Command u'/sandbox/bin/cmake
-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G Ninja -DTUT_BOARD=pc
-DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..'>.<Process 17525
['/sandbox/bin/cmake', '-DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake', '-G',
'Ninja', '-DTUT_BOARD=pc', '-DTUT_ARCH=x86_64',
'-DTUTORIAL_DIR=hello-camkes-1', '..']>: exit code not set, waiting on pid
-- The C compiler identification is GNU 7.3.1
-- The CXX compiler identification is GNU 7.3.1
-- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc
-- Check for working C compiler: /opt/rh/devtoolset-7/root/usr/bin/gcc --
works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
-- Check for working CXX compiler: /opt/rh/devtoolset-7/root/usr/bin/g++
-- Check for working CXX compiler: /opt/rh/devtoolset-7/root/usr/bin/g++ --
works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- The ASM compiler identification is GNU
-- Found assembler: /opt/rh/devtoolset-7/root/usr/bin/gcc
CMake Error at projects/sel4-tutorials/cmake/helpers.cmake:141 (message):
Failed to render:
PYTHONPATH=/home/john/sel4/projects/camkes/capdl/python-capdl-tool;python;/home/john/sel4/projects/sel4-tutorials/template.py;--tut-file;/home/john/sel4/projects/sel4-tutorials/tutorials/hello-camkes-1/hello-camkes-1;--out-dir;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/hello-camkes-1/gen;--input-files;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/input_files;--output-files;/home/john/sel4/hello-camkes-1_build/projects/sel4-tutorials/output_files;--arch;x86_64;;;,
Traceback (most recent call last):
File "/home/john/sel4/projects/sel4-tutorials/template.py", line 154,
in <module>
sys.exit(main())
File "/home/john/sel4/projects/sel4-tutorials/template.py", line 142,
in main
render_file(args, env, state, file)
File "/home/john/sel4/projects/sel4-tutorials/template.py", line 90, in
render_file
out_stream.write(template.render(context.get_context(args, state)))
File "/home/john/sel4/projects/sel4-tutorials/tools/context.py", line
435, in get_context
context.update(ObjectType.__members__.items())
AttributeError: type object 'ObjectType' has no attribute '__members__'
Call Stack (most recent call first):
projects/sel4-tutorials/cmake/helpers.cmake:164 (ExecuteGenerationProcess)
projects/sel4-tutorials/CMakeLists.txt:29 (GenerateTutorial)
-- Configuring incomplete, errors occurred!
See also "/home/john/sel4/hello-camkes-1_build/CMakeFiles/CMakeOutput.log".
Traceback (most recent call last):
File "./init", line 91, in <module>
File "./init", line 81, in main
File "/home/john/sel4/projects/sel4-tutorials/common.py", line 107, in
init_directories
return _init_build_directory(config, initialised, build_directory,
tute_directory, output, config_dict=config_dict)
File "/home/john/sel4/projects/sel4-tutorials/common.py", line 69, in
_init_build_directory
result = sh.cmake(args + ['..'], _cwd = directory, _out=output,
_err=output)
File "/sandbox/lib/python2.7/site-packages/sh.py", line 1427, in __call__
return RunningCommand(cmd, call_args, stdin, stdout, stderr)
File "/sandbox/lib/python2.7/site-packages/sh.py", line 774, in __init__
self.wait()
File "/sandbox/lib/python2.7/site-packages/sh.py", line 792, in wait
self.handle_command_exit_code(exit_code)
File "/sandbox/lib/python2.7/site-packages/sh.py", line 815, in
handle_command_exit_code
raise exc
sh.ErrorReturnCode_1:
RAN: /sandbox/bin/cmake -DCMAKE_TOOLCHAIN_FILE=../kernel/gcc.cmake -G
Ninja -DTUT_BOARD=pc -DTUT_ARCH=x86_64 -DTUTORIAL_DIR=hello-camkes-1 ..
STDOUT:
STDERR:
