Greetings,
I'm trying to understand how hypervisor functionality support is
working in seL4 for aarch32/aarch64. In the documentation there is a
list of platforms [1] for some of them ARM_HYP is said to be supported
for some not. I was trying to grep through the kernel, but it seemed
to me that ARM_HYP can be enabled on any ARM-based platform.
I've tried to compile sel4test for exynos5422 (for which ARM_HYP is
said to be enabled) and odroidc2 (for which it is said that it's not
supported) with -DARM_HYP=ON manually set, and for both compilation
succeeded. It failed for hikey, that should support it, but that's a
different story.
So my questions are
- How is it defined whether ARM_HYP is supported for a board/SoC,
provided that processor architecture supports it? What the platform
support code should provide for hypervisor to work?
- For platforms not supported by camkes-arm-vm (like, most of the
platforms) how ARM_HYP can be tested?
Thanks a lot,
Anton Gerasimov
[1] https://docs.sel4.systems/Hardware/
hello
can someone help me here what did i do wrong ,i have been trying to do
camkes-vm-linux and i have followed the instruction on sel4-tutorials when
i run ninja to build the file i have got an error as below
==========================================================================
ninja
[5/127] Building C object
camkes-vm-li...ents/Init/src/virtio_net_vswitch.c.obj
FAILED: ccache /usr/bin/gcc
--sysroot=/home/sel4/sel4-tutorials-manifest/camkes-vm-linux_build
-I../projects/camkes/vm/components/Init/src
-I../projects/camkes/vm/components/VM/configurations
-Icamkes-vm-linux/vm0/include -I../kernel/libsel4/include
-I../kernel/libsel4/arch_include/x86
-I../kernel/libsel4/sel4_arch_include/x86_64
-I../kernel/libsel4/sel4_plat_include/pc99
-I../kernel/libsel4/mode_include/64 -Ilibsel4/include
-Ilibsel4/arch_include/x86 -Ilibsel4/sel4_arch_include/x86_64
-I../projects/sel4runtime/include -I../projects/sel4runtime/include/mode/64
-I../projects/sel4runtime/include/arch/x86
-I../projects/sel4runtime/include/sel4_arch/x86_64
-Iprojects/musllibc/build-temp/stage/include -Ilibsel4/autoconf
-Ikernel/gen_config -Ilibsel4/gen_config
-I../tools/camkes/libsel4camkes/include
-I../projects/seL4_libs/libsel4debug/include
-I../projects/seL4_libs/libsel4debug/arch_include/x86
-I../projects/seL4_libs/libsel4debug/sel4_arch_include/x86_64
-I../projects/util_libs/libutils/include
-I../projects/util_libs/libutils/arch_include/x86
-Iprojects/util_libs/libutils/gen_config
-I../projects/util_libs/libplatsupport/include
-I../projects/util_libs/libplatsupport/plat_include/pc99
-I../projects/util_libs/libplatsupport/arch_include/x86
-Iprojects/util_libs/libplatsupport/gen_config
-I../projects/seL4_libs/libsel4muslcsys/include
-I../projects/util_libs/libcpio/include
-I../projects/seL4_libs/libsel4utils/include
-I../projects/seL4_libs/libsel4utils/sel4_arch_include/x86_64
-I../projects/seL4_libs/libsel4utils/arch_include/x86
-I../projects/seL4_libs/libsel4vspace/include
-I../projects/seL4_libs/libsel4vspace/arch_include/x86
-I../projects/seL4_libs/libsel4vka/include
-I../projects/seL4_libs/libsel4vka/sel4_arch_include/x86_64
-I../projects/seL4_libs/libsel4vka/arch_include/x86
-Iprojects/seL4_libs/libsel4vka/gen_config
-Iprojects/seL4_libs/libsel4utils/gen_config
-I../projects/seL4_libs/libsel4simple/include
-I../projects/seL4_libs/libsel4simple/arch_include/x86
-I../projects/seL4_libs/libsel4platsupport/include
-I../projects/seL4_libs/libsel4platsupport/arch_include/x86
-I../projects/seL4_libs/libsel4platsupport/plat_include/pc99
-I../projects/seL4_libs/libsel4simple-default/include
-I../projects/util_libs/libelf/include
-Iprojects/seL4_libs/libsel4muslcsys/gen_config
-I../projects/seL4_libs/libsel4sync/include
-I../projects/projects_libs/libvirtqueue/include
-Icamkes-vm-linux/libsel4camkes/gen_config
-Iprojects/sel4runtime/gen_config
-I../projects/seL4_libs/libsel4allocman/include
-I../projects/seL4_libs/libsel4allocman/sel4_arch/x86_64
-I../projects/seL4_libs/libsel4allocman/arch/x86
-I../projects/seL4_libs/libsel4vmm/include
-I../projects/util_libs/libpci/include
-I../projects/util_libs/libethdrivers/include
-I../projects/util_libs/libethdrivers/plat_include/pc99
-I../projects/util_libs/libethdrivers/arch_include/x86
-Iprojects/util_libs/libethdrivers/gen_config
-Iprojects/util_libs/liblwip/gen_config
-Iprojects/util_libs/libpicotcp/gen_config
-Iprojects/seL4_libs/libsel4vmm/gen_config -Icamkes-vm-linux/vm/gen_config
-I../projects/projects_libs/libvswitch/include
-I../projects/camkes/global-components/components/FileServer/libFileServer-client/.
-m64 -march=nehalem -D__KERNEL_64__ -g -nostdinc -fno-pic -fno-pie
-fno-stack-protector -fno-asynchronous-unwind-tables -ftls-model=local-exec
-mtls-direct-seg-refs -Wno-main -std=gnu11 -MD -MT
camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj
-MF
camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj.d
-o
camkes-vm-linux/CMakeFiles/vm0.instance.bin.dir/__/projects/camkes/vm/components/Init/src/virtio_net_vswitch.c.obj
-c ../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function
‘virtio_net_notify_vswitch_send’:
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:50:23:
warning: implicit declaration of function ‘virtqueue_driver_dequeue’
[-Wimplicit-function-declaration]
int dequeue_res = virtqueue_driver_dequeue(node->virtqueues.send_queue,
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function
‘emul_raw_tx’:
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:123:13:
error: unknown type name ‘virtqueue_t’
virtqueue_t *destbuff;
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:147:19:
warning: implicit declaration of function ‘virtqueue_driver_enqueue’
[-Wimplicit-function-declaration]
err = virtqueue_driver_enqueue(destnode->virtqueues.send_queue,
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:157:19:
warning: implicit declaration of function ‘virtqueue_driver_signal’
[-Wimplicit-function-declaration]
err = virtqueue_driver_signal(destnode->virtqueues.send_queue);
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:170:17:
warning: implicit declaration of function ‘virtqueue_driver_poll’
[-Wimplicit-function-declaration]
if (virtqueue_driver_poll(destnode->virtqueues.send_queue) ==
1) {
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function
‘virtio_net_notify_vswitch_recv’:
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:215:5:
error: unknown type name ‘virtqueue_t’
virtqueue_t *rxdata_buff;
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:234:23:
warning: implicit declaration of function ‘virtqueue_device_dequeue’
[-Wimplicit-function-declaration]
int dequeue_res = virtqueue_device_dequeue(node->virtqueues.recv_queue,
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:249:27:
warning: implicit declaration of function ‘virtqueue_device_enqueue’
[-Wimplicit-function-declaration]
enqueue_res =
virtqueue_device_enqueue(node->virtqueues.recv_queue, available_buff,
available_buff_sz);
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:275:11:
warning: implicit declaration of function ‘virtqueue_device_signal’
[-Wimplicit-function-declaration]
err = virtqueue_device_signal(node->virtqueues.recv_queue);
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function
‘virtio_net_notify_vswitch’:
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:292:17:
warning: implicit declaration of function ‘virtqueue_device_poll’
[-Wimplicit-function-declaration]
if
(virtqueue_device_poll(g_vswitch.nodes[i].virtqueues.recv_queue) == 1) {
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c: In function
‘make_vswitch_net’:
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:312:44:
warning: passing argument 1 of ‘camkes_virtqueue_driver_init’ from
incompatible pointer type [-Wincompatible-pointer-types]
err = camkes_virtqueue_driver_init(&send_virtqueue,
mac_mapping.send_id);
^
In file included from
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:29:0:
../tools/camkes/libsel4camkes/include/camkes/virtqueue.h:64:5: note:
expected ‘virtqueue_driver_t * {aka struct virtqueue_driver *}’ but
argument is of type ‘virtqueue_driver_t ** {aka struct virtqueue_driver **}’
int camkes_virtqueue_driver_init(virtqueue_driver_t *driver, unsigned int
camkes_virtqueue_id);
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:317:44:
warning: passing argument 1 of ‘camkes_virtqueue_device_init’ from
incompatible pointer type [-Wincompatible-pointer-types]
err = camkes_virtqueue_device_init(&recv_virtqueue,
mac_mapping.recv_id);
^
In file included from
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:29:0:
../tools/camkes/libsel4camkes/include/camkes/virtqueue.h:72:5: note:
expected ‘virtqueue_device_t * {aka struct virtqueue_device *}’ but
argument is of type ‘virtqueue_device_t ** {aka struct virtqueue_device **}’
int camkes_virtqueue_device_init(virtqueue_device_t *device, unsigned int
camkes_virtqueue_id);
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:320:13:
warning: implicit declaration of function ‘camkes_virtqueue_driver_free’
[-Wimplicit-function-declaration]
camkes_virtqueue_driver_free(send_virtqueue);
^
../projects/camkes/vm/components/Init/src/virtio_net_vswitch.c:333:13:
warning: implicit declaration of function ‘camkes_virtqueue_device_free’
[-Wimplicit-function-declaration]
camkes_virtqueue_device_free(recv_virtqueue);
^
[5/127] Building C object
camkes-vm-li...MakeFiles/sel4camkes.dir/src/dma.c.obj
ninja: build stopped: subcommand failed.
==================================================================
and why this happing
I'm using the docker image to build the CAmkES ARM VMM project using
roughly the instructions here:
https://docs.sel4.systems/VM/CAmkESARMVM.html (they are slightly out of
date).
I do:
../init-build.sh -DAARCH32=TRUE -DCAMKES_VM_APP=vm_minimal -DPLATFORM=tk1
ninja
Then I copy the resulting image from the images directory to an SD card and
put that in my TK1.
When U-Boot starts I use the following commands to try to boot
fatload mmc 1 0x10000000 capdl-loader-image-arm-tk1
bootelf 0x10000000
To which I get an error: No elf image at address 0x10000000
I tried with an older version of U-Boot (that worked following this same
procedure about a year ago). It is U-Boot SPL 2014.10-rc2-g3127911 (Jun 07
2016 - 21:00:01)
I also tried updating U-Boot to U-Boot SPL 2020.01-00442-gc00bd81ae0 (Jan
10 2020 - 11:10:18 -0500). Same error.
Any thoughts or suggestions on how I get this to boot?
Hello all,
I am working with sabre lite board and using camkes framework.
In my implementation I have a driver component that has 7 dataport buf and
I connected these buffers to hardware component.
In source of component driver I am initialize gpio_sys, mux_sys and pins
using these functions:
- imx6_mux_init()
- imx6_gpio_sys_init()
- gpio_new()
Here I have copied some part of my code:
******************************************
gpio_sys_t gpio_sys;
gpio_t pins[32*7];
mux_sys_t mux_sys;
void gpio__init()
{
imx6_mux_init(NULL, &mux_sys);
imx6_gpio_sys_init((void*)gpio0, (void*)gpio1, (void*)gpio2, (void*)gpio3,
(void*)gpio4, (void*)gpio5, (void*)gpio6, &mux_sys, &gpio_sys);
}
void gpio_init_pin(int pin, int direction)
{
if(pin>0 && pin< sizeof(pins)/sizeof(pins[0]))
{
gpio_new(&gpio_sys, pin, (enum gpio_dir)direction, &pins[pin]);
}
}
void gpio_set_pin(int pin, int value)
{
if(pin >= 0 && pin < (sizeof(pins)/sizeof(pins[0])))
{
if(value)
{
gpio_set(&pins[pin]);
}
else
{
gpio_clr(&pins[pin]);
}
}
}
int gpio_read_pin(int pin)
{
if(pin>0 && pin< sizeof(pins)/sizeof(pins[0]))
{
return gpio_get(&pins[pin]);
}
return -1;
}
******************************************
By calling "gpio_init_pin(ALARM_PIN= 28, 0);" I am getting this error:
Assertion failed: bank->data == v
(PATH/projects/util_libs/libplatsupport/src/plat/imx6/gpio.c:
imx6_gpio_write: 144)
How can I fix this error? How should I specify the GPIO pins?
Thank you for your time and consideration,
Parvaneh.
hi everybody
i have quick questions regarding how can you take an input form terminal in
seL4,i am trying to run a simple code of my own on sel4 and to display a
message we use printf(), why scanf() is not working for me the way printf
work.is there another way to do that
I have a bit of a noobish question, why are timing/scheduling abilities
being added to the kernel? I understand that userland still controls
scheduling, regardless of which branch is being used, but I'm confused as
to wby scheduling features needed to be added to the kernel itself.
Hi everyone,
I have a couple questions regarding the current CMake build structure for
CAmkES projects. It seems that the current structure intends you to put
your project in the camkes/apps folder, and then build your project with
`../init-build -DCAMKES_APP=<project_name>`, or the equivalent using the
griddle script. What I don't understand is how you are supposed to
configure your project. It seems easy_settings.cmake is always loaded. Is
it advisable to edit this file?
In the past, I could also tweak configuration variables manually by
invoking the ccmake gui on the top-level directory. Now that there is no
CMakeLists.txt in the top-level directory, this does not work. If I try it
in my project's directory, it tells me the cache is empty. Is it still
possible to edit CMake cache variables with ccmake?
Thanks!
Grant Jurgensen
Hi,
I have a design question regarding how to recycle capabilities/memory frames that were used by a thread once it terminates.
Let's assume that there is a MemoryManager server responsible to serve virtual memory to user processes (e.g similar to implementing VirtualAlloc).
The MemoryManager has to maintain the list of untyped object, retype them, maintain likely a list of resources allocated for a user thread, likely copy/mint the page frames to forward them to the user process...etc.
But when a thread terminates, as I can't see any related events in seL4, I would assume that the user process would have to explicitly notify the MemoryManager on exit.
Then the MemoryManager would know which user thread has exited and would update/recover the used capabilities and destroy them, in order to recover untyped objects.
Would it be a proper design that plays well with seL4? Do you think that it could be done more efficiently with seL4?
Thank you!
