Other than formal verification of your Ring 0 and Ring 1 kernel components, (L4 not withstanding- there seems like genuinely interesting innovation coming out o

Other than formal verification of your Ring 0 and Ring 1 kernel components, (L4 not withstanding- there seems like genuinely interesting innovation coming out of that project), it seems like the rest of those are re-implementations of concepts that have been around for decades. We've gone full circle back into virtualization that IBM System 360 -> z-Series and VAX/VMScluster had. The difference is now you have all this tech that used to cost millions of dollars, available for a few hundred thousand dollars, making it way more accessible to the "non-SAP/Oracle/IBM" demographic. RE: seL4 borrows a lot of TrustedBSD (and to some extent Trusted Solaris). I don't know what the technical implementation details of Xen/XenServer are but once you add all the doo-dads, you've basically got VMware ESX with VMotion/HA/VSan in terms of functionality. I'll give VMware credit because VSan appliances are an easy-to-configure-and-deploy HA fairly-high-IOPS component of the VMware suite that's going to be a EMC SAN killer. The innovation there is how well it's integrated into the rest of the VMware virtual networking/vMotion/HA/disaster recovery suite, though, and not anything you could present at a conference. I haven't looked at Mirage recently but I don't think they're doing anything really groundbreaking (i.e. academically; you won't see papers being presented on it)- a clever unikernel and useful tool but certainly not research. Read the old IBM Redbooks for z/OS and there's are numerous common components between the 1980s implementation of a System/390 running a hypervisor and and the Xen/ESX internals. I can only comment on IBM's stuff with confidence as a former IBMer, but VAX/VMS' clustering probably shares a lot of of what ESX is doing. Other than IBM and MSR, a heavy funder of SPJ at Haskell and F# support as a primary language, definitely paid for itself many times over w/r/t language research the Python 3.5 async await syntax-sugar and, to some extent semantics, which was influenced by C# clearly, derived from F#2. Apple has a few people working on Clang (though not LLVM IIRC, so eh). Facebook has a really interesting language agnostic suite of analysis (primarily static) which I'm tracking carefully because it looks like it has a boatload of interesting capabilities. There's a lot of interesting research going on, but not much of it is done by corporations, Microsoft Research notwithstanding.