>>>>> On Fri, 29 May 2009 16:03:04 +0200,
[hidden email] said:
XL> Hi,
XL> I have (again) some questions about OKL4 structure:
XL> I asked in a previous mail the difference between cells and address spaces.
XL> Josh answered that in the case off a Linux cell there is one address space
XL> for each program and I don't understand if those address spaces are OKL4
XL> address spaces or Linux address spaces.
Both. Linux address spaces get mapped onto OKL4 address spaces. OKL4
(kernel) address spaces are essentially an abstraction for page tables.
XL> In this mail Josh also said that an address space is associated with exactly
XL> one clist but in the pdf "OKL4 Programming Overview of the OKL4 3.0 API" at
XL> page 54 the diagram shows 3 address spaces in 2 cells and 4 clists. What is
XL> the rule about that point?
That diagram is misleading, apologies.
XL> How to decide between address space and cell isolation for a given
XL> application?
a Secure HyperCell is a high-level abstraction, which is implemented
by using low-level kernel abstractions, including Clists and address
spaces. The system designer should think in terms of the higher-level
constructs. Cells define isolation domains. If multiple processes
exist in such a domain (as is the case in the example of a virtual
machine) then they each get mapped onto a kernel address space, all
typically sharing the same Clist (although sub-domains with further
restricted rights can be set up -- there is much more support for this
in future releases).
XL> I would like to know the status of the kernel proof of correctness.
About a month away from completion.
Gernot
_______________________________________________
Developer mailing list
[hidden email]
https://lists.okl4.org/mailman/listinfo/developer
