-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA512

On Sun, May 21, 2023 at 01:40:31PM +1000, William ML Leslie wrote:

Hello,

I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me.

Here's Intel's RFC:

https://www.intel.com/content/www/us/en/developer/articles/technical/envisio...

I think I might steal your IO port API for newer versions of Coyotos, which /is/ impacted by the change. TBF, I think seL4 has a better IRQ handling interface than the one we currently have too. I guess it's only fair it goes both ways!

(Off-topic) Where can I find information on Coyotos? What advantages does it have over seL4, and do you plan to formally verify it in the future? - -- Sincerely, Demi Marie Obenour (she/her/hers) Invisible Things Lab

On 5/20/23, William ML Leslie william.leslie.ttg@gmail.com wrote:

Hello,

I just noticed in the new x86-S rfc that Intel published that there will be no further support for io port access for processes in ring 3. Thankfully, this doesn't look like it will impact seL4, which provides capabilities to special objects representing port ranges on x86, which are then implemented in the kernel. Just in case anyone was wondering if there will be any impact, since this is the one thing that stuck out to me.

I'd actually thought of trying to add support for direct use of PMIO instructions in user code under seL4 at one point, but there's probably not much of a point in that because modern performance-critical devices most often use just MMIO only. Really I'm not sure why Intel wouldn't just do away with PMIO entirely and just map ports onto MMIO (like on non-x86 architectures with PCI-like buses) if they're trying to clean up legacy cruft.

Another thing that would be an issue is the 32-bit boot code. I have preliminary code in my custom Multiboot loader for loading a 64-bit kernel directly into long mode, but I only ever used it with earlier experiments and never with seL4. I have disabled the ELF32 kernel conversion in my OS since my loader supports ELF64 binaries even though only 32-bit entry is working with seL4. Of course, my loader works rather differently than the CAmkES/seL4CP one does (the image is a list of separate Multiboot modules, one per file, rather than a cpio archive linked into the root server), so it wouldn't necessarily be a replacement.