Hi @djwillia - nice to see you here! It's really interesting to look into all the possible ways to isolate services; from pure emulation (arm on x86), to augumented emulation (Java with JIT) to hypercalls and containers. For my part I'm a big fan of Popek-Goldberg virtualization. The complete isolation it offers makes everything very portable (i.e. we can run on Windows / Mac / Linux with virtualbox) and the simplicity of an instruction-level isolation mechanism like that makes it easy to reason about it mathematically.
I'm certainly interested in higher-level interfaces, and we do have a project going to port the IncldueOS interface ported to userspace Linux. But I guess our priority is efficient, robust and portable Popek-Goldberg first, then everything else. Please let us know if you want to go any further with the virtio drivers - we'd love to collaborate.
And @avsm - I agree, C-linkage for ABI is a good approach - we can do that with a C++ compiler (unless there's a good reason not to?), which will just be a bit stricter about explicit type casts etc. The linker won't know the difference. Regarding compatibility with Mirage; is there an easy way to find the low-level requirements / ABI interface for it?