Re: Sigma1

[Luke A Guest]
> I've read that the kernel could allocate pages from sigma0, is this
> not correct?

If you look at the Version X2 reference manual you'll see that a
kernel thread can indeed allocate memory from sigma0.  This has not
been implemented yet.  We just use a boot time option to tell the
kernel how much memory it should allocate for itself.

You should note that the protocol described in the manual is only
supposed to be used during bootup; i.e., to allow the kernel to grab
some more memory during startup.  The lack of a mechanism for the
kernel to give memory back to sigma0 should prompt you to see that
this is the case.  Further, supporting the protocol during runtime
requires sigma0 to somehow make a decision about which application
memory to revoke and give to the kernel.  It is far beyond sigma0's
intended scope to make such decisions.

> I've also seen a paper mention that sigma1 was originally used for
> persistent storage, is that not true anymore?

Well, sort of.  If you look at:

   http://l4ka.org/publications/paper.php?docid=663

You'll see that the kernel can raise page faults on TCBs that are
unavailable or read-only (in the case of write accesses).  In this
scenario a page fault RPC is sent to the checkpointer (sigma1) which
in turn maps the TCB memory into the kernel.

The scheme described in the paper above was implemeneted as a
prototype in Hazelnut.  There has never been any sigma1 implementation
for Pistachio.  Or more importantly, Pistachio has never (yet) had
support for paging TCBs.

	eSk