B licenses

Kind Gerwin, wrote:

> Hi Jorge,
>
> Raf has a copy of his formal B model available for download at:
> http://xaph.net/x/APInov3.tgz
>
> As for B licenses: we don't really know.
>
> Raf says he would advise against B, unless you or your institute already
> have some licenses available. You can always ask the manufacturers, though.
> The main tools are Atelier B and the B Tool, I think. There is also a new
> version of B coming from the RODIN project, but I don't think Raf's
> formalisation will be compatible with that.
>
> Cheers,
> Gerwin
>

This is my response:

Hi Gerwin,

Thank you very much, Raf´s advise against B, would be great, since we dont have any licenses.

Why is it that you think that Raf's formalization wont be compatible with the B version from RODIN?, anyhow, I've seen the website: http://rodin-b-sharp.sourceforge.net/, but it seems that project stoped six months ago.

Thank you very much,

Jorge

PLEB-> Testbed for L4

So I came across with PLEB, an XSCALE single board computer designed at NICTA. They have everithing one will need to get it done, form hardware designs, til software code for BIOS and the rest. They even have one with CAN node integrated,
More info about it:
http://www.ertos.nicta.com.au/hardware/pleb/
lets see if I cant talk Jorge to get his hands on it.

where did sigmas go?

I wrote back:

This removal of sigma0 need, happens at the L4::N1 implementation or is it a very recent l4:Pistachio improvemnet?
Now I'm a little more confused than last time. When you mean that you've removed the sigma0 need, you mean that it is not a provileged thread anymore?, giving freedom of implementation for memory management, so there is no thread memory space asingment at kernel level, and that task is now performed at a user level, at same level of memory manager? which makes sense. If so, would it be better having memory manager implementations wich will do both deliver memory for threads(sigma0) and manage memory?, is your simple sigma0 implementation http://www.ertos.nicta.com.au/software/kenge/sigma0/devel/, a demo of it?.


Just as a reminder, I havent found any information about the l4::N1, I'll have to search some more.

L4 User-level reflection scheduler

I've found this article:
http://www.ertos.nicta.com.au/publications/papers/Ruocco_RTSS_06.pdf
In which Sergio Ruocoo describes his 100 loc implementation of a user-level reflection scheduler, for realtime implementations without cahnges at l4 kernel, I assume it is about a L4 Thread with the SCHEDULLER attribute set to 0, any how, there's the article, I'll write about it once I finish reding it. For now:

Computational reflection: “the activity performed by a computational system when doing computation about (and by that possibily affecting) its own state and computations”.

BenLeslie says: Sorry to tell, but sigma0 died!

Well, what can I say, unexpected answer from the kenge users list!. Friendly Ben Leslie answered about sigma1:

Hi Jorge,

We have actually removed the need for sigma1 (and sigma0). On our
latest version it does not exist.

Further e-mail about this I'll write. And about B-toolkit, he was kind enough to CC to the L4 formal method author. And about scheduler I was correct.

Few questions I have for my self, and for Ben off course.

distributed or disturbed notion of sigma0

Well, I had this project with my friend Jorge Cardona, about distributing an operative system trough a network of computers, so if you get to run a Virtual Machine on top of it, it would be transparent for the host OS, in other words a transparent cluster configuration.

How about making sigma0 distributed over a network?, in that way VM machine threads memory on top of L4 would be distributed, and then, it wouldnt be too complicated to make a thread to manage distrubuted interrups and make virtualized wombat to use such thread, thus having wombat working under multiple computers at the same time, and one could do cool things such as active-active failover OS.

Reading this B-method implementation i found this:

Sigma0 is the default system pager. Its job is to take up all possible non-kernel memory on start up, and give it out to threads as it is requested. Sigma0 is not a memory manager, and does not accept any form of request to take back (free) the memory that has once been given out. When other special threads load during the kernel loading procedure, memory is taken from sigma0. After this is done, a memory manager should take the remaining memory from sigma0 and manage it appropriately. Sigma0 gets its own address space, and is a privileged thread.

If I understand OK; in order to make it real one would have to worry aboout sigma0 and a memory manager.

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

Gernot thesis supervisor?

En el otro lado del charco, which textually translates, at the other side of the pool, is Gernot's mail user agent (MUA), and suddenly a weird mail from: jorge torres GH126: User-level scheduling in L4:

Professor Gernot Heiser,

I understand that you are a very busy person, so please receive my apologies for taking some of your time. I have seen your Thesis Topics list for undergraduate students, and I am convinced that User-level scheduling in L4 is what I want to do for my undergraduate thesis project. I have only one question: what can I do (if possible) In order for you to be my thesis Supervisor?,

Thank you very much for taking the time to read this,

Sincerely,

ME,

That was more than a week ago, so he probably wasnt interested at all, and decided to send it to the bulk mail, or to mark it as spam, since he didn't even answer something like: sorry, you are right I'm very busy.

Even if it's his idea or not, due to its under public domain, and under the freedom of choice I'm proud of having to tell, if I don't find something more interesting in L4, that will be my thesis project whether Gernot likes it or not!

B->AMN

Abstract machine notation, I meet with a friend of mine, "tocayo" Jorge Eduardo Cardona and between beers, he told me about this thing he was reading, the B-method, so it came in to my curiosity todo reading list, and as i got to talk to him tody again i remembered, I found this site:
http://www.b-core.com/aboutb_method.html
and documentation about it:
http://www.b-core.com/ONLINEDOC/Contents.html
Jorge tells me that there is this guy at NICTA who came up with the L4 microkernel implementation using the B-method:
http://cgi.cse.unsw.edu.au/%7Erafalk/pubs/b-l4-api.pdf
So having that on the table why not having a zero defect thesis, as b-core promises?

The B Method, developed by Jean-Raymond Abrial [1], is a system of formal development from the initial high-level specification all the way to implementation via a process called refinement. It is one of the few formal methods to do so. The idea is to abstract away the implementation and concentrate on pure functional requirements at the top level. Then, with each refinement step, provide more information on how exactly the system fulfils those requirements, until enough information exists to implement the system. Each refinement step requires proof of consistency with the previous step.

Rafal Kolansk

L4 thesis

I was never worried about my undergraduate thesis project, but time passes, and suddenly I found my self working as the information security officer of the biggest stock market company in Colombia, INTERBOLSA, in a job that takes almost 16 hours/day from me.
With that on the scene it is very easy to understand that my undergrad thesis is something I really need to worry about. As my family says to me: after 5 years of study, You cannot end up as a "tegua", which in my country means: some one how knows a job, but has learned in a empiric way. But that is not my consternation, I beleve teguas are people to admire. thing is I REALLY WANT to become a PhD some day, so finishing my undergraduate studies is my big MUST for this semester. That's why I've taken two decisions: QUIT INTERBOLSA, and start what at this moment is important for my life plans!.