sel4 / camkes-vm Goto Github PK

View Code? Open in Web Editor NEW

21.0 21.0 35.0 222.15 MB

Virtual Machine built as a CAmkES component.

License: Other

C 92.85% CMake 7.15%

camkes

camkes-vm's Introduction

The seL4 microkernel

This project contains the source code of seL4 microkernel.

For details about the seL4 microkernel, including details about its formal correctness proof, please see the sel4.systems website and associated FAQ.

DOIs for citing recent releases of this repository:

We welcome contributions to seL4. Please see the website for information on how to contribute.

This repository is usually not used in isolation, but as part of the build system in a larger project.

seL4 Basics

Community

See the contact links on the seL4 website for the full list.

Reporting security vulnerabilities

If you believe you have found a security vulnerability in seL4 or related software, we ask you to follow our vulnerability disclosure policy.

Manual

A hosted version of the manual for the most recent release can be found here.

A web version of the API can be found here

Repository Overview

include and src: C and ASM source code of seL4
tools: build tools
libsel4: C bindings for the seL4 ABI
manual: LaTeX sources of the seL4 reference manual

Build Instructions

See the seL4 website for build instructions.

Status

A list of releases and current project status can be found under seL4 releases.

Roadmap: new features in development
Hardware Support: information about hardware platform ports
Kernel Features: information about available kernel features
Userland Components and Drivers: available device drivers and userland components

License

See the file LICENSE.md.

camkes-vm's People

Contributors

Stargazers

Watchers

camkes-vm's Issues

How to bind a guest OS to a physical core in aarch64?

Hi! I'm new to the seL4 kernel. So I wander is there any way to specify the guest OS to run only on the specified physical core of aarch64?
I tried to set affinity attributes using the vm_multi of camkes VM projects on qemu-arm-virt platform, and called the seL4_DebugDumpScheduler() after all the vm are created.
Here is the affinity setting:

// projects/vm-examples/apps/Arm/vm_multi/vm_multi.camkes:
...
        vm0.affinity = 0;
        vm1.affinity = 1;
        vm2.affinity = 2;
...

Here is the qemu command:

qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic  -m size=2048  -kernel images/capdl-loader-image-arm-qemu-arm-virt -smp 4

And the output of the debug infos:

// on core 2
Dumping all tcbs!
Name                                            State           IP                       Prio    Core
--------------------------------------------------------------------------------------
                                 vm2:dtb        blocked on recv 0x4084e4                         254    2
                       vm2:fault_handler        blocked on recv 0x4084e4                         255    2
                             vm2:control                running 0x400580                         101    2
                             idle_thread                   idle 0                          0    2
// on core 1
Dumping all tcbs!
Name                                            State           IP                       Prio    Core
--------------------------------------------------------------------------------------
                                 vm1:dtb        blocked on recv 0x4084e4                         254    1
                       vm1:fault_handler        blocked on recv 0x4084e4                         255    1
                             vm1:control                running 0x400580                         101    1
                             idle_thread                   idle 0                          0    1
// on core 0
Dumping all tcbs!
Name                                            State           IP                       Prio    Core
--------------------------------------------------------------------------------------
                                   vm0:0                restart 0x40080000                        99    0
                 child of: 'vm0:control'        blocked on ntfn 0x41debc                         101    0
                                   vm1:0                restart 0x48080000                        99    0
                                   vm2:0                restart 0x50080000                        99    0
                   vm2_vm0:fault_handler        blocked on recv 0x4003f4                         255    0
                         vm2_vm0:control        blocked on recv 0x4003f4                         254    0
                   vm1_vm0:fault_handler        blocked on recv 0x4003f4                         255    0
                         vm1_vm0:control        blocked on recv 0x4003f4                         254    0
                                 vm0:dtb        blocked on recv 0x4084e4                         254    0
                       vm0:fault_handler        blocked on recv 0x4084e4                         255    0
                             vm0:control                running 0x400580                         101    0
                   time_server:the_timer        blocked on recv 0x403a50                         255    0
                 time_server:hwtimer_irq        blocked on ntfn 0x40611c                         255    0
               time_server:fault_handler        blocked on recv 0x401c60                         255    0
                     time_server:control        blocked on recv 0x401c60                         255    0
                       serial:serial_dev        blocked on ntfn 0x407914                         254    0
                  serial:processed_batch        blocked on recv 0x4081e4                         254    0
                          serial:getchar        blocked on recv 0x408fc8                         254    0
                    serial:fault_handler        blocked on recv 0x402dec                         255    0
                          serial:control        blocked on ntfn 0x4002ac                         254    0
                           fserv:fs_ctrl        blocked on recv 0x401e38                         254    0
                     fserv:fault_handler        blocked on recv 0x400804                         255    0
                           fserv:control        blocked on recv 0x400804                         254    0
                             idle_thread                   idle 0                          0    0
                              rootserver               inactive 0x4006f8                         255    0

The dumps show that vm0:0 vm1:0 and vm2:0 are all bound to core 0, and only some vmm related threads are submitted to the affinity setting.
Are all the guest OS only running on the core 0 or schedured to running on the random free core in this cricumstance?

qemu V7.0 virt changed value of GIC_IRQ_PHANDLE

Hi all,

For the time server our team ported a timer into the qemu v7.0 virt platform. We also do not provide a dtb for the vm during compilation but let the seL4 system modify the system device tree during runtime. When we tried to run the vm_serial_server example, however we did not get any output.

The root of the problem was a wrong value of GIC_IRQ_PHANDLE, in our case it moved from 0x8001 to 0x8002. The Linux kernel did not initialize the virtual pci interface because of the wrong phandle value and therefore hvc0 was also not initialized. In our qemu dtb the phandle was used by the cpu.

I then looked more into how the qemu virt platform assigns these phandle values. They are incremented for each added phandle. Also the cpu cores are added to the device tree before the gic and for each cpu core a new phandle is assigned to it. Therefore, depending on the number of available cores, the phandle value will also change.

I am not sure how to take it from here. Possible solutions to mitigate this problem could be:

Document this problem in the howto. Something along the lines if a custome qemu is used, look into that qemus dtb and update GIC_IRQ_PHANDLE value accordingly.
Automatically find the gic in the devicetree during compilation time and set the GIC_IRQ_PHANDLE to the correct value.
Parse the dtb at runtime to find the correct phandle and use that for the added devices during runtime.

Security vuln in Satadriver: read/write past partition boundary.

components/Sataserver/src/sataserver.c has the following code for read (and very similar for write):

        found = calulate_sector_offset(client, &offset, (uint32_t)sector);
        if (found) {
            err = sata_read_sectors(&sata_driver, drive, len / SATA_BLK_SIZE, sector + offset, packet);

where len is up to 4096, and sector is in SATA_BLK_SIZE units (typically, 512). This means that if sector points to a location within <8 blocks of the end of a partition, the read/write can go up to 3584 bytes past the end of partition, exposing up to 7 sectors at the beginning of the next partition, even if that partition is configured to be inaccessible to the Sataserver.

I fixed that bug while at HRL under DARPA HACMS contract; DARPA have subsequently released the code under distribution A. Attached patch was received directly from DARPA without any nondisclosure conditions
0002-Fixed-several-bugs-in-the-storage-driver.patch.

Note that there was an issue with this - it eliminates the limit in the buffer size for read/write. This did not cause issues with Ubuntu host, but did cause issues with CentOS hosts. A possible fix (which was not included in the DARPA-released code) is to support partial reads/writes.

delete merged branch "spdx"

Seems we can delete the merged branch "spdx"

Provide a label "hw-build"

Provide a label "hw-build" in addition to the existing "hw-test". That allows taking away some load from the CI board farm, as we can test separately if a PR does not break builds anywhere.

CNode_Revoke failed when reset resources

I want to reboot vm0 component, but it was failed when reset resources.

so i do some test. i direct revoke after untyped retype, it was also failed.

Have u meet the same issue?
BR

fileserver heap set to be 165536 bytes looks broken

I wonder if seL4/seL4_libs@cf6f917 (from seL4/seL4_libs#63, related also seL4/camkes-tool#109) now make an issue show up. Looking at:

camkes-vm/components/VM_Arm/configurations/vm.h

Lines 98 to 99 in 66183e9

 #define VM_GENERAL_CONFIGURATION_DEF() \ 

 fserv.heap_size = 165536; \

I wonder why the fileserver heap is set to the size 100000 + 2^16, and if this is supposed to work actually. I'm currently getting an error in the file server from sys_morecore.c, it complains at
https://github.com/seL4/seL4_libs/blob/cf6f9177da2694bee6a878cd426a9d66b034d066/libsel4muslcsys/src/sys_morecore.c#L198
that it can't hand out a memory block that is not 4 KiB aligned. However, with this heap initialization, this happen for me as memory is taken from the (unaligned) end.
Am I the only one running into this with the minimal VM example (using the cutting edge repo version and a custom build system)? My generated camkes.c contains

static char ALIGN(PAGE_SIZE_4K) heap [165536];

the symbol table of the ELF file has

00000000013c5000 l     O .bss	00000000000286a0 heap

an my customized debug logs eventually fail with

init_morecore_region@sys_morecore.c:125 morecore 0x13c5000 - 0x13ed6a0 (165536/0x286A0)
sys_mmap_impl_static@sys_morecore.c:207 [Cond failed: (base % 0x1000) != 0]
	morecore 0x13c5000 - 0x13ed6a0, len 0x1000, return address: 0x13ec6a0 (not 4 KiB aligned)

See we should fix the value and also ass some sanity checks in CAmkES that align down the heap values to a multiple of 4 KiB.

Do not run dispatch workflow action on github repo forks

Do not run dispatch workflow action on github repo forks, because they fail die to missing access rights

trigger.yaml
on push
Run seL4/ci-actions/trigger@master
/home/runner/work/_actions/seL[4](https://github.com/axel-h/camkes-vm/runs/6323832364?check_suite_focus=true#step:2:4)/ci-actions/master/js/../trigger/steps.sh
Need $INPUT_TOKEN for authentication.
Error: Action trigger failed.

This issue happen in other repos also, see e.g. seL4/docs#135

Dont hard-code GIC_IRQ_PHANDLE, read it from device tree instead

Follow-up from #42 (comment)

Remove the hard coded GIC_IRQ_PHANDLE define and take the value from the device tree instead. Or add at least a sanity check that the hard-coded values machtes the device tree.

There have been cases, where the phande changes, and that causes strange errors then.
See also #27

qemu-arm-virt turns on smp and reports an error when running

I followed the tutorial at https://github.com/seL4/camkes-vm-examples and tried to use qemu to simulate the environment of arm64 to run sel4 and start the linux virtual machine. At present, the single-core case can run correctly, but the multi-core error is reported:
This is my operation

1.
bst@bst-Vostro-3671:~/chenyu/sel4-arm64/build$ ../init-build.sh -DCAMKES_VM_APP=vm_minimal -DPLATFORM=qemu-arm-virt -DNUM_NODES=2
loading initial cache file /home/bst/chenyu/sel4-arm64/projects/vm-examples/settings.cmake
-- Set platform details from PLATFORM=qemu-arm-virt
--   KernelPlatform: qemu-arm-virt
-- Found seL4: /home/bst/chenyu/sel4-arm64/kernel  
-- Default cpu specified for virt board: cortex-a53
-- QEMU MEMORY is: 2048
-- 
-- Default cpu specified for virt board: cortex-a53
-- QEMU MEMORY is: 2048
-- 
-- Found GCC with prefix aarch64-linux-gnu-
-- The C compiler identification is GNU 9.4.0
-- The CXX compiler identification is GNU 9.4.0
-- The ASM compiler identification is GNU
-- Found assembler: /usr/bin/aarch64-linux-gnu-gcc
-- Check for working C compiler: /usr/bin/aarch64-linux-gnu-gcc
-- Check for working C compiler: /usr/bin/aarch64-linux-gnu-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: /usr/bin/aarch64-linux-gnu-g++
-- Check for working CXX compiler: /usr/bin/aarch64-linux-gnu-g++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Found camkes-arm-vm: /home/bst/chenyu/sel4-arm64/projects/vm  
-- Found camkes-tool: /home/bst/chenyu/sel4-arm64/projects/camkes-tool  
-- Found global-components: /home/bst/chenyu/sel4-arm64/projects/global-components  
-- Found camkes-vm: /home/bst/chenyu/sel4-arm64/projects/vm  
-- Found camkes-vm-images: /home/bst/chenyu/sel4-arm64/projects/camkes-vm-images  
-- Found sel4_projects_libs: /home/bst/chenyu/sel4-arm64/projects/seL4_projects_libs  
-- Found elfloader-tool: /home/bst/chenyu/sel4-arm64/tools/seL4/elfloader-tool  
-- Found musllibc: /home/bst/chenyu/sel4-arm64/projects/musllibc  
-- Found util_libs: /home/bst/chenyu/sel4-arm64/projects/util_libs  
-- Found seL4_libs: /home/bst/chenyu/sel4-arm64/projects/seL4_libs  
-- Found projects_libs: /home/bst/chenyu/sel4-arm64/projects/projects_libs  
-- Found capdl: /home/bst/chenyu/sel4-arm64/projects/capdl  
-- QEMU MEMORY is: 2048
-- 
-- /home/bst/chenyu/sel4-arm64/build/kernel/gen_headers/plat/machine/devices_gen.h is out of date. Regenerating from DTB...
-- CPIO test cpio_reproducible_flag PASSED
-- Detecting cached version of: capDL-tool
-- Found Git: /usr/bin/git (found version "2.25.1") 
--   Found valid cache entry for capDL-tool
-- Found sel4runtime: /home/bst/chenyu/sel4-arm64/projects/sel4runtime  
-- Performing Test compiler_arch_test
-- Performing Test compiler_arch_test - Success
-- libmuslc architecture: 'aarch64' (from KernelSel4Arch 'aarch64')
-- Detecting cached version of: musllibc
--   Found valid cache entry for musllibc
BenchUtiliz not available, as KernelArmExportPMUUser is OFF
-- Found camkes-vm-linux: /home/bst/chenyu/sel4-arm64/projects/vm-linux  
-- /home/bst/chenyu/sel4-arm64/build/ast.pickle is out of date. Regenerating...
-- /home/bst/chenyu/sel4-arm64/build/camkes-gen.cmake is out of date. Regenerating...
-- Configuring done
-- Generating done
-- Build files have been written to: /home/bst/chenyu/sel4-arm64/build
2
bst@bst-Vostro-3671:~/chenyu/sel4-arm64/build$ ninja 
[85/376] Building C object sel4_projects_libs/libsel4dma/CMakeFiles/sel4dma.dir/src/dma.c.obj
/home/bst/chenyu/sel4-arm64/projects/seL4_projects_libs/libsel4dma/src/dma.c:32:2: warning: #warning Unknown platform. DMA alignment defaulting to 32 bytes. [-Wcpp]
   32 | #warning Unknown platform. DMA alignment defaulting to 32 bytes.
      |  ^~~~~~~
[326/376] Building C object CMakeFiles/capdl-loader.dir/home/bst/chenyu/sel4-arm64/projects/capdl/capdl-loader-app/src/main.c.obj
/home/bst/chenyu/sel4-arm64/projects/capdl/capdl-loader-app/src/main.c: In function ‘get_capData’:
/home/bst/chenyu/sel4-arm64/projects/capdl/capdl-loader-app/src/main.c:154:18: note: parameter passing for argument of type ‘CDL_CapData’ {aka ‘struct <anonymous>’} changed in GCC 9.1
  154 | static seL4_Word get_capData(CDL_CapData d)
      |                  ^~~~~~~~~~~
[376/376] Generating images/capdl-loader-image-arm-qemu-arm-virt
3.
bst@bst-Vostro-3671:~/chenyu/sel4-arm64/build$ ./simulate --extra-qemu-args="-smp 2"
./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic  -m size=2048 -smp 2 -kernel images/capdl-loader-image-arm-qemu-arm-virt 
ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
  paddr=[61b48000..62fea0d7]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 61cce230.
Loaded DTB from 61cce230.
   paddr=[6024c000..6024dfff]
ELF-loading image 'kernel' to 60000000
  paddr=[60000000..6024bfff]
  vaddr=[8060000000..806024bfff]
  virt_entry=8060000000
ELF-loading image 'capdl-loader' to 6024e000
  paddr=[6024e000..61756fff]
  vaddr=[400000..1908fff]
  virt_entry=408f58
Boot cpu id = 0x0, index=0
Core 1 is up with logic id 1
Enabling hypervisor MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
available phys memory regions: 1
  [60000000..c0000000]
reserved virt address space regions: 3
  [8060000000..806024c000]
  [806024c000..806024de1f]
  [806024e000..8061757000]
Booting all finished, dropped to user space
<<seL4(CPU 0) [decodeUntypedInvocation/205 T0x80bc013400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>
Loading Linux: 'linux' dtb: 'linux-dtb'
[email protected]:651 module name: map_frame_hack
[email protected]:651 module name: init_ram
libsel4muslcsys: Error attempting syscall 215
libsel4muslcsys: Error attempting syscall 215
[email protected]:831 Failed to generate a fdt
Failed to load VM image
Halting...

I noticed that the fdt is not being generated correctly. Debugging with gdb, I found that sel4 will generate psci nodes for fdt, so I make changes:

bst@bst-Vostro-3671:~/chenyu/sel4-arm64/projects/vm/components/VM_Arm/plat_include/qemu-arm-virt/plat$ git diff vmlinux.h
diff --git a/components/VM_Arm/plat_include/qemu-arm-virt/plat/vmlinux.h b/components/VM_Arm/plat_include/qemu-arm-virt/plat/vmlinux.h
index e8ec49e..a51d06f 100644
--- a/components/VM_Arm/plat_include/qemu-arm-virt/plat/vmlinux.h
+++ b/components/VM_Arm/plat_include/qemu-arm-virt/plat/vmlinux.h
@@ -26,7 +26,7 @@ static const char *plat_keep_devices[] = {
     "/platform@c000000",
     "/pmu",
     "/flash@0",
-    "/psci",
+    //"/psci",
 };
 static const char *plat_keep_device_and_disable[] = {};
 static const char *plat_keep_device_and_subtree[] = {

Finally, I thought I entered the linux kernel, but there is a loop of printing:

ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
  paddr=[61b48000..62fea0d7]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at 61cce230.
Loaded DTB from 61cce230.
   paddr=[6024c000..6024dfff]
ELF-loading image 'kernel' to 60000000
  paddr=[60000000..6024bfff]
  vaddr=[8060000000..806024bfff]
  virt_entry=8060000000
ELF-loading image 'capdl-loader' to 6024e000
  paddr=[6024e000..61756fff]
  vaddr=[400000..1908fff]
  virt_entry=408f58
Boot cpu id = 0x0, index=0
Core 1 is up with logic id 1
Enabling hypervisor MMU and paging
Jumping to kernel-image entry point...

Bootstrapping kernel
available phys memory regions: 1
  [60000000..c0000000]
reserved virt address space regions: 3
  [8060000000..806024c000]
  [806024c000..806024de1f]
  [806024e000..8061757000]
Booting all finished, dropped to user space
^[[0m^[[30;1m<<^[[0m^[[32mseL4(CPU 0)^[[0m^[[30;1m [decodeUntypedInvocation/205 T0x80bc013400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>^[[0m
Loading Linux: 'linux' dtb: 'linux-dtb'
[email protected]:651 module name: map_frame_hack
[email protected]:651 module name: init_ram
libsel4muslcsys: Error attempting syscall 215
libsel4muslcsys: Error attempting syscall 215
[email protected]:266 Failed to find any untyped capable of creating an object at address 0x8020000
[email protected]:938 Grabbing the entire cap for device memory
[email protected]:941 Failed to grab the entire cap
[    0.000000] Booting Linux on physical CPU 0x0
[    0.000000] Linux version 4.9.189+ (alisonf@shinyu-un) (gcc version 6.3.0 20170516 (Debian 6.3.0-18) ) #16 SMP Tue Feb 25 14:14:50 AEDT 2020
[    0.000000] Boot CPU: AArch64 Processor [410fd034]
[    0.000000] efi: Getting EFI parameters from FDT:
[    0.000000] efi: UEFI not found.
[    0.000000] psci: probing for conduit method from DT.
[    0.000000] psci: PSCIv1.0 detected in firmware.
[    0.000000] psci: Using standard PSCI v0.2 function IDs
[    0.000000] psci: Trusted OS migration not required
[    0.000000] psci: SMC Calling Convention v1.0
[    0.000000] percpu: Embedded 22 pages/cpu s51608 r8192 d30312 u90112^M
[    0.000000] Detected VIPT I-cache on CPU0^M
[    0.000000] CPU features: enabling workaround for ARM erratum 845719^M
[    0.000000] Built 1 zonelists in Zone order, mobility grouping on.  Total pages: 129024^M
[    0.000000] Kernel command line:  maxcpus=2^M
[    0.000000] PID hash table entries: 2048 (order: 2, 16384 bytes)^M
[    0.000000] Dentry cache hash table entries: 65536 (order: 7, 524288 bytes)^M
[    0.000000] Inode-cache hash table entries: 32768 (order: 6, 262144 bytes)^M
[    0.000000] Memory: 490360K/524288K available (7484K kernel code, 1220K rwdata, 2524K rodata, 3776K init, 543K bss, 33928K reserved, 0K cma-reserved)^M
[    0.000000] Virtual kernel memory layout:^M
[    0.000000]     modules : 0xffff000000000000 - 0xffff000008000000   (   128 MB)^M
[    0.000000]     vmalloc : 0xffff000008000000 - 0xffff7dffbfff0000   (129022 GB)^M
[    0.000000]       .text : 0xffff000008080000 - 0xffff0000087d0000   (  7488 KB)^M
[    0.000000]     .rodata : 0xffff0000087d0000 - 0xffff000008a50000   (  2560 KB)^M
[    0.000000]       .init : 0xffff000008a50000 - 0xffff000008e00000   (  3776 KB)^M
[    0.000000]       .data : 0xffff000008e00000 - 0xffff000008f31200   (  1221 KB)^M
[    0.000000]        .bss : 0xffff000008f31200 - 0xffff000008fb9034   (   544 KB)^M
[    0.000000]     fixed   : 0xffff7dfffe7fb000 - 0xffff7dfffec00000   (  4116 KB)^M
[    0.000000]     PCI I/O : 0xffff7dfffee00000 - 0xffff7dffffe00000   (    16 MB)^M
[    0.000000]     vmemmap : 0xffff7e0000000000 - 0xffff800000000000   (  2048 GB maximum)^M
[    0.000000]               0xffff7e0000000000 - 0xffff7e0000800000   (     8 MB actual)^M
[    0.000000]     memory  : 0xffff800000000000 - 0xffff800020000000   (   512 MB)^M
[    0.000000] Hierarchical RCU implementation.^M
[    0.000000]  Build-time adjustment of leaf fanout to 64.^M
[    0.000000]  RCU restricting CPUs from NR_CPUS=256 to nr_cpu_ids=2.^M
[    0.000000] RCU: Adjusting geometry for rcu_fanout_leaf=64, nr_cpu_ids=2^M
[    0.000000] NR_IRQS:64 nr_irqs:64 0^M
[    0.000000] >>>>>> gic cpu init | CPU 0 | cpu_mask 0x1^M
[    0.000000] GICv2m: Invalid MSI base SPI (base:0)^M
[    0.000000] arm_arch_timer: Architected cp15 timer(s) running at 62.50MHz (virt).^M
[    0.000000] clocksource: arch_sys_counter: mask: 0xffffffffffffff max_cycles: 0x1cd42e208c, max_idle_ns: 881590405314 ns^M
[    0.000157] sched_clock: 56 bits at 62MHz, resolution 16ns, wraps every 4398046511096ns^M
[    0.011289] Console: colour dummy device 80x25^M
[    0.013115] console [tty0] enabled^M
[    0.013904] Calibrating delay loop (skipped), value calculated using timer frequency.. 125.00 BogoMIPS (lpj=250000)^M
[    0.014740] pid_max: default: 32768 minimum: 301^M
[    0.016122] Security Framework initialized^M
[    0.016209] Yama: becoming mindful.^M
[    0.017196] AppArmor: AppArmor disabled by boot time parameter^M
[    0.017738] Mount-cache hash table entries: 1024 (order: 1, 8192 bytes)^M
[    0.017807] Mountpoint-cache hash table entries: 1024 (order: 1, 8192 bytes)^M
[    0.033214] ftrace: allocating 26505 entries in 104 pages^M
[    0.208708] ASID allocator initialised with 32768 entries^M
[    0.223000] EFI services will not be available.^M
[    0.231891] Detected VIPT I-cache on CPU1^M
[    0.233481] >>>>>> gic cpu init | CPU 1 | cpu_mask 0x2^M
[    0.238295] CPU1: Booted secondary processor [410fd034]^M
[    0.239530] >>>> MAP for cpu: 0 | map: 1^M
[    0.240338] INJECTING SOFTIRQ -  multi map: 0x10000^M
[    0.244161] >>>> MAP for cpu: 0 | map: 1^M
[    0.244212] INJECTING SOFTIRQ -  multi map: 0x10000^M
[    0.245121] >>>> MAP for cpu: 1 | map: 2^M
[    0.245205] INJECTING SOFTIRQ -  multi map: 0x20000^M
[    0.256141] >>>> MAP for cpu: 0 | map: 1^M
[    0.256194] INJECTING SOFTIRQ -  multi map: 0x10000^M
[    0.256822] Brought up 2 CPUs^M
[    0.256895] SMP: Total of 2 processors activated.^M
[    0.257054] CPU features: detected feature: 32-bit EL0 Support^M
[    0.257136] CPU features: detected feature: Kernel page table isolation (KPTI)^M
[    0.257554] >>>> MAP for cpu: 1 | map: 2^M
[    0.257581] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.258930] >>>> MAP for cpu: 1 | map: 2^M
[    0.258976] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.259335] >>>> MAP for cpu: 1 | map: 2^M
[    0.259380] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.259761] >>>> MAP for cpu: 1 | map: 2^M
[    0.259805] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.260190] >>>> MAP for cpu: 1 | map: 2^M
[    0.260234] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.260615] >>>> MAP for cpu: 1 | map: 2^M
[    0.260659] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.261003] >>>> MAP for cpu: 1 | map: 2^M
[    0.261048] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.261437] >>>> MAP for cpu: 1 | map: 2^M
[    0.261482] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.261816] >>>> MAP for cpu: 1 | map: 2^M
[    0.261859] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.262184] >>>> MAP for cpu: 1 | map: 2^M
[    0.262384] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.263100] >>>> MAP for cpu: 1 | map: 2^M
[    0.263146] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.263442] >>>> MAP for cpu: 1 | map: 2^M
[    0.263486] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.263774] >>>> MAP for cpu: 1 | map: 2^M
[    0.263817] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.264123] >>>> MAP for cpu: 1 | map: 2^M
[    0.264167] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.264475] >>>> MAP for cpu: 1 | map: 2^M
[    0.264534] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.264829] >>>> MAP for cpu: 1 | map: 2^M
[    0.264873] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.265191] >>>> MAP for cpu: 1 | map: 2^M
[    0.265235] INJECTING SOFTIRQ -  multi map: 0x20001^M
[    0.265613] >>>> MAP for cpu: 1 | map: 2^M

@ Gerwin Klein
Can you help me with this problem?

delete branch revert-73-patch-axel-21

Now that #87 is merged and things work again, the branch branch revert-73-patch-axel-21 (https://github.com/seL4/camkes-vm/commits/revert-73-patch-axel-21) can be removed.

Not getting true interrupts

I am trying to run linux OS on camkes seL4 hypervisor. The hardware I use is x86-64. But I do not receive the interruptions of the devices that I have passed through, and Linux is managing the interruptions in the form of pooling.
This problem exists at the kernel level. Where the IO/APIC settings should be applied to the system but are not applied correctly. Is this problem solved in internal versions?

For example, physical interrupt 10 is defined for network hardware. Vector 58 is defined for this interval. The IO/APIC information used for this device is also specified. However, interrupts are not received correctly. (In fact, because the level trigger is set, interrupts are sent quickly, this is not true and causes a destructive effect on the performance of the guest OS)

Build for ARMv8 vm_minimal_sim build should not run QEMU

Now that we have separate build and HW-test steps, it might make sense to avoid running the QEMU simulation as part of the build for vm_minimal_sim, and have a dedicated simulation step here. The issue I am currently facing is, that the simulation fails hafer a few seconds, then the the queue is stuck for 50 min to recognize the failure and terminate the simulation.

This is what I'm seeing from https://github.com/seL4/camkes-vm/actions/runs/4684601834/jobs/8300924624?pr=81

2023-04-13T01:43:13.7011661Z Requested labels: ubuntu-latest
...
2023-04-13T01:46:05.5385900Z ##[group]vm_minimal_sim
2023-04-13T01:46:05.5386227Z �[1m-----------[ start test vm_minimal_sim ]-----------�[0m
2023-04-13T01:46:05.6144625Z �[33m+++ ../init-build.sh -DAARCH64=TRUE -DPLATFORM=qemu-arm-virt -DCAMKES_VM_APP=vm_minimal�[0m
2023-04-13T01:46:27.7973409Z [407/407] Generating images/capdl-loader-image-arm-qemu-arm-virt
2023-04-13T01:46:27.7980266Z �[33m+++ tar czf ../vm_minimal_sim-images.tar.gz images/�[0m
2023-04-13T01:46:29.0389620Z �[33m+++ bash -c expect -c 'spawn ./simulate; set timeout 3000; expect "buildroot login:"'�[0m
2023-04-13T01:46:29.0516106Z spawn ./simulate
2023-04-13T01:46:29.1339565Z ./simulate: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic  -m size=2048  -kernel images/capdl-loader-image-arm-qemu-arm-virt
2023-04-13T01:46:29.1343762Z 
2023-04-13T01:46:29.1346682Z ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
...
2023-04-13T01:46:30.6131863Z FAULT HANDLER: data fault from vm0.vm0_0_control (ID 0x2) on address 0x90, pc = 0x464014, fsr = 0x93800006
...
2023-04-13T01:46:30.6302854Z FAULT HANDLER:     +-- 0x0000000000400000 --
2023-04-13T01:46:30.6302985Z
...
...  now we are stuck for 50 min ...
...
2023-04-13T02:36:29.6319786Z �[1m-----------[ end test vm_minimal_sim ]-----------�[0m
2023-04-13T02:36:29.6320403Z ##[endgroup]
2023-04-13T02:36:29.6320682Z �[32mvm_minimal_sim succeeded�[0m
2023-04-13T02:36:29.6320829Z 
2023-04-13T02:36:29.6321087Z ##[group]vm_minimal_smp_tx1
...
2023-04-13T02:37:25.9190959Z Cleaning up orphan processes

simulating q35 machine in qemu software with network interface card.

Hi. I'm working on a new camkes-based project.
This project is simulated by using Qemu, on Q35 machine for X86_64 arch and e1000e eth. I am using intel controller driver (82574 controller) for network communication. my project has built successfully.

When Ethernet interface will be initialized using ethif_e82574_init() function, something happens like device initialization, disabling interrupts, transmit initialization, receive initialization, checking link status and etc.
in device initialization, when I reset hardware, phy_read() will be trapped.
in other word, in this line

while(REG_MDIC() & BIT(28))

BIT(28) is ready bit in MDIC register.

Qemu command:

sudo qemu-system-x86_64 -machine q35,accel=kvm,kernel-irqchip=split -cpu host,+vme,+pdpe1gb,xsave,xsaveopt,-xsavec,fsgsbase,invpcid,enforce,+vmx -netdev tap,id=netdev0,ifname=tap0,script=no,downscript=no -device virtio-net,id=nic0,netdev=netdev0,mac=52:55:00:d1:55:01,disable-modern=on,disable-legacy=off -device e1000e -nographic  -serial mon:stdio -m size=4G  -device intel-iommu  -kernel ./target/debug/images/kernel-x86_64-pc99  -initrd ./target/debug/images/capdl-loader-image-x86_64-pc99

how to fix this problem?
thank you.

	#define VM_GENERAL_CONFIGURATION_DEF() \
	fserv.heap_size = 165536; \