History log of /seL4-l4v-10.1.1/HOL4/src/experimental-kernel/Net.sig
Revision Date Author Comments
# 32bf1e49 02-Feb-2015 Piotr Trojanek <piotr.trojanek@gmail.com>

extra semicolons removed from (some) .sig files


# cf9c1e78 24-Oct-2014 Piotr Trojanek <piotr.trojanek@gmail.com>

correct indent (3 spaces) of documentation in .sig files


# 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.