Hi Alex,

I think this is a good direction to move in, and supporting MBI2 definitely makes sense. In an ideal world, yes we would try and cut out grub2 and be pure UEFI booted, but given current resources I cannot see that happening any time soon, and so I see no reason not to welcome MBI2 support.

As you point out some of the code itself is not perfect, but what it's actually doing seems fairly simple and non-controversial to me. Quite possibly you did this just to get it working as a proof of concept, but I would discourage adding more architecture information to the raw seL4_Bootinfo (the archInfo word is an old hack), and instead use the additional headers (https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo_types.h#L83). Aside from that, as you say the code needs some deduplication etc, but I'm happy to continue on github and get this in.

Adrian

On Fri 25-Aug-2017 11:31 PM, Alexander Boettcher wrote:
Hello,

since last week we successful added UEFI support to Genode/seL4 for x86.

In this course we extended the seL4 6.0 kernel (beside the NOVA kernel
and our own kernel - Genode/hw) to be also a Multiboot2 (MBI2) kernel.
The MBI2 specification [3] provides to the kernel the ACPI RSDP
information, which was the main reason to add MBI2 support. Together
with GRUB2 (as UEFI capable bootloader) we were able to get our setups
running on various native x86 machines and on Qemu.

Additionally we extended the 3 kernels to propagate the ACPI RSDP
information further to the user-land, since there the ACPI driver also
failed to lookup the ACPI RSDP information.

The patch for the seL4 kernel are currently on our staging branch (our
automatically tested branch) and will show up in the upcoming release
next week eventually.

Currently, the patches are tight to Genode, but I can open up a feature
issue on seL4 github if you are fine with the general direction - so
adding MBI2 support in general. Or you would rather go in another
direction like writing an own UEFI boot loader, which maybe is more
minimal compared to GRUB2 etc etc.

I have to admit, that the code addition to the seL4 kernel is far from
being optimal - amount of code because of redundant MBI 1 vs 2 code,
correctness of code (I'm not super familiar with the internals of the
seL4 kernel), missing framebuffer information etc - but this we may
discuss in more detail on github, if wanted.


Cheers,

Alex.

[0]
https://github.com/genodelabs/genode/commit/b9aa16eb3e671a7e3c1474b076a244c7c97e5dea
"sel4: kernel patch to get ACPI information"
[1]
https://github.com/genodelabs/genode/commit/c09783eed9a52ad72e8a1a986b832303574612ba
"sel4: add uefi boot support via mbi2"
[3]
http://git.savannah.gnu.org/cgit/grub.git/tree/doc/multiboot.texi?h=multiboot2

On 10.08.2017 16:50, Adrian.Danis@data61.csiro.au wrote:
Hi Edward,

In the near future? Unfortunately not. UEFI support is definitely something that we talk about every so often, but just never makes it high enough up the priority list for us internally.

A configuration option for overriding the RSDP search doesn't so too unreasonable in cases where there isn't a BIOS region to search. At least until we can retrieve the address from the UEFI runtime.

It is entirely possible that any number of tables and initialization needs to happen before the timer, or other hardware, will work. Currently the ACPI tables here are just being used to find the base address of the HPET, and it is assumed that it is in a working state and no further setup needs to be done.

As for the IRQ numbers in seL4 you are seeing the local CPU vector delivery number, not the source I/O APIC interrupt number or GSI. To determine the IRQ source you could check the x86KSIRQState for the local CPU vector (in this case 125), unpack the x86_irq_state_t type, and see where it came from.

The user code though is first trying to use the HPET and then if it cannot find that (i.e. it's not in the ACPI tables) then it falls back to the PIT. If it finds a HPET then it will try and use FSB (i.e. MSI) delivery, and failing that fall back to I/O APIC delivery. If you want to work out which of these its using you could either infer from the x86KSIRQState as mentioned above or instrument https://github.com/seL4/util_libs/blob/fff76a36a02b8ccef3aa0b201751c57b62ac3621/libplatsupport/src/plat/pc99/ltimer.c#L225 and https://github.com/seL4/util_libs/blob/fff76a36a02b8ccef3aa0b201751c57b62ac3621/libplatsupport/src/plat/pc99/ltimer.c#L306 to see what exactly it is doing.

Adrian

On Thu 10-Aug-2017 4:56 AM, Edward Sandberg wrote:

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?





_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel