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
We have a multi component camkes application with each component using a
few common services and then having application interfaces to a small
number of other components.All these components are imported into a top
level system description camkes file.
Examining the generated camkes I see that all the generated header and
source files have exactly the same make prerequisites meaning a change to
logically unrelated components causes them all to be regenerated and
recompiled.
Now I have discovered the camkes cache this is less of an issue but is
there a better way we can structure our application to reduce the
edit-compile-go cycle ?
Regards
Gordon
We have a security requirement on our ARM based product using CAmkES 2.2.x
to ensure all sensitive data declared in specific seL4SharedData regions
are erased on detection of a power failure. We achieve this by overwriting
the data with a known pattern that we read back from a separate component
before declaring the device as secured. This is working fine. But we need
to guarantee that the overwrite data is actually written to DDR and we
aren't just using cached values. This means flushing the L1 and L2 data
caches specific regions.
We could use seL4HardwareMMIO regions and declare our data in the memory
map and use these regions as un-cached. Or use the _hardware_cached
attribute and call the provided flush method when necessary. Our main issue
with doing this, except the fiddle of mapping multiple different sized
regions into the memory map, is we could potentially expose the physical
locations of the sensitive data rather than having it wrapped in the
virtual address space of a component.
Having a flush method on seL4SharedData would be the ideal solution.
We are not in a position to upgrade our CAmkES version on this product at
the moment.
Any thoughts?
Zippy
Hi,
The PPTR address range between UART and GIC distributor was 12k
(kernel/include/plat/tx1/plat/machine/device.h). But when refer in TX1
reference sheet the length was specified as 64byte for UART,4k for GIC
distributor and 8k for interrupt controller.
can you please point out the reference or reason to choose this address for
Tx1 board?
/* These devices are used by the seL4 kernel. */
#define UARTA_PPTR 0xffffffffffff0000
#define GIC_DISTRIBUTOR_PPTR 0xffffffffffff3000
#define GIC_CONTROLLER_PPTR 0xffffffffffff4000
These addresses are used during kernel device map to access in the
userspace
map_kernel_devices : kernel_devices[i].paddr :0x50042000
kernel_devices[i].pptr 0xffffffffffff4000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]:
0xffffff800002b000 vaddr :0x1f4
map_kernel_devices : kernel_devices[i].paddr :0x50041000
kernel_devices[i].pptr 0xffffffffffff3000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]:
0xffffff800002b000 vaddr :0x1f3
map_kernel_devices : kernel_devices[i].paddr :0x70006000
kernel_devices[i].pptr 0xffffffffffff0000
map_kernel_frame - armKSGlobalKernelPT[GET_PT_INDEX(vaddr)]:
0xffffff800002b000 vaddr :0x1f0
Regards,
Munees
Hi seL4 Dev Team,
I am bringing up the sel4 kernel on tx2 board with ref of Tx1. I
encountered the TLB invalidation hang issue after kernel map window setup.
I do not know the exact reason for hang so just disable that piece of code
to look further execution of sel4 kernel. After that it dropped into the
usersapce and throwing the cap fault or vm fault issue.
Does anyone has come across this type of issue and how it debugged?.
Please share your thought or pointers to debug this issue. I shared the
full log details here.
## Starting application at 0x82000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3
paddr=[82000000..827abfff]
kernel_phys_start: 0xffffffff80000000
kernel_phys_end:0xffffffff8022fcdf
load_elf : image_size 0x230000
ELF-loading image 'kernel'
paddr=[80000000..8022ffff]
vaddr=[ffffff8000000000..ffffff800022ffff]
virt_entry=ffffff8000000000
load_elf : image_size 0x5e9000
ELF-loading image 'sel4test-driver'
paddr=[80230000..80818fff]
vaddr=[400000..9e8fff]
virt_entry=41b160
Enabling MMU and paging
Jumping to kernel-image entry point...
kernel_info.virt_entry : 0x0
user_info.phys_region_start : 0xffffffff80230000
user_info.phys_region_end:0xffffffff80819000
user_info.virt_region_start:0x400000
user_info.virt_region_end:0x9e9000
user_info.phys_virt_offset:0x7fe30000 user_info.virt_entry:0x41b160
Bootstrapping kernel
Booting all finished, dropped to user space
Caught cap fault in send phase at address 0x0
while trying to handle:
vm fault on code at address 0x41b160 with status 0x82000010
in thread 0xffffff8027ef4200 "rootserver" at address 0x41b160
With stack:
halting...
Kernel entry via VM Fault, fault type: 4305248
Thanks in advance
Muneeswaran R
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
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
Hi Sel4 Dev Team,
Any update of SMP and Hypervisor feature which fully functional on TX2. If
its not available when will get this feature supported .
Regards,
Munees
Hello,
I am attempting to port the camkes-arm-vm to the zynqmp platform. For the TK1 and Exynos platforms, the physical address of the hardware devices are well below the kernelBase of 0xe0000000. However, for the zynqmp, these hardware devices are greater than the kernel base. This causes the "map_emulated_device" function call to fail for the GIC and any other passthrough devices.
sel4utils_reserve_range_at_no_alloc@vspace.c:589 Range not available at 0xff010000, size 0x1000
Assertion failed: res.res (/home/chrisguikema/seL4/NAMC/camkes-arm-vm/libs/libsel4arm-vmm/src/devices.c: map_device: 160)
Is there a way to 1:1 map these devices, even if they are above the kernelBase?
Thanks,
Chris
Hi,
I am trying to bring up sel4 on tegra Tx2 platform using tegra Tx1 as
reference.
I tweaked the important changes of UART,Timer configuration and IRQ number
and also GIC controller, GIC distributor configuration w.r.t Tx2
after loading and booting the Tx2 board sel4 enter into init kernel to
initialize the kerenl memory map for GIC and UART devices then control
transfer to user space. I underdtand from ref manual both Tx1 and Tx2 using
the same clock and baud rate for UART configuration.
## Starting application at 0x82000000 ...
ELF-loader started on CPU: ARM Ltd. Cortex-A57 r1p3
paddr=[82000000..827abfff]
kernel_phys_start: 0xffffffff80000000
kernel_phys_end:0xffffffff8022fcdf
load_elf : image_size 0x230000
ELF-loading image 'kernel'
paddr=[80000000..8022ffff]
vaddr=[ffffff8000000000..ffffff800022ffff]
virt_entry=ffffff8000000000
load_elf : image_size 0x5e9000
ELF-loading image 'sel4test-driver'
paddr=[80230000..80818fff]
vaddr=[400000..9e8fff]
virt_entry=41b160
Enabling MMU and paging
Jumping to kernel-image entry point...
Also try to add debug print in the init kernel thread to understand the
virtual memory set-up but its crashed with synchronous exception.
It indicates that the UART driver till not available to log the messages
this was seen in Tx1 and Tx2. Not able to check/debug further on this issue.
Also experimented with various arbitrary address for UARTA_PPTR and
GIC_PPTR because Tx1 UARTA has 64byte size in case of Tx2 its 1MB.but still
nothing has improved the state remain same.
I completely walk through the sel4 boot and arm MMU code.I do not see any
board specific changes in this code apart from UART,GIC configuration and
IRQ number. The assembly code of MMU mainly setting up TCR ,TTBR , TLB
invalidation and pagetable setup for arma-57.
Please let me know your thought on this issue and how do debug this kind of
issue.
Regards,
Munees
Hello,
I want to learn about seL4 so I am trying to get is started on the hardware
I already have (a zynq 7000).
I have generated the image: sel4test-driver-image-arm-zynq7000
Now I try to load that onto the zynq by executing these commands in XMD:
connect arm hw
rst
fpga -f design_1_wrapper.bit
source ps7_init.tcl
ps7_init
ps7_post_config
dow sel4test-driver-image-arm-zynq7000
run
All of the above seem to be successful. Then, I have a serial link hooked
up to the board (uart)
and there I get the following output (screen /dev/ttyUSB1 115200) :
ELF-loader started on CPU: ARM Ltd. Cortex-A9 r3p0
paddr=[10000000..103c881f]
ELF-loading image 'kernel'
paddr=[0..2afff]
vaddr=[e0000000..e002afff]
virt_entry=e0000000
But then nothing more. I am lost what to do from this position in order to
continue exploring seL4.
I don't even know if what I see is an indication of a problem or not.
If anyone has experience in running seL4 on zynq and if you sit on
knowledge you want to share,
please fill me in.
Thank you
