echo mailto kenge-users >> /dev/null ??

I DONT know why, every time I write to the kenge-users list I dont get any answers, this time I worte about some questions I had.

to: kenge-users@ertos.nicta.com.au
Subject: sigma1 and L4 formal model

Hi you all,

I'm confused about what sigma1 is for?, I've found that it is about task persistency, but still it isn't clear to me, is it an atempt of having a swap memory manager?

Another question, is there any CVS for the Rafal Kolanski formal description of L4 using the B-method?, are there any kind of B-toolkit research licences, for thesis projects, I want to use it for a formal model of L4 scheduler so that a privileged thread such as sigma0 but for handling time interrupts which will IPC to a user space thread in which schedulling dessisions will be taken.

I understand that the internal scheduler is not a thread it self, it is just a function that chooses next thread to execute based on scheduller attribute.

Thank you very much,


Jorge