Thanks for the big reply Will. I have no idea what #MontE is so I don't think that was me 😅.
Files and Drivers (or a Driver Manager perhaps) are two examples I've started to curate. A photo picker for mobile phone apps is one motivation that strikes me as a good one - e.g. choosing a photo to post on a social media site shouldn't dictate that its app needs complete access to your filesystem! I'd come across SHILL but got a bit scared off by its sandbox environment and Racket basis. It's been the same for many Javascript-based languages and implementations - big language/runtime bases to have to first wrangle into working on a microkernel... The Genode launcher sounds like something I need to look into. Your last point on sync v.s. async is indeed one of the core problems that's come up in the research so far. I've been looking a lot at the Pony language, which is capabilities-secure, and has a neat system of 'reference capabilities' for tracking usage rights on object *references*. It also aims at C-level performance which made it seem a good pick for systems development on seL4 (as opposed to say, Javascript...). However one of the primary mechanisms the rcap system is contingent on is the actor model the language is built around, and the fact that all actor interaction is done with asynchronous, non-blocking, send-only message passing (termed actor "behaviours"). Messages are just quickly popped onto queues (in the same address space, another potential seL4 problem) and get picked up to be run by the runtime scheduling later, and rest of the code after the message send point just continues on from there. So to do something dependent on an actor behaviour, introducing some kind of callback would become essential (the language also has no async/await). This leads to somewhat of an impedance mismatch because some kind of asynchronous message pump between ocap vats may be required to get it working on seL4 across protection domains, as capability *transfer* only works with a synchronous Send() call on an seL4 Endpoint capability. Asynchronous events between domains can be implemented with seL4 Notifications, but can't do the cap transfer. It's leading me to think that "the perfect ocap language" for seL4 might need ways to express both synchronous and asynchronous invocations. So I'm now trying to look around at other ocap language implementations to see if there's anything better I could try adapt, lest I have to arrive on the conclusion of writing a whole new language (which I don't really have time for...). If you happen to know of any ocap languages with synchronous stylings do let me know... Cap'n Proto, whilst not strictly a langauge per se, has also recently struck me as something that might be worth looking at, as it seems that when I look at trying to map ocap contexts onto seL4 protection domains, the API contracts between domains become pretty important. CAmkES is probably another example of this. My experience with capabilities stems more from working with the Barrelfish microkernel in the Advanced OS course at ETH Zurich, and I know that an interface definition language (Flounder, loosely documented here https://barrelfish.org/publications/TN-011-IDC.pdf) was a core part of the Barrelfish project too. (I don't think we were allowed to use it though!) _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
