Is there a plan to add UEFI support in seL4 for x86 hardware in the near
future? Newer x86 boards are frequently UEFI only. It is possible to
get around the lack of UEFI support, as I have done with the UP board:
https://up-community.org/wiki/Hardware_Specification
but I am hitting problems which I will detail below.
When I compile using ia32_debug_xml_defconfig and boot using the
resulting images the board fails to find the RSDP location. To fix this
I had to modify the source code a bit:
* seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.h
+ #define UPBOARD_RSDP 0x5B161000
* seL4test/projects/util_libs/libplatsupport/src/plat/pc99/acpi/acpi.c
- acpi->rsdp = acpi_sig_search(acpi, ACPI_SIG_RSDP,
strlen(ACPI_SIG_RSDP),
- (void *) BIOS_PADDR_START, (void *)
BIOS_PADDR_END);
+ acpi->rsdp = (void *)UPBOARD_RSDP;
* seL4test/kernel/src/plat/pc99/machine/acpi.c
- for (addr = (char*)BIOS_PADDR_START; addr < (char*)BIOS_PADDR_END;
addr += 16) {
+ for (addr = (char*)0; addr < (char*)PPTR_BASE; addr += 16) {
It would be handy to have this as a kernel parameter to cover cases
where it is not successfully discovered automatically. With these
changes I can boot the board and several tests pass but then I get stuck
on INTERRUPT0001 (Test interrupts with timer). I don't get a test
failure or an error the board just sits and makes no more progress.
Someone had that test fail in this post:
https://sel4.systems/pipermail/devel/2017-February/001328.html
and the first recommendation was to check if the irq of the timer was
correctly found. I booted the board into linux to find the correct irq
which was listed as 0 in /proc/interupts. I added a printf to
handleInterrupt in the kernel source, recompiled and when I booted seL4
I found that the irq reported to handleInterrupt is 125 (which sel4
reports as the max interrupt value) every time that function is called.
Adding this printf also showed me that when the test hangs the board
hasn't crashed or locked up as calls to handleInterrupt are made
continuously.
At this point I noticed that before any tests started to run several
ACPI tables are not recognized:
Parsing ACPI tables
Skipping table FPDTD, unknown
Skipping table FIDT<9c>, unknown
Skipping table UEFIB, unknown
Skipping table TPM24, unknown
Skipping table LPIT^D^A, unknown
Skipping table BCFG9^A, unknown
Skipping table PRAM0, unknown
Skipping table CSRTL^A, unknown
Skipping table BCFG9^A, unknown
Skipping table OEM0<84>, unknown
Skipping table OEM1@, unknown
Skipping table PIDVÜ, unknown
Skipping table RSCI,, unknown
Skipping table WDAT^D^A, unknown
Warning: skipping table ACPI XSDT
Maybe one or more of those tables needs to be loaded to handle
interrupts properly. The LPIT table is conspicuous in the case of the
timer test but I think other tests are likely to depend on the other tables.
Any suggestions about porting this type of hardware?
--
Edward Sandberg
Adventium Labs
111 3rd Avenue S. Suite #100
Minneapolis, MN 55401
ed.sandberg(a)adventiumlabs.com
Hello,
I realize that the only officially supported SMP platform is the i.mx6 but I did see some code on 6.0 to master for SMP and the zynq7000 so I am trying to test out some SMP functionality on my zc702 board.
I am wondering if anyone has this working because my system is failing when compiling from master and the 6.0 and compatible tags.
My second core seems to be coming up but the system ultimately fails and prints out:
Bo
ot
nKgE RaNlEl L fDinAiTsAh eAdBO, RdT!r
ppFaeud lttio nugs eirn stspraucctei o
n: 0xe001d1b0 o
FAR: 0xfffffff8 DFSR: 0x807
halting...
Kernel entry via Syscall, number: 1, Call
Cap type: 1, Invocation tag: 37
Which seems to be "Booting all finished, dropped to user space" from core0 and "KERNEL DATA ABORT!" from core1.
The "0xe001d1b0" seems to be the label of the "idle_thread" function.
While stepping through via JTAG, I have verified that core1 gets through "init_kernel" and then enters "restore_user_context" at some point in "restore_user_context" the fault registers as shown in the printed output are set. I think it is either in the c_exit_hook in restore_user_context or after the program branches to "0xFFF0010" which is "ldr pc,0xFFFF0030". This branches to the "arm_data_abort_exception" label, which goes to "kernel_data_fault" label and then to "kernel data abort".
I'm having trouble exactly pin pointing where the fault occurs but it seems to be close to there.
Has anyone had similar issues with SMP? It seems to get fairly far without setting the fault registers.
I have tried to step through the execution over JTAG and here are some of my (verbose) notes
| CORE0 Address | Core0 Function | Core0 Instruction | CORE1 Address | Core1 Function | Core1 Instruction | DFSR | DFAR | Note |
|---------------+-----------------------------+------------------------+---------------+------------------------------------+----------------------+------------+------------+------|
| 0x10000000 | label: start | =cpsid aif= | 0xFFFFFF34 | | =mvn r0,#0x0f= | 0x00000000 | 0x00005000 | |
| 0x10003A2C | call: platform_init | =bl -x10003DD8= | 0xFFFFFF30 | | =wfe= | 0x00000000 | 0x00005000 | |
| 0x10003ACC | call: smp_boot | =bl 0x100039FC= | 0xFFFFFF34 | | =mvn r0,#0x0f= | 0x00000000 | 0x00005000 | |
| 0x10003ADO | ret: smp_boot | =bl 0x10005C54= | 0x10000020 | in: non_boot_core | =orr r0,r0,#0x40= | 0x00000000 | 0x00005000 | 2 |
| 0x10003ADC | =if(is_hyp_mode())= | =beq 0x10003AF0= | 0x10002200 | label: arm_disable_dcaches | =push {r14}= | 0x00000000 | 0x00005000 | |
| 0x10003AFC | call: arm_enable_mmu | =bl 0x10002174= | 0xE0006190 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 |
| 0xE0001D70 | label: init_kernel | =push {r11,r14}= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 |
| 0xE0001814 | label: try_init_kernel | =push {r11,r14}= | 0xE0001690 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 |
| 0xE0001B80 | call: create_initial_thread | =str r0, [r11,#-0x14]= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1 |
| 0xE0001C48 | call: SMP_COND_STATEMENT | =bl 0xE0003C20= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1, 3 |
| 0xE0001C4C | call: SMP_COND_STATEMENT | =bl 0xE00017D8= | 0xE0001680 | in: try_init_kernel_secondary_core | =beq 0xE0001680= | 0x00000000 | 0x00005000 | 1, 4 |
| 0xE0001C50 | NODE_LOCK_SYS | =bl 0xE0019280= | 0xE0019288 | in: getCurrentCPUIndex | =sub r13,r13,#0x8= | 0x00000000 | 0x00005000 | 5 |
| 0xE0001D1C | call: arch_pause | =bl 0xE0019DB0= | 0xE0019290 | in: getCurrentCPUIndex | =str r0,[r11,#-0x8]= | 0x00000000 | 0x00005000 | 6 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE00037F4 | in: init_core_state | =pop {r4,r11,pc}= | 0x00000000 | 0x00005000 | |
| 0xE0001D20 | in: clh_lock_acquire | =mov r2,#0xE800= | 0xE0003754 | in: init_core_state | =movw r2,#0xE8E0= | 0x00000000 | 0x00005000 | 7 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE00017C4 | in: try_init_kernel_secondary | =mov r3,#0x1= | 0x00000000 | 0x00005000 | 8 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE002A06C | in: schedule | =push {r11,r14}= | 0x00000000 | 0x00005000 | 9 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE002979C | in: activateThread | =push {r11, r14}= | 0x00000000 | 0x00005000 | 10 |
| 0xE0001D40 | in: clh_lock_acquire | =uxtb r3,r3= | 0xE001D24C | label: Arch_activateIdleThread | =push {r11}= | 0x00000000 | 0x00005000 | 11 |
| 0xE0001D38 | in: clh_lock_acquire | =ldr r3,[r3,#0x4]= | 0xE0000054 | in: start | =b 0xE001CEC8= | 0x00000000 | 0x00005000 | 12 |
Notes
1. Core1 is in a =while (!node_boot_lock)= loop
2. In =smp_boot=, CORE1 changes after =init_cpus= (branch location: ZSR:10003A08)
- In =smp_boot=, =boot_cpus= is called
- This sets the =CPU_JUMP_PTR= =*((volatile uint32_t*)CPU_JUMP_PTR) = (uint32_t)entry;=
- calls =dsb= (data synchronization barrier)
- After this call, CPU1 goes to =FFFFFF2C: dsb sy=
- And then =sev=
- After this call, CPU1 goes to the =non_boot_core= label
- SEV
- SEV causes an event to be signaled to all cores within a multiprocessor system. If SEV is implemented, WFE must also be implemented.
- WFE
- If the Event Register is not set, WFE suspends execution until one of the following events occurs:
- an IRQ interrupt, unless masked by the CPSR I-bit
- an FIQ interrupt, unless masked by the CPSR F-bit
- an Imprecise Data abort, unless masked by the CPSR A-bit
- a Debug Entry request, if Debug is enabled
- an Event signaled by another processor using the SEV instruction.
- If the Event Register is set, WFE clears it and returns immediately.
- If WFE is implemented, SEV must also be implemented.
- After CPU0 executes =arm_enable_mmu()= from the =main= function
- by the end of =smp_boot= core1 is just starting =non_boot_main=
3. The =SMP_COND_STATEMENT= is calling =clh_lock_init=
4. The =SMP_COND_STATEMENT= is calling =release_secondary_cpus=
5. right after Core0 returned from releasing secondary cpus
- First time Core1 has exited the loop
- Core1's stack is
- =getCurrentCPUINdex=
- =init_core_state=
- =try_init_kernel_secondary_core=
- =init_kernel=
6. Core0 is in a =while(big_kernel_lock.node_owners[cpu].next->value ! = CLHState_Granted)=
- Core0 is in a static inline function =clh_lock_acquire= in =try_init_kernel=
- Core1 is in =getCurrentCPUIndex= but being called from =tcbDebugAppend=
- =tcbDebugAppend= is being called from a =for= loop in =init_core_state=
7. Core0 is still in the previously mentioned while loop
- Core1 is in "init_core_state" and has exited the for loop that called =tcbDebugAppend(NODE_STATE_ON_CORE(ksIdleThread, i))=
8. Core0 is still in the previously mentioned while loop
- Core1 has returned to =try_init_kernel_secondary_core= from =init_core_state= and is at the end of the function
9. Core0 is still in the previously mentioned while loop
- Core1 has entered the =init_kernel= call and then the =schedule= function.
10. Core0 is still in the previously mentioned while loop
- Core1 has entered the =activateThread= call after =schedule= in =init_kernel=
11. Core0 is still in the previously mentioned while loop
- Core1 seems to have dropped into the =case ThreadState_IdleThreadState:= case when switching on =switch (thread_state_get_tsType(NODE_STATE(ksCurThread)->tcbState))=
- This was in =activateThread=
12. Core0 is still in the previously mentioned while loop
- Core1 has exited =init_kernel= and is now branching to =restore_user_context=
To test everything out I am using the "camkes-sols-master" manifest and building the "CAmkES Hello World application with events and dataports".
The changes I made are
* I edited the top level CAmkES file to set the affinity for two separate cores.
* Upped the Max Number of CPU nodes to 2
The rest of the config is pretty standard. I have it attached to this message.
The FSBL and ps7_init script I use are the standard ones created for the zc702 from the 2017.2 version of the Xilinx XSDK.
I am booting from jtag and first run the ps7_init script and then flash the fsbl and then the "capdl-loader-experimental-image-arm-zynq7000" that was built.
I am wondering if anyone is using a modified fsbl or ps7_init that does something else, if there is config value that I missed, or if it is still in development? If it is still in development I'd like to work with whoever is
Thanks,
Jesse Millwood
Hello,
I am working with seL4 7.0.0 on the zynq7000 platform. I have come across a bug
that occurs when a device physical memory region includes the highest address,
i.e. where the memory region ends at 0xFFFFFFFF on 32 bit systems. When I
create a CAmkES component that uses the highest address, I see the following error.
ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0
paddr=[10000000..100ac81f]
ELF-loading image 'kernel'
paddr=[0..32fff]
vaddr=[e0000000..e0032fff]
virt_entry=e0000000
ELF-loading image 'capdl-loader-experimental'
paddr=[33000..1aefff]
vaddr=[8000..183fff]
virt_entry=befc
Enabling MMU and paging
Bootstrapping kernel
Booting all finished, dropped to user space
<<seL4(CPU 0) [decodeUntypedInvocation/210 T0xffdfd100 "rootserver" @8fa8]:
Untyped Retype: Insufficient memory (1 * 4096 bytes needed, 0 bytes available).>>
Warning: using printf before serial is set up. This only works as your
printf is backed by seL4_Debug_PutChar()
[Err seL4_NotEnoughMemory]:
I have traced this problem to an integer overflow bug in the capdl-loader. The
patch below shows how I have addressed this error.
>From 22c9dd76a31713c98710830c2ea865a4e5d8a078 Mon Sep 17 00:00:00 2001
From: Jeff Kubascik <jeff.kubascik(a)dornerworks.com>
Date: Wed, 27 Sep 2017 13:52:36 -0400
Subject: [PATCH] Fixed integer overflow bug in capdl-loader that occurs when a
device physical memory region ends at 0xFFFFFFFF
---
capdl-loader-app/src/main.c | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/capdl-loader-app/src/main.c b/capdl-loader-app/src/main.c
index 34eedb0..305da2a 100644
--- a/capdl-loader-app/src/main.c
+++ b/capdl-loader-app/src/main.c
@@ -554,7 +554,7 @@ static int find_device_object(void *paddr, seL4_Word type,
int size_bits, seL4_C
/* Assume we are allocating from a device untyped. Do a linear search for it */
for (unsigned int i = 0; i < bootinfo->untyped.end -
bootinfo->untyped.start; i++) {
if (bootinfo->untypedList[i].paddr <= (uintptr_t)paddr &&
- bootinfo->untypedList[i].paddr +
BIT(bootinfo->untypedList[i].sizeBits) >= (uintptr_t)paddr + BIT(size_bits)) {
+ bootinfo->untypedList[i].paddr +
BIT(bootinfo->untypedList[i].sizeBits) - 1 >= (uintptr_t)paddr + BIT(size_bits)
- 1) {
/* just allocate objects until we get the one we want. To do this
* correctly we cannot just destroy the cap we allocate, since
* if it's the only frame from the untyped this will reset the
--
2.7.4
I have added a -1 to the end address calculations to fix the edge case when
bootinfo->untypedList[i].paddr + BIT(bootinfo->untypedList[i].sizeBits) is equal
to 0x100000000, an integer overflow. The current statement is comparing the
address of the next byte past the end of the memory region. My change is
comparing the address of the last byte in the memory region.
I have tested this fix on the zynq7000 and it works. However, I am not too
familiar with the capdl-loader. Are there any problems with this fix that I
have not considered?
Thanks,
Jeff Kubascik
Not sure if this is the best place to post this question but I noticed on
the seL4 roadmap page on the website that 64-bit support for ARM is due out
at the end of 3Q2017. Is that correct, and if so, can someone give me some
hints of where to look for it in the repository?
Hi,
I am trying to run sel4 on QEMU, i am following this steps(https://wiki.sel4.systems/Hardware/Qemu)
make clean
make optiplex9020_defconfig
make silentoldconfig
make
but while doing make i am getting following error..
/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c: In function ‘get_breakpoint_format’:/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:130:27: error: ‘seL4_InstructionBreakpoint’ undeclared (first use in this function) *break_type = seL4_InstructionBreakpoint; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:130:27: note: each undeclared identifier is reported only once for each function it appears in/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:131:19: error: ‘seL4_BreakOnRead’ undeclared (first use in this function) *rw = seL4_BreakOnRead; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:135:27: error: ‘seL4_DataBreakpoint’ undeclared (first use in this function) *break_type = seL4_DataBreakpoint; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:136:19: error: ‘seL4_BreakOnWrite’ undeclared (first use in this function) *rw = seL4_BreakOnWrite; ^/home/arun/test_default/libs/libsel4camkes/src/gdb_server/gdb.c:146:19: error: ‘seL4_BreakOnReadWrite’ undeclared (first use in this function) *rw = seL4_BreakOnReadWrite; ^make[1]: *** [src/gdb_server/gdb.o] Error 1make: *** [libsel4camkes] Error 2
can you please give any solution to solve these errors..
RegardsAshok
Hi
I am trying to cross-compile sel4 for rasperry-pi-3.
i am executing following command on sel4 kernel source to cross-compile.
TOOLPREFIX=arm-linux-gnueabi- ARCH=arm PLAT=bcm2837 ARMV=armv8-a CPU=cortex-a53
i am getting following error while doing make
[BF_GEN] arch/object/structures_gen.h
[BF_GEN] plat/machine/hardware_gen.h
[BF_GEN] 32/mode/api/shared_types_gen.h
[CPP] src/arch/arm/armv/armv8-a/32/machine_asm.s_pp
In file included from src/arch/arm/armv/armv8-a/32/machine_asm.S:11:0:
./include/config.h:17:22: fatal error: autoconf.h: No such file or directory
compilation terminated.
make: *** [src/arch/arm/armv/armv8-a/32/machine_asm.s_pp] Error 1
rm 32/mode/api/shared_types_gen.h plat/machine/hardware_gen.h arch/object/structures_gen.h
is there any solution for this...
RegardsAshok
So, I know that at a basic level, a block device driver would probably need
I/O permissions, and I'm guessing that it would be handling requests from a
file system driver.
Is that basically how the seL4 software ecosystem is laid out? What's
typical for how "software in the wild" is actually organized and layered on
top of the microkernel?
I only know about seL4 from a theoretical standpoint, read the manual and
stuff, and mostly familiar with the actual kernel, but I'm a complete noob
when it comes to actual software.
Hi,
I am trying to cross-compile seL4 for rapsberry pi 3 using steps mentioned hereseL4 on the Raspberry Pi 3
|
| |
seL4 on the Raspberry Pi 3
| |
|
I am getting following error while compiling, are there any patches available to fix this error: [STAGE] libsel4sync.a[libs/libsel4sync] done.[apps/sel4test-tests] building... [HEADERS] [STAGE] test_init_data.h [STAGE] arch/* [STAGE] arch_frame_type.h [STAGE] autoconf.h [CC] src/helpers.o [CC] src/main.o [CC] src/tests/multicore.o [CC] src/tests/preempt.o [CC] src/tests/serial_server.o [CC] src/tests/breakpoints.o [CC] src/tests/scheduler.o [CC] src/tests/pagetables.o [CC] src/tests/inc_untyped.o [CC] src/tests/interrupt.o [CC] src/tests/sync.o [CC] src/tests/iopt.o [CC] src/tests/ioports.o [CC] src/tests/vspace.o [CC] src/tests/ipc.o [CC] src/tests/schedcontext.o [CC] src/tests/fpu.o [CC] src/tests/ept.o [CC] src/tests/trivial.o [CC] src/tests/binding.o [CC] src/tests/cnodeops.o [CC] src/tests/threads.o [CC] src/tests/cspace.o [CC] src/tests/regressions.o/tmp/cc7e2jo9.s: Assembler messages:/tmp/cc7e2jo9.s:120: Error: selected processor does not support ARM mode `ldrex r2,[r3]'/tmp/cc7e2jo9.s:154: Error: selected processor does not support ARM mode `strex r0,r3,[r2]'make[1]: *** [src/tests/regressions.o] Error 1make: *** [sel4test-tests] Error 2user@user-Lenovo:~/seL4test$
Thanks,Prathamesh
Hi guys,
This is Ashokkumar, i want to write a sample serial(UART) communication user-space driver in sel4,can i get any help from your side. I am just started sel4 i don't know how to build and execute the programs,if you have any documents or examples about user-space programs please share with me...
RegardsAshok
Hello *,
I hope you're all doing well. I recently got seL4 running on my Raspberry
Pi 3, and wanted to report some notes here and ask some questions regarding
the port, and perhaps get some help working on a patch (or twelve, I'm
sure.)
Recently I followed the Data61 blog post here to get a recent copy of seL4
on my RPi, but hit a few errors along the way that burned some time. In
particular I got burned by the U-Boot glitch and getting seL4 building due
to a glitch in the 'repo' setup for sel4test: https://research.csiro.au/
tsblog/sel4-raspberry-pi-3/
I ended up writing my own blog post, with effectively "fully reproducible"
instructions (e.g. one of the codepad.org links on the RPi3 wiki page was
dead) for a recent build. This includes proper setup for uboot.env in order
to `fatload` and `bootm` the seL4 ELF binary off disk, the right U-Boot
version, and using Docker to build the seL4 image:
https://inner-haven.net/posts/2017-09-15-sel4-rpi3.html
That's all fine, but...
I got curious about this U-Boot glitch, as even a recent (git) copy of
U-Boot still suffered from the issue reported in the original Data61 blog
post. I found it strange this regression would exist for nearly 9 months,
unless it was possibly something intentional (e.g. an intended behavioral
change) or it went unreported.
The glitch is this: after booting the seL4 binary, the system immediately
hangs with no output after trying to start the sel4test application. This
glitch did not occur in versions of U-Boot up-to v2017.01. Versions
v2017.03 and later (to now) suffer.
I decided to spend some time bisecting this problem and found the issue.
Versions of U-Boot after v2017.01 include the following patch, which causes
the data cache to be enabled prior to U-Boot loading and executing ELF
binaries:
https://github.com/thoughtpolice/u-boot/commit/
995eab8b5b580b67394312b1621c60a71042cd18
This behavior previously existed as a workaround for QNX, which required
that the dcache be disabled before execution. U-Boot, previously, disabled
the dcache when booting *any* ELF binary at all (the binary can of course
enable it or check to see if it isn't enabled already), as a simplistic
workaround. This patch changes it to only disable the dcache on U-Boot
images (uImages) marked as QNX ELF binaries, so that QNX systems boot
properly still.
It would seem then that seL4 -- or at least sel4test -- requires the dcache
to be disabled upon entry for the RPi3. If the dcache is enabled, as in the
above patch, it otherwise hangs immediately.
In fact, a recent copy of U-Boot *can* execute seL4 properly: you simply
have to use `./tools/mkimage` inside U-Boot to mark the application as
`mkimage -C none -A arm -T kernel -O qnx -d <input> <output>` first -- this
creates a uImage with the appropriate header to mark the ELF as a QNX
binary. U-Boot recognizes this and appropriately disables the dcache before
application entry, once you use `bootm` or something.
I took the time to write a patch to U-Boot in order to add a new OS
definition -- "sel4" -- in order to address this problem more clearly. My
change is here:
https://github.com/thoughtpolice/u-boot/commit/
720caf6c398584658abfa883d4d390f4b6200269
With this change, you can mark any seL4 binary as `-O sel4` to create an
appropriately bootable uImage, with the dcache appropriately disabled.
Assuming this is in place, the following U-Boot commands will execute seL4:
U-Boot> setenv bootfile uImage
U-Boot> fatload mmc 0 ${loadaddr} ${bootfile}
U-Boot> bootm ${loadaddr}
## Booting kernel from Legacy Image at 00200000 ...
Image Name:
Image Type: ARM seL4 Kernel Image (uncompressed)
Data Size: 3385548 Bytes = 3.2 MiB
Load Address: 00000000
Entry Point: 00000000
Verifying Checksum ... OK
Loading Kernel Image ... OK
CACHE: Misaligned operation at range [20000000, 200078bc]
CACHE: Misaligned operation at range [200078bc, 2032a720]
CACHE: Misaligned operation at range [2032c000, 2033c820]
## Starting application at 0x20000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A53 r0p4
paddr=[20000000..2033c81f]
ELF-loading image 'kernel'
paddr=[0..32fff]
vaddr=[e0000000..e0032fff]
virt_entry=e0000000
ELF-loading image 'sel4test-driver'
paddr=[33000..44dfff]
vaddr=[10000..42afff]
virt_entry=2a03c
Enabling MMU and paging
Jumping to kernel-image entry point...
----
So with that all done, it's clear there's a change needed *somewhere* but
I'm not sure where or what to do:
1) Is the above the right approach? Clearly, seL4 on the RPi3 assumed a
disabled dcache during its development, but this has now changed, so for
this platform something will need to be fixed, such as the above.
2) Or perhaps this is not a U-Boot problem, but should be fixed in seL4.
Or in sel4test. For example, is there an option to assume the dcache is
already enabled in the configuration? Maybe that should be toggled instead.
Or does seL4 *always* assume it is disabled at boot? What about non-RPi3
platforms like other ARM systems? These likely use U-Boot as well, but it's
unclear if the cache should be disabled here, too. In this case, the above
U-Boot patch is (in theory) wrong, but if that's true, it was always wrong
to begin with (as it always disabled the cache prior to ELF loading).
If something like this was the case, then the rpi3 configurations (or
perhaps some bootinfo code) needs to change.
3) Alternatively, this is just an outright bug in seL4 that should be
fixed and U-Boot was previously masking it. (I'm not sure if the proofs
cover this one :)
4) Perhaps it should be a mix of both. For example, perhaps the
sel4/sel4test code should be changed to assume an already-enabled dcache,
or fixed outright. But perhaps a U-Boot patch would still be good to submit
upstream: for example, I could submit the above patch upstream, but
*remove* the dcache code. This would allow U-Boot users to mark seL4
binaries appropriately for clarity and future compatibility and make U-Boot
"officially support" seL4. And in the future, should seL4 need more
patches/workarounds/requirements from U-Boot, it would be easier to add and
maintain them.
---
I'd prefer not to run myself into dead ends trying to get the wrong
solution upstream to either seL4 or U-Boot, and it would be great to fix
this for users. I'd also like to look into more adventurous stuff in the
future (like multicore on the RPi3 which seems unsupported), so any advice
is appreciated to get started. Even then: bisection and the patch creation
only took an hour, so if it's wrong, not much was lost.
--
Regards,
Austin - PGP: 4096R/0x91384671
