A collection of libraries for seL4. These libraries are compatible with seL4_libs.
Contributions welcome!
See the CONTRIBUTING file for more.
License: Other
A collection of libraries for seL4. These libraries are compatible with seL4_libs.
Contributions welcome!
See the CONTRIBUTING file for more.
This is a breaking change but is probably worthwhile to consider:
Removing the vspace_t dependency from libsel4vm and libsel4vmmplatsupport
and interacting with the vspace objects directly mostly resolves a series of issues
and don't really introduce any significant new problems for guests or a client vmm
other than needing to update vmm drivers that expect to use the vspace objects.
It also provides a reasonably small stepping stone for eventually removing more of
sel4_libs as discussed recently (https://sel4.discourse.group/t/sel4-virtualization-support-current-efforts/665/3)
vspace_t is an abstraction that wraps seL4 vspace objects and provides
the following functionality:
Unfortunately there are the following issues:
The VMM only really needs features 1, 2 and 9, and it already implements
its own version of region reservations (2) separately. There's also some
helper functions in libsel4utils that implement just 1. and depend on a
vka_t interface that the VMM also already has a copy of.
As for 6. the vmm does need a more efficient copyin/copyout mechanism
that would be somewhat system specific and shouldn't create new mappings
on each access.
I was working around with the default vm_minimal
for qemu-arm-virt
64bits platform and tried to allocate 2GB RAM for the VM linux and got some allocation fail error.
./simulate: QEMU command: qemu-system-aarch64 -machine virt,virtualization=on,highmem=off,secure=off -cpu cortex-a53 -nographic -m size=4096 -kernel images/capdl-loader-image-arm-qemu-arm-virt
ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
paddr=[c1b39000..c2fa90d7]
No DTB passed in from boot loader.
Looking for DTB in CPIO archive...found at c1c94cc8.
Loaded DTB from c1c94cc8.
paddr=[c0242000..c0243fff]
ELF-loading image 'kernel' to c0000000
paddr=[c0000000..c0241fff]
vaddr=[80c0000000..80c0241fff]
virt_entry=80c0000000
ELF-loading image 'capdl-loader' to c0244000
paddr=[c0244000..c173cfff]
vaddr=[400000..18f8fff]
virt_entry=408d88
Enabling hypervisor MMU and paging
Jumping to kernel-image entry point...
Bootstrapping kernel
Warning: Could not infer GIC interrupt target ID, assuming 0.
available phys memory regions: 1
[c0000000..140000000]
reserved virt address space regions: 3
[80c0000000..80c0242000]
[80c0242000..80c0243ddc]
[80c0244000..80c173d000]
Booting all finished, dropped to user space
<<seL4(CPU 0) [decodeUntypedInvocation/205 T0x813f813400 "rootserver" @4006f8]: Untyped Retype: Insufficient memory (1 * 2097152 bytes needed, 0 bytes available).>>
[email protected]:1332 Invalid 'num_vcpus' attribute setting: Exceeds maximum number of supported nodes. Capping value to CONFIG_MAX_NUM_NODES (1)
[email protected]:704 module name: map_frame_hack
[email protected]:704 module name: init_ram
ram_ut_alloc_iterator@guest_ram.c:304 Failed to allocate page
map_vm_memory_reservation@guest_memory.c:477 Failed to get frame for reservation address 0x8e83a000
Loading Kernel: 'linux'
Loading Initrd: 'linux-initrd'
Loading Generated DTB
vm_ram_touch@guest_ram.c:165 Failed to touch ram region: Not registered RAM region
32 bit ARM insts not decoded
--------
Pagefault from [vm0]: write fault @ PC: 0xffff0000083bd92c IPA: 0xbffff000, FSR: 0x92000046
Context:
x0: 0xffff7dfffe63b000
x1: 0x0
x2: 0xfc0
x3: 0x4
x4: 0x0
x5: 0x40
x6: 0x3f
x7: 0x0
x8: 0xffff7dfffe63b000
x9: 0x0
x10: 0x40000000
x11: 0x0
x12: 0x3
pc: 0xffff0000083bd92c
x14: 0x0
sp: 0xffff000008e00000
spsr: 0x40000085
x13: 0xffff000008f7b530
x15: 0x18
x16: 0x1800
x17: 0x8b0
x18: 0xffffffffffffffff
x19: 0xbffff000
x20: 0xffff000008e08000
x21: 0xffff000008e4b308
x22: 0xffff7dfffe800000
x23: 0xffff000008e08000
x24: 0x0
x25: 0x0
x26: 0x0
x27: 0x0
x28: 0x40a50018
x29: 0xffff000008e03e60
x30: 0xffff000008a56160
m--------
Assertion failed: rt >= 0 (/host/projects/seL4_projects_libs/libsel4vm/src/arch/arm/fault.c: fault_get_width: 620)
I found that it was caused by that the static memory pool of allocman
was consumed up. Then I mentioned that the static memory pool was predefined default to 80MB size. (https://github.com/seL4/camkes-vm/blob/master/templates/seL4AllocatorMempool.template.c#L9)
I tried to add it to 140MB and VM Linux was boot successed. But 140MB / 2GB is an unexpected proportion to me.
Then I dived into the details of the related codes and found the default allocator for untyped
frames is Buddy
like and the RAM allocation is at a 4K granularity.
https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/src/utspace/split.c
seL4_projects_libs/libsel4vm/src/guest_ram.c
Line 292 in 9736082
With this, a 2GB RAM region will need (2GB / 4KB) * 2 * (sizeof(node) + overload) = 120MB memory.
Here we may switch to use seL4_LargePage
in VM RAM register, and the allocation granularity is 2M, and reduce the memory overhead to 120MB / 512 size.
I wonder, in
seL4_projects_libs/libsel4vm/src/arch/arm/vm.c
Lines 234 to 241 in 9de0630
vm->run.exit_reason = VM_GUEST_ERROR_EXIT;
if vcpu_idx
is invalid?
Hi,
I think I may have found a bug in vmm_pci_helper_map_bars
from libsel4vmmplatsupport/src/arch/x86/drivers/vmm_pci_helpers.c
.
The PCI interface standard mandates that BAR addresses be naturally aligned, i.e. the address must be a multiple of the size. This is a requirement for the weird BAR size probing logic (save value, write 0xffffffff, read back size mask, restore value) to function properly. The vmm_pci_helper_map_bars
function however calls vm_reserve_anon_memory
to reserve memory in the guest space and this function does not (necessarily) returns naturally aligned addresses.
I ran into this using qemu
. Simple CAmkES setup with a single Linux VM, with PCI pass-throughs for both a virtio-net
and a e1000
network interfaces. At boot, the PCI bus is correctly scanned as such:
lib_pci_scan_dev found pci device 0 0
PCI :: 00.00.00 : intel Unknown device ID. (vid 0x8086 did 0x29c0) line0 pin0
lib_pci_scan_dev found pci device 0 1
PCI :: 00.01.00 : Unknown vendor ID. Unknown device ID. (vid 0x1234 did 0x1111) line0 pin0
BAR0 : [ mem 0xfd000000 sz 0x1000000 szmask 0xff000000 prefetch ]
BAR2 : [ mem 0xfebf0000 sz 0x1000 szmask 0xfffff000 ]
lib_pci_scan_dev found pci device 0 2
PCI :: 00.02.00 : Unknown vendor ID. Unknown device ID. (vid 0x1af4 did 0x1000) line11 pin1
BAR0 : [ io 0xc080 sz 0x20 szmask 0xffffffe0 ]
BAR1 : [ mem 0xfebf1000 sz 0x1000 szmask 0xfffff000 ]
BAR4 : [ mem 0xfe000000 sz 0x4000 szmask 0xffffc000 64bit prefetch ] /* size: 0x4000 */
lib_pci_scan_dev found pci device 0 3
PCI :: 00.03.00 : intel Unknown device ID. (vid 0x8086 did 0x100e) line11 pin1
BAR0 : [ mem 0xfebc0000 sz 0x20000 szmask 0xfffe0000 ] /* size: 0x20000 */
BAR1 : [ io 0xc000 sz 0x40 szmask 0xffffffc0 ]
lib_pci_scan_dev found pci device 0 31
PCI :: 00.1f.00 : intel intel_ich9_8 (vid 0x8086 did 0x2918) line0 pin0
lib_pci_scan_dev found multi function device 0 31
PCI :: 00.1f.02 : intel Unknown device ID. (vid 0x8086 did 0x2922) line10 pin1
BAR4 : [ io 0xc0a0 sz 0x20 szmask 0xffffffe0 ]
BAR5 : [ mem 0xfebf2000 sz 0x1000 szmask 0xfffff000 ]
PCI :: 00.1f.03 : intel intel_ich9_6 (vid 0x8086 did 0x2930) line10 pin1
BAR4 : [ io 0x700 sz 0x40 szmask 0xffffffc0 ]
The issue shows up with BAR4 of PCI device 00.02.00 (virtio-net) as well as BAR0 of PCI device 00.03.00 which have sizes larger than one page. Here's what the guest Linux kernel finds:
[ 0.190000] pci 0000:00:00.0: [5e14:0042] type 00 class 0x060000
[ 0.190000] pci 0000:00:01.0: [1af4:1000] type 00 class 0x020000
[ 0.200000] pci 0000:00:01.0: reg 0x10: [io 0xc080-0xc09f]
[ 0.210000] pci 0000:00:01.0: reg 0x14: [mem 0x18001000-0x18001fff]
[ 0.210000] pci 0000:00:01.0: reg 0x18: [mem 0x18002000-0x18003fff pref] /* size: 0x2000 ! */
[ 0.220000] pci 0000:00:02.0: [8086:100e] type 00 class 0x020000
[ 0.230000] pci 0000:00:02.0: reg 0x10: [mem 0x18006000-0x18007fff] /* size: 0x2000 ! */
[ 0.230000] pci 0000:00:02.0: reg 0x14: [io 0xc000-0xc03f]
The address 0x18002000 is not legal to store a BAR of size 0x4000 (0x18002000 & (0x4000 - 1) != 0). Likewise address 0x18006000 is not legal to store a BAR of size 0x20000 (0x18006000 & (0x20000 - 1) != 0).
truct gic_dist_map {
uint32_t enable; /* 0x000 /
uint32_t ic_type; / 0x004 /
uint32_t dist_ident; / 0x008 */
uint32_t res1[29]; /* [0x00C, 0x080) */
uint32_t irq_group0[CONFIG_MAX_NUM_NODES]; /* [0x080, 0x84) */
uint32_t irq_group[31]; /* [0x084, 0x100) */
uint32_t enable_set0[CONFIG_MAX_NUM_NODES]; /* [0x100, 0x104) */
uint32_t enable_set[31];
irq_group0, enable_set0 is not mean work muti core, this will not work OK
for examp:
For interrupt ID m, when DIV and MOD are the integer division and modulo operations:
the corresponding GICD_ISENABLER number, n, is given by n = m DIV 32
the offset of the required GICD_ISENABLER is (0x100 + (4*n))
the bit number of the required Set-enable bit in this register is m MOD 32.
delete branch xu4_vmm_wip
, this has been merged already
It is not clear how this repository compares with seL4_libs. I know that seL4_libs is (or at least was) not considered to be of production quality, for example.
There are a lot of branches that look as if the work has been merged. Could you remove them here?
missing-lincenses
spdx
spdx-syntax
alyons-ppi
kent/fix-style
kent/rockpro64
kent/remove-warning
nomadeel/fdt-fix
Follow-up from commit 0f9286d of #16 for libsel4vm/src/arch/x86/guest_x86_context.c
:
/* Under release mode, this file will get built using -O3. Howerver on gcc 8.4,
* the -O3 optimisation level is too aggressive and causes issues for the guest
* VM. Hence, instead of using -O3 we use -O2 to avoid the issue. */
In vgic_dist_set_pending_irq()
we enque an interrupt and then dequeue one
seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vgic.c
Lines 581 to 602 in 9de0630
Since there is no guarantee that we dequeue the same interrupt we have enqueued, I wonder if this should dequeue in a loop while there are interrupts in the queue and there are list registers available?
8-bit and 16-bit read and write faults do not seem to be handled correctly. For example, if a VM performs a 8-bit read and the fault is set to return 0, it will instead return a 32-bit value with garbage in the upper 24-bits and 0x00 in the lower 8-bits.
The function fault_get_data_mask()
only produce the mask within 32 bits which meas it can't return a mask like 0xffffffff00000000
with 64 bits seL4_Word
.
GICD_IROUTER
of gicv3 which is in 64 bits width, the mask and the related fault function fault_emulate()
can't handler the access to the upper 32 bits correctly.github CI job 'trigger' should not run on forks, as this fails when updating master there:
Run seL[4](https://github.com/axel-h/seL4_projects_libs/runs/5490887825?check_suite_focus=true#step:2:4)/ci-actions/trigger@master
/home/runner/work/_actions/seL4/ci-actions/master/js/../trigger/steps.sh
Need $INPUT_TOKEN for authentication.
Error: Action trigger failed.
When vgic_dist_set_pending_irq()
called from a write to pending_bits
in emulated GIC distributor, the vcpu
here to enqueue the vIRQ is the vcpu
that performed the write operation.
seL4_projects_libs/libsel4vm/src/arch/arm/vgic/vdist.h
Lines 222 to 229 in eb42051
pending_bits
only moves the IRQ to the pending state, and the target vcpu
of the IRQ is still specified by it's target_bits
, which may not be the vcpu
that the vIRQ was inserted into as the above code shows.
That' mean when an IRQ is set to route to the vcpu_0
, a write to the pending_bit
of the IRQ from vcpu_1
inserts the IRQ into vcpu_1
rather than vcpu_0
.
libvchan.h
includes <linux/types.h>
which causes it to fail to compile in my environment. It seems like this include is only used to get size_t
so it can be replaced by <stddef.h>
instead.
Follow-up from https://lists.sel4.systems/hyperkitty/list/[email protected]/thread/YNTMEMTAUD5ZE6X7J4O4E75OELA6T345/
The error
Unhandled offset of 0x14 of size 1, writing 0x2
Assertion failed: !"panic"
seL4_projects_libs/seL4_projects_libs/libsel4vmmplatsupport/src/drivers/virtio_emul.c: emul_io_out: 109
Seem to indicate that the virtio_net driver of the libsel4vmmsupport does not support IO control for changing the MAC addess of the virtio net in the guest.
(Moved from: https://sel4.atlassian.net/browse/SELFOUR-793)
Currently libsel4arm-vmm provides basic support for decoding and emulating faults for the TK1. This works by relying on the HSR register providing a valid instruction syndrome.
From the armv7 manual:
"A valid instruction syndrome provides information that can help a hypervisor to emulate the
instruction efficiently. Instruction syndromes are returned for instructions for which such
accelerated emulation is possible."
The syndrome contains what register is used for the read/write, what the width of the data is, whether it needs to be sign extended. This makes the fault easy to decode and emulate which libsel4arm-vmm currently does.
However a valid syndrome only occurs for a subset of arm data instructions. For instructions outside of this the instruction needs to be decoded and properly emulated (such as handling register write back where the second register that holds the address of the lookup is updated with the immediate offset such as pop and push instructions). Currently this is not supported.
This only becomes a problem when the vmm wants to trap and emulate faults. Memory protection faults that result in needing to map a page into the mmu doesn't require decoding any instructions because the fault address is stored in a different register and the fault is normally handled by mapping in a page and then restarting the faulting instruction rather than advancing the fault instruction which requires the instruction to be emulated.
We currently use trap and emulation for providing more granular memory access control than the frame level. Up until now this lack of support hasn't been an issue but could become an issue in the future.
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.