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 can't find where these tests are now running?

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 !

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.

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?

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?

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.

../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.

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.

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.

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

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?

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,

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/

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?

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.