[okl4-developer] OKL4 structure questions

[Xavier.LANGELLIER at fr.thalesgroup.com]

Hi,

I have (again) some questions about OKL4 structure:

I asked in a previous mail the difference between cells and address spaces.
Josh answered that in the case off a Linux cell there is one address space
for each program and I don't understand if those address spaces are OKL4
address spaces or Linux address spaces.
In this mail Josh also said that an address space is associated with exactly
one clist but in the pdf "OKL4 Programming Overview of the OKL4 3.0 API" at
page 54 the diagram shows 3 address spaces in 2 cells and 4 clists. What is
the rule about that point?
How to decide between address space and cell isolation for a given
application?

I would like to know the status of the kernel proof of correctness.

Thanks.