sel4 / sel4 Goto Github PK
View Code? Open in Web Editor NEWThe seL4 microkernel
Home Page: https://sel4.systems
License: Other
The seL4 microkernel
Home Page: https://sel4.systems
License: Other
ARCH=arm PLAT=imx6 CPU=cortex-a9 ARMV=armv7-a DEBUG=1 make
--- a/configs/imx6/autoconf.h
+++ b/configs/imx6/autoconf.h
@@ -41,6 +41,7 @@
#define CONFIG_LIBSEL4DEBUG_FUNCTION_INSTRUMENTATION_NONE 1
#define CONFIG_LIB_SEL4_UTILS 1
#define CONFIG_LIB_SEL4_VSPACE 1
+#define CONFIG_PRINTING 1
#define CONFIG_LIB_PLATSUPPORT 1
#define CONFIG_LIB_SEL4_ALLOCMAN 1
#define CONFIG_HAVE_LIB_SEL4_SIMPLE_DEFAULT 1
@@ -71,14 +72,14 @@
#define CONFIG_HAVE_LIB_SEL4_SIMPLE 1
#define CONFIG_ARCH_ARM 1
#define CONFIG_HAVE_LIB_ELF 1
-#define CONFIG_PLAT_SABRE 1
+#define CONFIG_PLAT_WANDQ 1
#define CONFIG_HAVE_LIB_PLATSUPPORT 1
#define CONFIG_NUM_DOMAINS 16
#define CONFIG_HAVE_LIB_UTILS 1
#define CONFIG_USER_OPTIMISATION_O2 1
#define CONFIG_LIB_CPIO 1
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
-#define CONFIG_ROOT_CNODE_SIZE_BITS 12
+#define CONFIG_ROOT_CNODE_SIZE_BITS 14
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_TESTPRINTER_REGEX ".*"
#define CONFIG_APP_SEL4TEST 1
@@ -93,3 +94,5 @@
#define CONFIG_BUILDSYS_USE_CCACHE 1
#define CONFIG_MAX_NUM_NODES 1
#define CONFIG_KERNEL_STACK_BITS 12
+#define CONFIG_ENABLE_BENCHMARKS 1
+#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
leads to:
[CC] kernel_final.s
In file included from ./include/plat/imx6/plat/machine/hardware.h:19:0,
from ./include/arch/arm/arch/32/mode/machine.h:19,
from ./include/machine.h:17,
from ./include/api/syscall.h:14,
from src/api/faults.c:16:
./include/arch/arm/arch/benchmark_overflowHandler.h: In function ‘handleOverflowIRQ’:
./include/arch/arm/arch/benchmark_overflowHandler.h:31:9: error: implicit declaration of function ‘armv_handleOverflowIRQ’ [-Werror=implicit-function-declaration]
armv_handleOverflowIRQ();
^~~~~~~~~~~~~~~~~~~~~~
./include/arch/arm/arch/benchmark_overflowHandler.h:31:9: error: nested extern declaration of ‘armv_handleOverflowIRQ’ [-Werror=nested-externs]
cc1: all warnings being treated as errors
Makefile:626: recipe for target 'kernel_final.s' failed
make: *** [kernel_final.s] Error 1
Guarding benchmark_overflowHandler.h with a #ifdef leads to following link error:
[LD] kernel.elf
kernel.o: In function `benchmark_arch_utilisation_reset':
sel4.git/./include/arch/arm/armv/armv7-a/armv/benchmark.h:20: undefined reference to `ccnt_num_overflows'
sel4.git/./include/arch/arm/armv/armv7-a/armv/benchmark.h:20: undefined reference to `ccnt_num_overflows'
collect2: error: ld returned 1 exit status
Makefile:643: recipe for target 'kernel.elf' failed
Am I on the right track here?
Currently libsel4 has support for more than just interfacing to the kernel, it should be simplified and also it would be desirable to not require libc to use libsel4. The current libc (musl) contains support for many system calls not provided by seL4, one example is thread creation and there are other features, such as capabilities which musl will not likely ever support.
Therefore not having libsel4 depend upon libc can significantly reduce the amount of code needed for some uses of seL4. See this thread (http://sel4.systems/pipermail/devel/2015-June/000391.html) for some additional discussion.
This line https://github.com/seL4/seL4/blob/master/tools/lex.py#L46 causes this error:
# make
[KERNEL]
[MKDIR] arch/object
[PBF_GEN] arch/object/structures.pbf
[PBF_GEN] plat/32/plat_mode/machine/hardware.pbf
[PBF_GEN] 32/mode/api/shared_types.pbf
[BF_GEN] arch/object/structures_gen.h
Traceback (most recent call last):
File "/home/podhrad/Workspace/sel4/test_default/kernel/tools/bitfield_gen.py", line 29, in <module>
import lex
File "/home/podhrad/Workspace/sel4/test_default/kernel/tools/lex.py", line 46, in <module>
from past.builtins import cmp
ImportError: No module named past.builtins
/home/podhrad/Workspace/sel4/test_default/kernel/Makefile:699: recipe for target 'arch/object/structures_gen.h' failed
make[1]: *** [arch/object/structures_gen.h] Error 1
tools/common/project.mk:258: recipe for target 'kernel_elf' failed
make: *** [kernel_elf] Error 2
After commenting out line 46 compilation works as before.
We have experimental support for seL4 as platform for Genode and updated to 2.1.0 recently. Since then we've got strange page faults in src/arch/x86/kernel/apic.c.
========== KERNEL EXCEPTION ==========
Vector: 0xe
ErrCode: 0x0
IP: 0x100335
SP: 0xe0100de4
FLAGS: 0x96
CR0: 0x8000003b
CR2: 0x100335 (page-fault address)
CR3: 0x13a000 (page-directory physical address)
CR4: 0x290
Stack Dump:
*0xe0100de4 == 0xe0103097
...
From my investigation, this is caused by the call to pit_init()
which is marked PHYS_CODE
, but the calling function apic_measure_freq()
is marked BOOT_CODE
since 64aed53. Do we miss some detail when building seL4 for Genode?
Compilation error generated by clang:
~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:786:9: error: variable 'asid_map' is used uninitialized whenever 'if' condition is false [-Werror,-Wsometimes-uninitialized]
if (cap_get_capType(vspaceCapSlot->cap) == cap_pml4_cap) {
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:798:59: note: uninitialized use occurs here
poolPtr->array[asid & ((1ul << (asidLowBits))-1ul)] = asid_map;
^~~~~~~~
~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:786:5: note: remove the 'if' if its condition is always true
if (cap_get_capType(vspaceCapSlot->cap) == cap_pml4_cap) {
^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:785:5: note: variable 'asid_map' is declared here
asid_map_t asid_map;
^
Problematic code from ~/seL4test/kernel/src/arch/x86/64/kernel/vspace.c:
exception_t
performASIDPoolInvocation(asid_t asid, asid_pool_t *poolPtr, cte_t *vspaceCapSlot)
{
asid_map_t asid_map;
if (cap_get_capType(vspaceCapSlot->cap) == cap_pml4_cap) {
cap_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid);
cap_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1);
asid_map = asid_map_asid_map_vspace_new(cap_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap));
} else {
#ifdef CONFIG_VTX
assert(cap_get_capType(vspaceCapSlot->cap) == cap_ept_pml4_cap);
cap_ept_pml4_cap_ptr_set_capPML4MappedASID(&vspaceCapSlot->cap, asid);
cap_ept_pml4_cap_ptr_set_capPML4IsMapped(&vspaceCapSlot->cap, 1);
asid_map = asid_map_asid_map_ept_new(cap_ept_pml4_cap_get_capPML4BasePtr(vspaceCapSlot->cap));
#endif
}
poolPtr->array[asid & MASK(asidLowBits)] = asid_map;
return EXCEPTION_NONE;
}
I get a compiler error when I try to compile seL4 as a hypervisor. The error message is:
[CC] src/sel4_bootinfo.o
In file included from /home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/faults.h:16:0,
from /home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4.h:25,
from /home/ajgacek/phase3-workspace/next-phase3/libs/libsel4/src/sel4_bootinfo.c:11:
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4_arch/faults.h: In function 'seL4_getArchFault':
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4_arch/faults.h:50:58: error: 'seL4_Fault_VGICMaintenance_IDX' undeclared (first use in this function)
return seL4_Fault_VGICMaintenance_new(seL4_GetMR(seL4_Fault_VGICMaintenance_IDX));
^
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4_arch/faults.h:50:58: note: each undeclared identifier is reported only once for each function it appears in
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/include/sel4/sel4_arch/faults.h:52:52: error: 'seL4_Fault_VCPUFault_HSR' undeclared (first use in this function)
return seL4_Fault_VCPUFault_new(seL4_GetMR(seL4_Fault_VCPUFault_HSR));
^
/home/ajgacek/phase3-workspace/next-phase3/stage/arm/exynos5/common/common.mk:254: recipe for target 'src/sel4_bootinfo.o' failed
make[1]: *** [src/sel4_bootinfo.o] Error 1
tools/common/project.mk:306: recipe for target 'libsel4' failed
make: *** [libsel4] Error 2
The error seems to stem from commit b827ad3. See also https://github.com/seL4/seL4/blob/master/libsel4/sel4_arch_include/aarch32/sel4/sel4_arch/faults.h#L50.
Further to #33, I decided to do a bit of digging to see if I could figure out where that async abort was coming from.
Let's start with the some details:
And to recap, here's the async abort on return to user space (c.f. sel4test-driver's virt_entry) I'm seeing with an unmodified debug build:
=> fatload mmc 1:1 $loadaddr sel4test-driver-image-arm-imx6 && bootelf $loadaddr
reading sel4test-driver-image-arm-imx6
3065572 bytes read in 165 ms (17.7 MiB/s)
## Starting application at 0x20000100 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A9 r2p10
paddr=[20000100..202f041f]
ELF-loading image 'kernel'
paddr=[10000000..10037fff]
vaddr=[e0000000..e0037fff]
virt_entry=e0000000
ELF-loading image 'sel4test-driver'
paddr=[10038000..103fafff]
vaddr=[10000..3d2fff]
virt_entry=1de7c
Enabling MMU and paging
Jumping to kernel-image entry point...
DIDRv: 3, armv 70, coproc baseline only? no.
CPU is in secure mode. Enabling debugging in secure user mode.
Bootstrapping kernel
Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on data at address 0x7b63f3a2 with status 0x1c06
in thread 0xffdfad00 "rootserver" at address 0x1de7c
Okay, so let's turn on async aborts everywhere and see what blows up. Step 1: Add cpsie a
to the kernel's _start
and see what happens:
Bootstrapping kernel
KERNEL DATA ABORT!
Faulting instruction: 0xe0000338
FAR: 0xeb25bbaa DFSR: 0x1c06
halting...
Nice! Working backwards just to make sure the abort didn't exist earlier in the boot chain, I also initialised CPSR and turned on async abort interrupts in elfloader's _start
. Same error. Nice!
What's the faulting instruction?
e0000300 <initL2Cache>:
e0000300: e30330ff movw r3, #12543 ; 0x30ff
e0000304: e3a00000 mov r0, #0
e0000308: e34f3ff0 movt r3, #65520 ; 0xfff0
e000030c: e52de004 push {lr} ; (str lr, [sp, #-4]!)
e0000310: e1a02003 mov r2, r3
e0000314: e3001121 movw r1, #289 ; 0x121
e0000318: e3430c07 movt r0, #15367 ; 0x3c07
e000031c: e3a0e203 mov lr, #805306368 ; 0x30000000
e0000320: e30fcfff movw ip, #65535 ; 0xffff
e0000324: e5830005 str r0, [r3, #5]
e0000328: e5831009 str r1, [r3, #9]
e000032c: e583100d str r1, [r3, #13]
e0000330: e583ee61 str lr, [r3, #3681] ; 0xe61
e0000334: e583c67d str ip, [r3, #1661] ; 0x67d
e0000338: e592367d ldr r3, [r2, #1661] ; 0x67d /* !!! */
e000033c: e6ff3073 uxth r3, r3
e0000340: e3530000 cmp r3, #0
e0000344: 1afffffb bne e0000338 <initL2Cache+0x38>
...
Fine, I'll be a jerk about it and disable the L2 cache. On the off chance it doesn't blow up elsewhere, we'll have narrowed things down at least.
Lo and behold!
Bootstrapping kernel
... 8< ... lots of test output ... 8< ...
218/222 tests passed.
*** FAILURES DETECTED ***
Looks like the imx6 platform doesn't have its own initL2Cache
function, so I'll have to start digging into src/arch/arm/machine/l2c_310.c
. (So far I'm a wee bit flummoxed by the difference between what's in kernel_final.c
versus kernel_final.s
.)
Given it's an async/imprecise abort, it's not necessarily that instruction that caused the problem, but at least we know something's going awry with the L2 cache. I might see what happens if I tell u-boot not to initialise or use it…
sel4.systems is not reachable. Probably module lxml is not installed properly.
ProcessId: 3936
Interpreter: 'sel4.systems.keg.ertos.in.nicta.com.au'
ServerName: 'sel4.systems.keg.ertos.in.nicta.com.au'
DocumentRoot: '/var/www/seL4/content'
URI: '/home.pml'
Location: '/home.pml'
Directory: None
Filename: '/var/www/seL4/content/home.pml'
PathInfo: None
Phase: 'PythonHandler'
Handler: 'ertos'
Traceback (most recent call last):
File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1537, in HandlerDispatch
default=default_handler, arg=req, silent=hlist.silent)
File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 1202, in _process_target
module = import_module(module_name, path=path)
File "/usr/lib/python2.7/dist-packages/mod_python/importer.py", line 304, in import_module
return __import__(module_name, {}, {}, ['*'])
File "/var/www/seL4/code/ertos.py", line 5, in <module>
from lxml import etree
ImportError: No module named lxml
There are times when IPC needs to happen, but a sending process cannot wait around for another process to be receiving. seL4_NBSend is basically the system call for this, but it never provides any feedback whether or not IPC took place.
Can the seL4 be compiled in thumb mode?
When trying to build seL4 on distros where Python 3 is the default python (such as Arch), the build fails when running python files as they are are python2 code, instead of python3.
The shebang should be:
#!/usr/bin/env python2.7
I imagine this isn't the right place for this, but i can't find a better one.
I see the performance comparisons at http://l4hq.org/docs/performance.php are run on all different processors. In its current form, the performance numbers here are completely useless. It would be very informative to have real performance benchmarks where the exact same processor is used for every OS in comparison. Otherwise, what am I supposed to do with those number?
Required if one wants to use the bindings with shared libraries as done on Genode/seL4.
When testing x86_64 debug builds under hardware virtualisation (KVM rather than QEMU's TCG), the suite succeeds up to TEST_FPU0001
, then grinds the CPU at 100%. This happens with the default FXSAVE
, XSAVEOPT
, a non-simulation build, etc.
Any thoughts as to what might be causing it, how I should approach debugging it, etc.?
Starting test 19: TEST_FPU0000
TEST_FPU0000
Running test FPU0000 (Ensure that simple FPU operations work)
Test FPU0000 passed
Starting test 20: TEST_FPU0001
TEST_FPU0001
Running test FPU0001 (Ensure multiple threads can use FPU simultaneously)
(I filed this here because it makes more sense to me that this would be an issue with the kernel than the test suite, but I could very well be wrong!)
The roadmap is out of date — for example, it lists tasks as “to-do” with expected completion dates in the past. This is a feature request that the roadmap be updated to reflect the current situation.
src/kernel/thread.c:125:13: error: logical not is only applied to the left hand side of this comparison [-Werror,-Wlogical-not-parentheses]
if ((!!(!seL4_Fault_get_seL4_FaultType(sender->tcbFault) != seL4_Fault_NullFault))) {
I think there's a mess with !
usage here.
On our test machine, nightly tests are unstable since we connected a custom USB-HID test device that acts rather dynamically with periodic connect-disconnect cycles. The symptom is that the kernel boot just hangs during PCI scan. I traced this down to console_putchar()
in src/plat/pc99/machine/io.c which produces the hang by not returning, and for me the following code looked suspicious
while (!(in8(port + 5) & 0x60));
The implementation checks if the THRE 0x20 or TEMT 0x40 flag was set in the UART. If I remove TEMT from the check all tests work as expected. Also, most other UART drivers I know of just check for THRE as the flag is defined as the UART is ready to accept a new character for transmission (from http://archive.pcjs.org/pubs/pc/datasheets/8250A-UART.pdf).
Hello
I installed sel4 on ubuntu o.s. Now I want to install container engine(Docker/kubernetes) on the top of Sel4 microkernel.
Can anyone please help me with the steps.
Thanks.
I compiled the sel4 3.1.0 kernel [0]
make ARCH=x86 PLAT=pc99 SEL4_ARCH=ia32 DEBUG=y
and started afterwards it by
qemu-system-i386 -kernel kernel.elf -serial stdio
but get no output at all.
Doing the same with sel4 2.1.0 [1] and 3.0.1 leads to some kernel messages.
Also on native x86 hardware I get on 2.1.0 and 3.0.1 output, but nothing for the
3.1.0 kernel. Also tried with recent git master [2].
Additionally I git bisected between 3.0.1 and 3.1.0 and beginning with commit 541289a there is no output anymore.
In file included from seL4/src/api/faults.c:16:
In file included from seL4/include/api/syscall.h:15:
In file included from seL4/include/machine.h:18:
In file included from seL4/include/plat/pc99/plat/machine/hardware.h:15:
seL4/include/plat/pc99/plat/machine/interrupt.h:53:17: warning: implicit conversion from enumeration type 'interrupt_t' (aka 'enum _interrupt_t') to different enumeration type 'irq_t' (aka 'enum _irq_t') [-Wenum-conversion]
irq_t ret = x86KSPendingInterrupt;
~~~ ^~~~~~~~~~~~~~~~~~~~~
seL4/include/plat/pc99/plat/machine/interrupt.h:78:29: warning: implicit conversion from enumeration type 'irq_t' (aka 'enum _irq_t') to different enumeration type 'interrupt_t' (aka 'enum _interrupt_t') [-Wenum-conversion]
x86KScurInterrupt = servicePendingIRQ();
~ ^~~~~~~~~~~~~~~~~~~
This is a feature request for mitigating against Spectre variant 1 attacks.
At present, Kconfig
contains the entries about arm926ej_s
and IntegratorCP
:
config ARM926EJ_S
bool "ARM926EJ-S"
depends on ARCH_ARM
select ARCH_ARM_V5
help
Support for ARM926EJ_S
However, there is no architecture support for armv5
/arm926ej_s
. Would it be better if the related configuration entries are removed?
The idle thread uses the hard-coded CPSR value PMODE_IDLE
, which does not mask FIQs or async aborts. If an async abort is pending, the kernel will fault as soon as the system becomes idle.
I see this fault happening on i.MX6Q, presumably triggered by a bad device register access in either the loader or the kernel's serial or timer drivers. Depending on the platform it may also be possible to deliberately trigger it from a user thread that has device registers mapped.
This was fixed before by commit a5f61c7, but it looks like the fix was lost in a merge with the hyp support branch. Also, the CPSR_IDLETHREAD
value added by that commit has not been updated for hyp; it should use PMODE_IDLE
instead of PMODE_SYSTEM
.
Nothing major -- links 2, 3 reference dead pages on the sel4.systems website, and link 5 is actually a redirect.
For your convenience here's a patch to correct the links.
Patch: https://github.com/watbe/seL4/commit/74276ce9ccd7489a06bc8cfd90aa0fc4a3d429cc.patch
Hi,
When trying to build for the Tegra K1, I got the following issue. To reproduce the issue:
In file included from /home/sel4/tegra-test/stage/arm//include/platsupport/io.h:24:0,
from /home/sel4/tegra-test/stage/arm//include/platsupport/timer.h:17,
from /home/sel4/tegra-test/libs/libplatsupport/src/arch/arm/generic_timer.c:18:
/home/sel4/tegra-test/stage/arm//include/platsupport/clock.h:27:36: fatal error: platsupport/plat/clock.h: No such file or directory
compilation terminated.
make: *** No rule to make target src/arch/x86/machine_asm.S', needed by
src/arch/x86/machine_asm.s'.
Hii
Can anyone please help me how to install sel4 on top of ubuntu?
Like the instructions for installation
Thanks
In file tool/invocation_header_gen.py
, around line 80:
enum sel4_arch_invocation_label {
{{for label, condition in invocations}}
...
{{label}} = nInvocationLabels,
...
{{endfor}}
nSeL4ArchInvocationLabels
}
On ia32, becasue seL4_arch_invocations
is an empty list, this will cause nSeL4ArchInvocationLabels
to be declared as 0, rather than nInvocationLabels
as intented.
Userspace processes need to be protected against Spectre attacks by other such processes. While the seL4 security claim does not extend to covert channels, timing attacks are a significant threat when untrusted code and trusted code are running on the same system.
Domains, while awesome for high-integrity software development where all trusted code is known a priori, do not suffice for this use case, because they are too strict: the number of domains, and the fraction of the CPU allocated to each, must be set at compile time (at least if I am reading the documentation correctly). As such, e.g. a version of QubesOS on seL4 would not be able to use them.
This issue also applies regarding cross-VM, VM→user, and user→VM attacks.
The Makefile tries to add the tools directory to the path, but doesn't properly quote in the case that the original PATH has spaces in it. Fixed by quoting the variable assignment as follows:
diff --git a/Makefile b/Makefile
index 2ab6292..737edfa 100644
--- a/Makefile
+++ b/Makefile
@@ -158,7 +158,7 @@ default: all
### Tool setup
############################################################
-PATH := ${SOURCE_ROOT}/tools:${PATH}
+PATH := "${SOURCE_ROOT}/tools:${PATH}"
export PATH
PARSER = c-parser
When compiling seL4 for the TK1 with profiling turned on, I get the following error:
/home/ajgacek/phase3-workspace/camkes/kernel/include/plat/tk1/plat/machine/hardware.h:157:9: error: implicit declaration of function 'handleOverflowIRQ' [-Werror=implicit-function-declaration]
handleOverflowIRQ();
I think that hardware.h
file is missing
#include <arch/benchmark_overflowHandler.h>
I noticed that the KE95 summer projects, 12/2010 – 2/2011 was about porting seL4 to 64-bit Intel.
http://ertos.nicta.com/education/summer.pml
I'm filing this issue to get some documentation/feedback on what happened and possibly feasability or plans for this.
I am compiling seL4 for the ARM, Exynos5410 (Odroid-XU, ARMv7a, Coretx A15) with hypervisor support and it fails with the following messages:
[AS] kernel.o
kernel_final.s: Assembler messages:
kernel_final.s:522: Error: Banked registers are not available with this architecture. -- `msr sp_usr,lr'
kernel_final.s:524: Error: Banked registers are not available with this architecture. -- `msr elr_hyp,lr'
kernel_final.s:526: Error: Banked registers are not available with this architecture. -- `msr spsr_hyp,lr'
kernel_final.s:528: Error: selected processor does not support ARM mode `eret'
kernel_final.s:66215: Error: Banked registers are not available with this architecture. -- `msr sp_usr,lr'
kernel_final.s:66217: Error: Banked registers are not available with this architecture. -- `msr elr_hyp,lr'
kernel_final.s:66219: Error: Banked registers are not available with this architecture. -- `msr spsr_hyp,lr'
kernel_final.s:66221: Error: selected processor does not support ARM mode `eret'
kernel_final.s:67378: Error: Banked registers are not available with this architecture. -- `msr sp_usr,lr'
kernel_final.s:67380: Error: Banked registers are not available with this architecture. -- `msr elr_hyp,lr'
kernel_final.s:67382: Error: Banked registers are not available with this architecture. -- `msr spsr_hyp,lr'
kernel_final.s:67384: Error: selected processor does not support ARM mode `eret'
make[1]: *** [kernel.o] Error 1
make: *** [kernel_elf] Error 2
Hello,
it would be great if the section on VM faults could be extended, I can say nothing regarding ARM but for IA32 the following changes would be great:
Change the ARMish term 'FSR' to the more x86ish 'Page-Fault Error Code'.
When describing the contents of IPCBuffer[3] state that it is a exact copy of the Page-Fault Error Code which the CPU produces on a page fault. A reference to the following would be great (https://www-ssl.intel.com/content/dam/www/public/us/en/documents/manuals/64-ia-32-architectures-software-developer-system-programming-manual-325384.pdf, p. 135-137). This part of the intel manual describes this value in full detail.
Hi,
When running repo sync command this error will occured.
Can anyone help me?
Line 295 in c5184b8
This is a feature request for an epoll-like polling system that allows one thread to wait on a message to be sent to any of N different endpoints/notifications, using at most O(log N) time per receive. Currently, this can be emulated with threads, but threads are relatively expensive, while my hope is that this would not be.
Does it work at a32 mode? And which compiler fit for it? I would be very appreciate if someone could give me some detailed information.
After reading the Qemu tutorial on seL4 wiki, I can run 32-bit version smoothly with following scripts
make clean
make optiplex9020_defconfig
make silentoldconfig
make
cd images
qemu-system-x86_64 -m 512 -kernel kernel-ia32-pc99 -initrd capdl-loader-experimental-image-ia32-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic
However, I cannot run 64-bit version with error fsgsbase instructions not supported by the processor reported using almost the same scripts except x86_64 parameters.
......
make x64_optiplex9020_defconfig # x64
......
sudo qemu-system-x86_64 -m 512 -kernel kernel-x86_64-pc99 -initrd capdl-loader-experimental-image-x86_64-pc99 --enable-kvm -smp 2 -cpu Nehalem,+vmx -nographic #x86_64
My CPU is i7 6700 (Skylake) and FSGSBASE is enabled (checked by lscpu | grep fsgsbase).
Can anyone help me, please?
Hi,
I want to boot seL4 test on imx6q-sabrelite and I do as https://docs.sel4.systems/Testing.html. Now there is a problem for me like that:
Do you have any ideas?
Thank you !
On Genode/x86 we use for all of our 7 supported x86 micokernels the BIOS data area to read out the serial configuration. This eliminates for us the need to manually finding out the I/O ports, which is especially handy on native machines you don't have next to you. Also the support of external users becomes comfortable since most the time the serial output 'just' works. We combine this mechanism with a small chained bootloader like bender [0, 1] that scans for PCI serial cards or/and Intel AMT SerialOverLine, writes it to the BIOS data area and then starts the actual microkernel.
What is your opinion about adding this BDA feature to seL4 in general ?
alex-ab/genode@4c1fe8b depicts the required changes, we currently apply manually to our Genode/seL4 version. (I decided for now to add extra cmdline options, which however are not strictly necessary for us.)
python sel4/libsel4/tools/syscall_stub_gen.py --buffer -a ia32 --word-size 32 -o ...
Traceback (most recent call last):
File ".../libsel4/tools/syscall_stub_gen.py", line 821, in <module>
sys.exit(main())
File ".../libsel4/tools/syscall_stub_gen.py", line 817, in main
generate_stub_file(args.arch, wordsize, args.files, args.output, args.buffer)
File ".../libsel4/tools/syscall_stub_gen.py", line 725, in generate_stub_file
result.append("assert_size_correct(%s, %d);" % (x.name, x.native_size_bits / 8))
TypeError: unsupported operand type(s) for /: 'str' and 'int'
I would like to point out that identifiers like "__API_H
" and "__MACHINE_H
" do not fit to the expected naming convention of the C language standard.
Would you like to adjust your selection for unique names?
vspace.c: In function init_boot_pd
vspace.c:58:23error: array subscript is above array bound ....
Tried using the flag, and can recreate this on multiple machines
in allocate_bi_frame():
/* create the bootinfo frame object */
pptr = alloc_region(BI_FRAME_SIZE_BITS); <--allocated BI_FRAME_SIZE_BITS
if (!pptr) {
printf("Kernel init failed: could not allocate bootinfo frame\n");
return 0;
}
clearMemory((void*)pptr, PAGE_BITS); <-- clear PAGE_BITS
It allocates one size, but clears another. Per chance they are the same so the whole thing didn't blow up.
Compiling the seL4 kernel on ARM with hypervisor support and fastpath disabled produces a linker error about the function slowpath missing. The definition of this function is guarded by an #ifdef FASTPATH:
https://github.com/seL4/seL4/blob/master/src/arch/arm/32/hyp_traps.S#L286
If I move it out of the #ifdef block, everything compiles and links.
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.