Hello, I'm new to seL4 and I'm just doing it for learning purpose. I'm
trying to run seL4 test suite or simple hello world task from seL4
tutorials on the real hardware. So far I had no problems compiling seL4
test suite and running via QEMU for both x32 and x64 platforms. However,
when I try to run it on the actual hardware following Running on real
hardware tutorial for x86 I end up with no output at all and no error msgs
that can give me a clue on where something went wrong.
After compiling …
[View More]seL4test for x86, I ended up with two images in
sel4_dir/images/ folder. Copied them over to /boot/sel4/ folder and created
a new GRUB2 entry that looks like this
menuentry “seL4 test suite” --class os {
load video
insmod gzio
insmod part_msdos
insmod ext2
set root=’(hd0,msdos5)’
multiboot /boot/sel4/kernel-ia32-pc99
module /boot/sel4/sel4test-driver-image-ia32-pc99
}
update grub, restart and select the new entry from GRUB menu.
I end up with blinking cursor on the top-left side of the screen. Please
advise.
[View Less]
Hi seL4 Dev team,
Can someone explain the reason (share the reference) to invalidate the
local TLB during kernel vspace activation as part CPU initialisation.
The Tx2 board stuck while performing this operation. As per my
understanding both Tx1 and Tx2 are using same A57 core. so the TLB
initialisation and invalidation remain same for Tx2 and should not stuck
during invalidation.Please correct me if anything wrong here.
I understand from that instruction (tlbi vmalle1) which is invalidating
…
[View More]stage 1 entries associated to the current VMID. Also from arm mmu code the
seL4 setting up (TCR_EL1) TCR register addressing space as 48bit, ASID as
16bit and page table setup 4k granular size.
I am using MRS macro to dump the spsr_el1 and dspsr_el0 register to see the
state of processor but its throwing synchronous exception. Do we have any
other option to dump all the register content to see the state of processor
like we have one in 'sel4debug_dump_registers' which is used in sel4test
code.
Regards,
Muneeswaran R
[View Less]
Hi all,
Sorry to bother, I have some basic questions about seL4 memory management. Can someone help me?
1. where is the kernel’s address space?
I know there are basically three methods:
a) separate virtual address space, e.g. through changing page tables on entry into privileged mode to access
b) physical space, e.g. through disable automatic hardware translation of virtual addresses on entry into privilege mode
c) privilege region in each process’s virtual address space, e.g. through …
[View More]page table to map kernel address into use-mode process.
My question is which of this is being used by seL4 microkernel?
2. Objects like CSpace, VSpace, CNode, TCB, Endpoint, etc. are called kernel objects, but it seems all dynamically allocated in thread running/creating time. Are those objects (e.g. Figure 3.3 in seL4 manual) in kernel space or in user space?
3. I read that after the kernel boot up, it passes all resources, untyped memory to the first thread. Are those untyped memory physical memory or virtual memory in a single page?
The reason I ask is I’m learning the code of the UNSW AOS project (two of the assignment projects are implementing frame and papers). I’m confused that before the implementation of frames and pages what kind of memory is passed to the the first thread? I saw int AOS project, it uses ut_table_init(), ut_steal_mem(), I wonder what kind of memory it operates on?
Thanks
-Dan
[View Less]
Dear sel4 community,
yesterday I've started to develop a low-level platform test to stress several
multi-processor aspects on top of the Genode API. Thereby, I've
recognized that on sel4/x86_64 the TLB is practically not always
cleaned properly in SMP systems.
The test spawns threads of one protection domain on each available cpu.
Each thread accesses one of the first words of a shared dataspace.
Afterwards the main thread on CPU 0 detaches and destroys the
dataspace. Unfortunately, the …
[View More]threads on other CPUs still successfully
access the corresponding memory instead of triggering a fault.
To be able to reproduce the problem, you might investigate the simple
test case here:
https://github.com/skalk/genode/commit/2d2d7f982555f551227ad5dcbf9df46705d7…
My colleague Alexander Boettcher already investigated the problem in
part, and might share his insights with you.
Best regards
Stefan
--
Stefan Kalkowski
Genode labs
https://github.com.skalk | https://genode.org
[View Less]
Hello
I have a linking problem in the picoserver CAmkES-application which was added 2 days ago.
Steps I did:
1) repo init -u https://github.com/seL4/camkes-manifest.git
2) repo sync
3) start docker container
4) (in new subfolder) ../init-build.sh -DPLATFORM=x86_64 -DSIMULATION=1 -DCAMKES_APP=picoserver
(side note: aborts because picotcp folder is missing in projects folder, but that's easy fixed)
5) ninja
Error:
[5/16] Linking C executable projects/camkes/ethdriver.instance.bin
FAILED: …
[View More]projects/camkes/ethdriver.instance.bin
: && ccache /usr/bin/gcc --sysroot=/host/test -m64 -march=nehalem -D__KERNEL_64__ -g -march=nehalem -D__KERNEL_64__ -Wl,-m -Wl,elf_x86_64 -static -nostdlib -z max-page-size=0x1000 -static -nostdlib -u _camkes_start -e _camkes_start -Wl,--script=/host/test/projects/camkes/ethdriver/linker.lds /host/test/lib/crt1.o /host/test/lib/crti.o /usr/lib/gcc/x86_64-linux-gnu/6/crtbegin.o projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/ethdriver.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/82574.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.simple.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/camkes.environment.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/EthDriver_seL4HardwareMMIO_0.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/irq_seL4HardwareInterrupt_0.c.obj projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/ethdriver/client_seL4Ethdriver_0.c.obj -lgcc -lgcc_eh libsel4/libsel4.a projects/camkes-tool/libsel4camkes/libsel4camkes.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/util_libs/libutils/libutils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libethdrivers/libethdrivers.a projects/projects_libs/libvirtqueue/libvirtqueue.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4debug/libsel4debug.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4vka/libsel4vka.a libsel4/libsel4.a projects/util_libs/libplatsupport/libplatsupport.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a projects/util_libs/libpicotcp/picotcp_external/picotcp/build//lib/libpicotcp.a -lgcc -lgcc_eh libsel4/libsel4.a projects/camkes-tool/libsel4camkes/libsel4camkes.a projects/seL4_libs/libsel4sync/libsel4sync.a projects/util_libs/libutils/libutils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libplatsupport/libplatsupport.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4muslcsys/libsel4muslcsys.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4vka/libsel4vka.a projects/seL4_libs/libsel4allocman/libsel4allocman.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/util_libs/libethdrivers/libethdrivers.a projects/projects_libs/libvirtqueue/libvirtqueue.a projects/seL4_libs/libsel4utils/libsel4utils.a projects/seL4_libs/libsel4platsupport/libsel4platsupport.a projects/seL4_libs/libsel4simple-default/libsel4simple-default.a projects/seL4_libs/libsel4debug/libsel4debug.a projects/seL4_libs/libsel4simple/libsel4simple.a projects/util_libs/libelf/libelf.a projects/util_libs/libcpio/libcpio.a projects/seL4_libs/libsel4vspace/libsel4vspace.a projects/seL4_libs/libsel4vka/libsel4vka.a libsel4/libsel4.a projects/util_libs/libplatsupport/libplatsupport.a projects/util_libs/libutils/libutils.a projects/musllibc/build-temp/lib/libc.a projects/util_libs/libpicotcp/picotcp_external/picotcp/build//lib/libpicotcp.a /usr/lib/gcc/x86_64-linux-gnu/6/crtend.o /host/test/lib/crtn.o -o projects/camkes/ethdriver.instance.bin && :
/usr/bin/ld: projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj: in function `camkes_iommu_dma_alloc':
/host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:48: undefined reference to `sel4utils_iommu_dma_alloc_iospace'
/usr/bin/ld: projects/camkes/CMakeFiles/ethdriver.instance.bin.dir/__/global-components/components/Ethdriver/src/plat/pc99/common.c.obj: in function `pc99_eth_setup':
/host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:71: undefined reference to `simple_get_iospace'
/usr/bin/ld: /host/test/../projects/global-components/components/Ethdriver/src/plat/pc99/common.c:88: undefined reference to `sel4utils_make_iommu_dma_alloc'
I checked all the files in the Ethdriver component and for me it seems that all should be fine, thus I cannot find/see the error (or the missing configuration).
(The only file I edited was picoserver.camkes but that is irrelevant.)
Any help/hint would be very appreciated.
Best regards,
Benjamin
[View Less]
Hello,
Is there any way in seL4 (library function?) to check free heap memory?
Thank you,
Leonid
________________________________
This message and all attachments are PRIVATE, and contain information that is PROPRIETARY to Intelligent Automation, Inc. You are not authorized to transmit or otherwise disclose this message or any attachments to any third party whatsoever without the express written consent of Intelligent Automation, Inc. If you received this message in error or you are not …
[View More]willing to view this message or any attachments on a confidential basis, please immediately delete this email and any attachments and notify Intelligent Automation, Inc.
[View Less]
