This one seems to have dropped off the radar, sorry. On 01.08.2014, at 3:07 am, Prashanth Mundkur wrote:

These seem to be missing from the system documentation, especially on how to use it with qemu. I've built the simulator, but am unsure how to use it. The build generates a libHSSEL4-0.3.a, but I can't find an executable anywhere.

Will try to dig out the old qemu interface the library hooks up to. To be honest, this hasn’t actually been run in a long time, because it’s now easier to just run the C kernel. Initialisation code might have bitrotted quite a bit. The Haskell kernel is still used as an intermediate step in the proof, though, which doesn’t talk about initialisation (hence the potential for that part being outdated).

Also, the simulator manual says it is out-of-date, but the manual seems to include the Haskell literate sources directly. It also says the Haskell code is kept up-to-date. That sounds a bit contradictory. Are the comments in the sources that obsolete?

Yes, the comments and introduction are out of date, the code is kept in sync because it is needed in the proof. Cheers, Gerwin ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.