L4 and Plan 9 or Inferno or both?

Some folks already started in on a Plan 9 port to L4 it seems (PDF), but I'm not sure how far they've gotten with it. I've been sort of peeping at L4 on and off for a long time now, and OKL4 has been successfully shipped in a few ARM phones, successfully being used to host Linux and a Qualcomm OS that drives the phone's radios and such. Neat stuff.

Been wondering if Plan 9 or Inferno and L4 are really a good marriage and what benefits could be added by leveraging Plan 9's namespace based resource management and L4's powerful IPC mechanisms.

As I've had a little more spare time lately, I've been digging around looking into L4 again, and I'm interested in exploring some ideas a little more deeply.

There's a few different implementations of L4 to look at...

OKL4 is now basically an ARM only platform in it's latest releases. Fiasco is a Pentium targeted L4 implementation that has a userland implementation that might be fun to work with (Fiasco-UX), and Pistachio is still being worked by at least a few people, with the latest changes coming in as of yesterday. Pistachio also supports a lot of architectures.

I'm tempted to play with each of these, but my problem has always been one of focus when it comes to these spare time projects as free time for me is usually at a premium.

Tim Newsham has been following the seL4 stuff, and OKL4 is migrating towards those APIs. His vote is I shoot for OKL4, so I believe that's where I'm going to start. There's a good community around that implementation, and a commercial pressure to keep things working nicely.

But as they say, talk is cheap... Let's see what I learn.

(UPDATE!)

Looks like a lot of progress was made by others who have already started this work!