sel4 / camkes-vm-examples Goto Github PK
View Code? Open in Web Editor NEWLicense: Other
License: Other
Hi,
I read the doc https://github.com/seL4/camkes-vm under Serial, know that i can use @m
to control vm,but i don't know where to send @m
, and how to send it.
I just want to switch the command shell between two vms on my board which started the app vm_multi.
How can i fix it ?
I've been testing some more CI configurations and ran into some issues with QEMU/ARMv7 CMake that prevent this from working nicely. Once these are resolved, building VM_minimal
for QEMU/ARMv7 works, but it still misses a 32-bit linux image. There should at least be a warning in CMake scripts that this is unsupported. I'm not sure if this platform has worked once and just needs the linux images, or if there more that needs to be done. There seems not much practical value in ARMv7 virtualization nowadays.
Hi!
I'm trying to build the x86_64 example because I can read:
"Boot images/kernel-x86_64-pc99 and images/capdl-loader-experimental-image-x86_64-pc99"
anyway, whenever I try to build x86_64 with:
../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=x86_64
or
../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=x86
or
../init-build.sh -DCAMKES_VM_APP=vm_minimal
all of them fail with this error:
hugo@anakin:~/camkes-vm-examples/build$ ../init-build.sh -DCAMKES_VM_APP=vm_minimal
loading initial cache file /home/hugo/camkes-vm-examples/projects/vm-examples/settings.cmake
CMake Error at apps/Arm/vm_minimal/settings.cmake:9 (message):
PLATFORM: x86 not supported.
Supported: tk1;tx1;tx2;exynos5422;qemu-arm-virt;odroidc2
Call Stack (most recent call first):
settings.cmake:67 (include)
-- Configuring incomplete, errors occurred!
So, documentation is referencing a "kernel-x86_64-pc99" kernel, which looks like a x86_64 platform, but at the very beginning it says "x86_64 (coming)". Not sure if there's support and if not, should the documentation be fixed to avoid confusion?
Best,
In https://github.com/seL4/camkes-vm-examples/actions/runs/7696538606?pr=57 the run "Hardware (nehalem)" was cancelled with the message Canceling since a higher priority waiting request for 'camkes-hw-pr-0' exists
. There are are few PRs running in parallel and it feels like something in #60 is still not working as expected. The hardware runs should queue up nicely, but not cancel others other.
How do I port this to raspberry pi 4B?
I have practiced with reference to this repository, but got an error:
https://github.com/second-state/wasmedge-seL4/wiki/%5BWIP%5D-seL4-on-Raspberry-Pi-4
Booting all finished, dropped to user space
[email protected]:66 Simple FDT helper failed to read path (-22, /soc/timer@7e003000)
bcm_system_timer_init@system_timer.c: 214 Failed to allocate with fdt
[email protected]:112 system timer initialisation failed
post_init@time_server.c:231 [Cond failed: error]
Failed to init timer
[email protected]:1156 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1)
[email protected]:266 Failed to find any untyped capable of creating an object at address 0xff846000
Loading Linux: 'linux' dtb: ''
[email protected]:651 module name: map_frame_hack
[email protected]:651 module name: init_ram
[email protected]:651 module name: virtio_con
[email protected]:651 module name: cross_vm_connections
libsel4muslcsys: Error attempting syscall 215
libsel4muslcsys: Error attempting syscall 215
how do i handle it?
I can't find where these tests are now running?
CI does not cover apps/Arm/vm_introspect
, see https://github.com/seL4/ci-actions/blob/master/camkes-vm/builds.yml with the current coverage. At least a build for all examples should happen.
[Failed build]
Traceback (most recent call last):
File "/usr/lib/python3.8/runpy.py", line 194, in _run_module_as_main
return _run_code(code, main_globals, None,
File "/usr/lib/python3.8/runpy.py", line 87, in _run_code
exec(code, run_globals)
File "/home/jingjin/workspace/sel4-hypervisor/projects/camkes-tool/camkes/runner/main.py", line 316, in
sys.exit(main(sys.argv, sys.stdout, sys.stderr))
File "/home/jingjin/workspace/sel4-hypervisor/projects/camkes-tool/camkes/runner/main.py", line 292, in main
g = r.render(i, assembly, template, render_state, obj_key,
File "/home/jingjin/workspace/sel4-hypervisor/projects/camkes-tool/camkes/runner/Renderer.py", line 89, in render
t = self.env.get_template(template)
File "/usr/lib/python3/dist-packages/jinja2/environment.py", line 830, in get_template
return self._load_template(name, self.make_globals(globals))
File "/usr/lib/python3/dist-packages/jinja2/environment.py", line 804, in _load_template
template = self.loader.load(self, name, globals)
File "/usr/lib/python3/dist-packages/jinja2/loaders.py", line 405, in load
return loader.load(environment, name, globals)
File "/usr/lib/python3/dist-packages/jinja2/loaders.py", line 125, in load
code = environment.compile(source, name, filename)
File "/usr/lib/python3/dist-packages/jinja2/environment.py", line 591, in compile
self.handle_exception(exc_info, source_hint=source_hint)
File "/usr/lib/python3/dist-packages/jinja2/environment.py", line 780, in handle_exception
reraise(exc_type, exc_value, tb)
File "/usr/lib/python3/dist-packages/jinja2/_compat.py", line 37, in reraise
raise value.with_traceback(tb)
File "/home/jingjin/workspace/sel4-hypervisor/projects/vm/templates/seL4VMParameters.template.c", line 23, in
/- set entry_offset = 0x80000 if is_64_bit else 0x8000 -/
File "/usr/lib/python3/dist-packages/jinja2/environment.py", line 497, in _parse
return Parser(self, source, name, encode_filename(filename)).parse()
File "/usr/lib/python3/dist-packages/jinja2/parser.py", line 901, in parse
result = nodes.Template(self.subparse(), lineno=1)
File "/usr/lib/python3/dist-packages/jinja2/parser.py", line 888, in subparse
self.stream.expect('block_end')
File "/usr/lib/python3/dist-packages/jinja2/lexer.py", line 386, in expect
raise TemplateSyntaxError("expected token %r, got %r" %
jinja2.exceptions.TemplateSyntaxError: expected token 'end of statement block', got 'x80000'
[299/388] Building C object kernel/CMakeFiles/kernel.elf.dir/kernel_all.c.obj
image
repo init -u https://github.com/seL4/camkes-vm-examples-manifest.git
repo sync
mkdir build
cd build
../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt -DAARCH64=TRUE
ninja
../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt
logs:
[304/385] Generating capDL-tool/parse-capDL
FAILED: capDL-tool/parse-capDL /home/luffy/workspace/github/sel4-vm-example/build/capDL-tool/parse-capDL
cd /home/luffy/workspace/github/sel4-vm-example/build/capDL-tool && printf capDL-tool/parse-capDL:\ > /home/luffy/workspace/github/sel4-vm-example/build/capDL-tool/parse-capDL.d && find -L /home/luffy/workspace/github/sel4-vm-example/projects/capdl/capDL-tool/ -type f -printf %p\ >> /home/luffy/workspace/github/sel4-vm-example/build/capDL-tool/parse-capDL.d && cp -a /home/luffy/workspace/github/sel4-vm-example/projects/capdl/capDL-tool/* . && /home/luffy/workspace/tools/cmake-3.24.0-rc3-linux-x86_64/bin/cmake -E env make && mkdir -p /home/luffy/workspace/github/sel4-vm-example/.sel4_cache/capDL-tool/04d18331a3ec4f4b408937b7b72886aa && tar -zcf code.tar.gz -C /home/luffy/workspace/github/sel4-vm-example/build/capDL-tool/ parse-capDL && mv code.tar.gz /home/luffy/workspace/github/sel4-vm-example/.sel4_cache/capDL-tool/04d18331a3ec4f4b408937b7b72886aa/
stack build --fast
Downloading lts-19.12 build plan ...
RedownloadFailed Request {
host = "raw.githubusercontent.com"
port = 443
secure = True
requestHeaders = []
path = "/fpco/lts-haskell/master//lts-19.12.yaml"
queryString = ""
method = "GET"
proxy = Nothing
rawBody = False
redirectCount = 10
responseTimeout = ResponseTimeoutDefault
requestVersion = HTTP/1.1
}
"/home/luffy/.stack/build-plan/lts-19.12.yaml" (Response {responseStatus = Status {statusCode = 404, statusMessage = "Not Found"}, responseVersion = HTTP/1.1, responseHeaders = [("Connection","keep-alive"),("Content-Length","14"),("Content-Security-Policy","default-src 'none'; style-src 'unsafe-inline'; sandbox"),("Strict-Transport-Security","max-age=31536000"),("X-Content-Type-Options","nosniff"),("X-Frame-Options","deny"),("X-XSS-Protection","1; mode=block"),("Content-Type","text/plain; charset=utf-8"),("X-GitHub-Request-Id","FF6A:572A:28389:32C8B:638FF70A"),("Accept-Ranges","bytes"),("Date","Wed, 07 Dec 2022 02:14:34 GMT"),("Via","1.1 varnish"),("X-Served-By","cache-tyo11937-TYO"),("X-Cache","MISS"),("X-Cache-Hits","0"),("X-Timer","S1670379275.513819,VS0,VE236"),("Vary","Authorization,Accept-Encoding,Origin"),("Access-Control-Allow-Origin","*"),("X-Fastly-Request-ID","0c35d2a057b850289454425d205f8e919dbf0b12"),("Expires","Wed, 07 Dec 2022 02:19:34 GMT"),("Source-Age","0")], responseBody = (), responseCookieJar = CJ {expose = []}, responseClose' = ResponseClose})
Makefile:51: recipe for target 'parse-capDL' failed
make: *** [parse-capDL] Error 1
[306/385] Performing CAmkES generation for 20 files
ninja: build stopped: subcommand failed.
This uses the repo https://github.com/SEL4PROJ/linux-tegra, which has not been migrated to https://github.com/sel4 yet. Are there any license issues preventing this or is this just another open maintenance task?
Separate CI build and simulation run, so the building queue is no blocked by the simulation getting stuck. Currently, if a build is for a platform that has a simulation, the python script in the ci-actions repo will start the simulation immediately after the build. See e.g. https://github.com/seL4/ci-actions/blob/0161435968ab9d2811e478c4c6e32bb0d4f5f4fb/camkes-vm/build.py#L46-L50 how it it implemented at the moment. Once we have split build and simulation, we could also run simulation in parallel then.
I follow the step to build the camkes arm vmm.
I got some errors when I run ../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt
.
CMake Error at CMakeLists.txt:12 (find_package):
By not providing "Findcamkes-arm-vm.cmake" in CMAKE_MODULE_PATH this
project has asked CMake to find a package configuration file provided by
"camkes-arm-vm", but CMake did not find one.
Could not find a package configuration file provided by "camkes-arm-vm"
with any of the following names:
camkes-arm-vmConfig.cmake
camkes-arm-vm-config.cmake
Add the installation prefix of "camkes-arm-vm" to CMAKE_PREFIX_PATH or set
"camkes-arm-vm_DIR" to a directory containing one of the above files. If
"camkes-arm-vm" provides a separate development package or SDK, be sure it
has been installed.
How can I solve this problem?
Hi,
I try to follow the documentation to build.
And it generate two image capdl-loader-image-x86_64-pc99 and kernel-x86_64-pc99.
What is different between them ?
And how can I use them to run on a real platform ?
Thanks !
Hi,
Here is the instruction that i did for running images on qemu:
#in build directory(build_vm)
sudo qemu-system-x86_64 -m 512 -kernel images/kernel-ia32-pc99 -initrd images/capdl-loader-image-ia32-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic
#output
Boot config: parsing cmdline 'images/kernel-ia32-pc99 '
Boot config: console_port = 0x3f8
Boot config: debug_port = 0x3f8
Boot config: disable_iommu = false
Detected 1 boot module(s):
module #0: start=0x149000 end=0x175ad18 size=0x1611d18 name='images/capdl-loader-image-ia32-pc99'
Parsing GRUB physical memory map
Physical Memory Region from 0 size 9fc00 type 1
Physical Memory Region from 9fc00 size 400 type 2
Physical Memory Region from f0000 size 10000 type 2
Physical Memory Region from 100000 size 1fee0000 type 1
Adding physical memory region 0x100000-0x1fc00000
Physical Memory Region from 1ffe0000 size 20000 type 2
Physical Memory Region from feffc000 size 4000 type 2
Physical Memory Region from fffc0000 size 40000 type 2
Multiboot gave us no video information
ACPI: RSDP paddr=0xf6860
ACPI: RSDP vaddr=0xdfcf6860
ACPI: RSDT paddr=0x1ffe1656
ACPI: RSDT vaddr=0xdffe1656
WARNING SKIM window not enabled, this machine is probably vulernable to Meltdown (https://www.meltdownattack.com), consider enabling
Kernel loaded to: start=0x100000 end=0x148000 size=0x48000 entry=0x100076
ACPI: RSDT paddr=0x1ffe1656
ACPI: RSDT vaddr=0xdffe1656
ACPI: FADT paddr=0x1ffe14aa
ACPI: FADT vaddr=0xdffe14aa
ACPI: FADT flags=0x80a5
ACPI: 0 IOMMUs detected
ACPI: MADT paddr=0x1ffe159e
ACPI: MADT vaddr=0xdffe159e
ACPI: MADT apic_addr=0xfee00000
ACPI: MADT flags=0x1
ACPI: MADT_APIC apic_id=0x0
ACPI: MADT_APIC apic_id=0x1
ACPI: Not recording this APIC, only support 1
ACPI: MADT_IOAPIC ioapic_id=0 ioapic_addr=0xfec00000 gsib=0
ACPI: MADT_ISO bus=0 source=0 gsi=2 flags=0x0
ACPI: MADT_ISO bus=0 source=5 gsi=5 flags=0xd
ACPI: MADT_ISO bus=0 source=9 gsi=9 flags=0xd
ACPI: MADT_ISO bus=0 source=10 gsi=10 flags=0xd
ACPI: MADT_ISO bus=0 source=11 gsi=11 flags=0xd
ACPI: 1 CPU(s) detected
ELF-loading userland images from boot modules:
size=0x2027000 v_entry=0x8051870 v_start=0x8048000 v_end=0xa06f000 p_start=0x175b000 p_end=0x3782000
Moving loaded userland images to final location: from=0x175b000 to=0x148000 size=0x2027000
Starting node #0 with APIC ID 0
XSAVE not supported
seL4 called fail at /home/hedi/camkes_vm_examples/kernel/src/arch/x86/kernel/boot_sys.c:785 in function boot_sys, saying "boot_sys failed for some reason :(
"
halting...
Kernel entry via Interrupt, irq 0
Hedi/
I am a newbie to SeL4 and followed the step by step process to build camkes-vm-linux project
but it fails while running ninja and the output is as follows
ubuntu@ubuntu1804:~/sel4-tutorials-manifest/b11_build$ ninja
[5/427] Performing configure step for 'hello-app'
FAILED: hello-app-stamp/hello-app-configure
cd /home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app && /usr/local/bin/cmake -DCMAKE_BUILD_TYPE=Debug -DCMAKE_TOOLCHAIN_FILE=/home/ubuntu/sel4-tutorials-manifest/tools/seL4/cmake-tool/polly_toolchains/linux-gcc-32bit-pic.cmake -GNinja /home/ubuntu/sel4-tutorials-manifest/b11/pkg/hello && /usr/local/bin/cmake -E touch /home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app-stamp/hello-app-configure
-- [polly] Used toolchain: Linux / gcc / PIC / c++11 support / 32 bit
-- The C compiler identification is GNU 7.5.0
-- Check for working C compiler: /usr/bin/gcc
-- Check for working C compiler: /usr/bin/gcc -- broken
CMake Error at /usr/local/share/cmake-3.13/Modules/CMakeTestCCompiler.cmake:52 (message):
The C compiler
"/usr/bin/gcc"
is not able to compile a simple test program.
It fails with the following output:
Change Dir: /home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app/CMakeFiles/CMakeTmp
Run Build Command:"/usr/bin/ninja-build" "cmTC_ac0a4"
[1/2] Building C object CMakeFiles/cmTC_ac0a4.dir/testCCompiler.c.o
[2/2] Linking C executable cmTC_ac0a4
FAILED: cmTC_ac0a4
: && /usr/bin/gcc -m32 -fPIC CMakeFiles/cmTC_ac0a4.dir/testCCompiler.c.o -o cmTC_ac0a4 && :
/usr/bin/ld: cannot find Scrt1.o: No such file or directory
/usr/bin/ld: cannot find crti.o: No such file or directory
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/7/libgcc.a when searching for -lgcc
/usr/bin/ld: cannot find -lgcc
/usr/bin/ld: skipping incompatible /usr/lib/gcc/x86_64-linux-gnu/7/libgcc.a when searching for -lgcc
/usr/bin/ld: cannot find -lgcc
collect2: error: ld returned 1 exit status
ninja: build stopped: subcommand failed.
CMake will not be able to correctly generate this project.
Call Stack (most recent call first):
CMakeLists.txt:5 (project)
-- Configuring incomplete, errors occurred!
See also "/home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app/CMakeFiles/CMakeOutput.log".
See also "/home/ubuntu/sel4-tutorials-manifest/b11_build/hello-app/CMakeFiles/CMakeError.log".
What changes are to be made and How do I solve this.
Support hw-test CI run for this repo also, so we can verify PRs do not break anything. Currently, the way to do such a test is via a dummy PR in the camkes-vm repo.
Hi,
I have already boot the vm on the sel4 hypervisor, but it used the ramdisk(in-memory initrd). I want to know how can i switch to use SD mmc partition to store the file persistently.Can i change the bootargs in camkes file from “root=/dev/mem” to "root=/dev/blkxxxxp1"? It is really useful to me.
Thanks,
Comet
After building vm_multi app for qemu and running ./simulate in my build directory, the console always printed the log "udhcpc: sending discover",which indicating udhcpc can not return. Meanwhile, your prebuilt rootfs did not support brctl in busybox judging from error log "/etc/init.d/S90bridge_setup: line 12: brctl: not found".
The related log was shown as follows:
Starting syslogd: OK
Starting syslogd: OK
Starting syslogd: OK
Starting klogd: OK
Starting klogd: OK
Starting klogd: OK
Running sysctl: OK
Running sysctl: OK
Running sysctl: OK
Initializing random number generator... [ 43.352936] random: dd: uninitialized urandom read (512 bytes read)
done.
Initializing random number generator... [ 43.476458] random: dd: uninitialized urandom read (512 bytes read)
done.
Initializing random number generator... [ 44.130296] random: dd: uninitialized urandom read (512 bytes read)
done.
Starting network: OK
Starting network: OK
Starting network: OK
udhcpc: started, v1.31.0
udhcpc: started, v1.31.0
/etc/init.d/S90bridge_setup: line 12: brctl: not found
Welcome to Buildroot
[ 53.859732] random: mktemp: uninitialized urandom read (6 bytes read)
[ 53.967484] random: mktemp: uninitialized urandom read (6 bytes read)
udhcpc: sending discover
udhcpc: sending discover
udhcpc: sending discover
udhcpc: sending discover
udhcpc: sending discover
udhcpc: sending discover
udhcpc: sending discover
udhcpc: sending discover
udhcpc: sending discover
These two errors may have some interdependency. Is the expected resutl for the vm_multi that an ip address will be respectively given to eth0 and br0?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.