I have become quite familar with L4/x86 Reference manual and
L4 User manual (for MIPS) but I think they don't give
enough information about
designing and writing programs on to the L4 architecture.
In my opinion they are
a bit unclear and incomplete.
Therefore I'd like to ask some questions on that subject.
What kind of address space do the initial servers get? I
know that sigma0 has the
complete physical address space idempotently mapped but
what about others?
What pages do they have initially mapped?
I have understood that the kernel isn't able to free memory
it has allocated.
Is that true?
How is the destination address of an intercepted IPC
delivered to the chief?
What is sigma1? What should it do?
Is sigma0 able to map memory above 0x40000000? How?
What happens when the version numbers of a task are used
up? Could they be reused?
Could tasks donate interrupts like they can donate task
numbers?
Thanks for everyone who bothers to answer.