yorik.sar

On the second thought, you don’t even need microkernel here. Genode has “hw” platform that uses hardware features to provide everything that’s usually done in kernel. And Mill might do really good with it.

Genode is an OS framework (“an offspring of the L4 community” they say on wiki). It uses whatever microkernel you give it (NOVA, Fiasco, L4) and provides everything you need to get proper OS on top of it. It can also run Linux or FreeBSD processes within it. And it heavily uses services that Mill supports in hardware.

So I wonder if it would be easier to port L4 with Genode instead of Linux on top of it to Mill to get proper OS faster and with less effort.

I tried to post not so long post (about 1216 chars) and got… nothing (empty response). It looks like longer POST requests are just ignored.

If it does, how is that region verified? Should turf ids be the same as turf that running thread is in currently? Can application abuse this by saying “All TBs of my memory are portals. Go, verify”?
* How does that need for portals map to existing C APIs?

Thank you very much for what you do in both creating a really good architecture and teaching it.

* Some services might require passing a list of callbacks. Application will have to essentially build a number of portals in its data space. Can any application grant portal permissions to some address space that it can write?

Sorry for mixing things up in the comments. I can’t post long posts here somehow.

I also have some questions that bothered me throughout the talk.

* How do you create a turf? Who can create it? Can it be abused?
* Can you create a VMM that doesn’t have right to read/write/execute all the memory but can grant access to it? Can you decouple VMM from the rest of OS?

Great talk!

I found myself thinking that what you’re saying is mostly what I was thinking about when I was comprehending Genode OS Framework. I understood that you cannot do those ways efficiently and securely on x86. What’s missing is small and fast portals that you have! Are you going to build your OS for Mill with Genode or something like it?

Looks like it was an issue with the network I was in yesterday. Sorry to trouble you.

Ok, let me tests this again here. Here’s my original post:

Great talk!

I found myself thinking that what you’re saying is mostly what I was thinking about when I was comprehending Genode OS Framework. I understood that you cannot do those ways efficiently and securely on x86. What’s missing is small and fast portals that you have! Are you going to build your OS for Mill with Genode or something like it?

I also have some questions that bothered me throughout the talk.

* How do you create a turf? Who can create it? Can it be abused?
* Can you create a VMM that doesn’t have right to read/write/execute all the memory but can grant access to it? Can you decouple VMM from the rest of OS?
* Some services might require passing a list of callbacks. Application will have to essentially build a number of portals in its data space. Can any application grant portal permissions to some address space that it can write? If it does, how is that region verified? Should turf ids be the same as turf that running thread is in currently? Can application abuse this by saying “All TBs of my memory are portals. Go, verify”?
* How does that need for portals map to existing C APIs?

Thank you very much for what you do in both creating a really good architecture and teaching it.