History log of /seL4-l4v-master/HOL4/src/experimental-kernel/Net.sml
Revision Date Author Comments
# fd1efab9 31-Jul-2010 Tjark Weber <Tjark.Weber@cl.cam.ac.uk>

Removed Lib.gather. Use {Lib,List}.filter instead.


# fb840c11 13-Dec-2002 Michael Norrish <Michael.Norrish@nicta.com.au>

Thanks to an enlightened Internet cafe in Perth running DHCP, I can
finally check this in. It's a name-carrying implementation of the
kernel, and should be a drop-in replacement for the existing code.
To make the replacement change src/0 in tools/build.sml to be
src/experimental-kernel.
Sadly, the code is not as fast as I'd like just yet. In particular,
the benchmark example is 20% slower. I don't know quite why this
should be, but I'm looking into it. The performance of the checked-in
code will be even worse than it should be at the moment because I've
used Profile-ing throughout. (The most called (potentially expensive)
function in the kernel? Term.compare it seems.) This profiling seems
to cause a strange Time exception on big builds, which has stopped me
testing the new code on the netsem examples (which are 90% of the
motivation for the change---argh).
Anyway, if anyone feels the urge to fix obvious bugs, please feel
free. Though access to the 'net for my Linux partition is a tad on
the tedious side, I can read my e-mail at home, and this means that I
can see messages to hol-checkins without any difficulties.