Hi Bernhard,
you should perhaps take a look at Fiasco, which is an L4V2 kernel with the focus on real time properties.
Thx for advice. I will consider that code when we will look for a new os for our board.
A capability in L4.sec is a references to a kernel object and permissions to use it. Kernel objects are for example threads, endpoints or tasks. Permissions are whether it is allowed to send to an endpoint or to modify the state of a thread.
A capability space is a table of capabilities. These capabilities are referenced through task local numbers called capability id's. This is very similar to file descriptors in unix.
So,a capability is a machine word used like a pointer and another machine word used for the permissions or it is just a machine word with some of the most significant bits used as permission field? I see now that the capability space is a table. (So why don't call it capability table?) I think my problem is that some terms clash into my mind. I think the address space is and underlying hardware structure that permits access to structures in memory. I was probably misled by the name. I can imagine now that address space, capability space and io space are all structures from ur point of view. Isn't it? Am I correct if I think that MMU control is transparent to the concepts of the three spaces?
If you need some pictures to understand this, have a look at my thesis, where I give a short introduction into L4.sec. You can find the thesis at http://os.inf.tu-dresden.de/papers_ps/kauer-diplom.pdf
I already have read ur thesis. But probably I lack some knowledge to fully understand it. I'm studying the kernel code of L4 for this reason as well. Many thanks for ur answer, Anton