On Mon, 16 May 2022 at 18:09, <[email protected]> wrote: > Hi all, > > I'm working on a Masters research project looking into mapping an > object-capability programming language onto seL4, in a way that includes > some kind of mapping from the language object capabilities onto seL4's > capabilities (or vice versa). > > I'm at a stage of the project now where it would be really helpful to have > some 'motivating examples' for transferring caps between threads/CSpaces. > So I was hoping I could reach out to other seL4 developers to see if they > had built any systems that made extensive use of moving capabilities > around. Ideally, in an ocap language, these examples would be much easier > to program than they currently would be in C... > > The simplest example I can think of is a memory allocation server, but > that wouldn't necessarily involve handing caps on beyond the one > (requesting) process, which is the kind of thing I think more interesting > examples would comprise of. > > Fantastic to hear you will be digging into this! I think I remember you bringing this up in #MontE in the summer.
After running process construction, the next obvious example is opening files. You might have a program that wants the user to select a picture or document to open, and so it requests the user's file picker (powerbox) to make that request. If the user selects a file to give to the program, it hands a capability back to the requester. I'm currently working in driver code, so my mind turns there - when you plug a new device into a system, the driver needs to initialise it and make it available to the user, at which point they might grant some program access to the device; or alternatively some program might have a capability to enumerate new devices of a certain type. If you want more complex examples, building shells that can express capability concepts is one. You might want to provide a running process access to listen on a new tcp port, or grant it more of the CPU, or map another directory into its store. TBF there's already a wealth of prior art to build on there; from Ka-Ping Yee through Norm Hardy's writings on shells to Shill and to Genode's launcher. Any of these would benefit from being able to leverage an existing capability language. I also think that you digging into this stuff will help explore one issue that we will have building large scale systems on existing capability architectures. Capability languages have for the most part been forward-thinking enough that capability invocation is an asynchronous activity. This appears to be a good thing from a liveness perspective because you can invoke other domains without being starved for CPU yourself. On the other hand, capability-based kernels have tended to only implement synchronous send and receive. This is fine if you can trust every subsystem you call, but it is a problem we will need to solve as we build bigger systems. I have begun to explore this in Coyotos, but so far I've had Bigger Fish to Fry. It will be really interesting to see what your research here turns up. -- William ML Leslie _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
