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/fff76a36a02b8ccef3aa0b201751c57b62ac3... and https://github.com/seL4/util_libs/blob/fff76a36a02b8ccef3aa0b201751c57b62ac3... 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?