There is a whole library around this and similar techniques in Boost. I've used it before on several occasions. It's quite nice, although it somewhat lays a trap, in the sense that CPP really should be your metaprogramming technique of last (or second-to-last) resort, so it remaining difficult keeps your incentives in line. :)
I've never used Chaos PP (the predecessor of Boost.Preprocessor), but IIRC, it enables even more cool stuff at the cost of reduced portability (Boost.Preprocessor contains all the hacks to work on broken preprocessors, while I think Chaos takes more of a "fix your preprocessor" approach).
Has anyone seen open source user space for this? I find the kernel really interesting.
I'm a fan of the way they put device drivers in user space, for example. But I'm curious if anyone has actually written a NIC driver for it. I'd like to take it for a spin and write some sample code, but I'm not sure if I can boot this thing with a network stack for my experiments to use.
I was one of the early users of seL4 and am still a named author on the seL4 manual.
It's quite possible that things have changed/improved over the last few years, but when I was working on it, I found the programming environment to be, very, very difficult. The capability system suffers from several circular dependencies (e.g splitting up memory capabilities required cnode capabilities, making cnode capabilities required memory capabilities). And the userspace environment is very bare, you have to manage your own page-tables, and your own capabilities. That said, it is also very powerful if you want to write fast, secure, embedded programs, which is what it was really designed for.
I'm pretty sure they wrote a device driver for a network card as part of one of the projects, but I don't know if it ever made it out the door. I'm sure you could ask the current team to see if they did and if they would make it open. You never know, you might get lucky.
Yes but it's not general purpose. If you look you will find examples but they are all rather specific to hardware and usually also to the application running on top of the microkernel. I don't believe there is a Linux/Minix style "interactive userland" available at this time, and Genode while useful to begin building one, lacks the ability to just provide one "out of the box" on seL4.
I've never used Chaos PP (the predecessor of Boost.Preprocessor), but IIRC, it enables even more cool stuff at the cost of reduced portability (Boost.Preprocessor contains all the hacks to work on broken preprocessors, while I think Chaos takes more of a "fix your preprocessor" approach).
http://www.boost.org/doc/libs/1_59_0/libs/preprocessor/doc/i...