Kinetic: Greetings, Redditors

Much to my surprise, Kinetic was linked to from the Programming sub-Reddit today.

In the past couple of days, Kinetic has suddenly drawn some attention. The feedback has been encouraging, but a few themes have come up in the questions people have asked. So here’s a few comments that might clear things up a bit:

  1. I hadn’t really intended for Kinetic to get much review; I had created the website merely so my friends could see what I was up to. In other words, the statements aren’t meant to be taken too seriously: this isn’t an academic journal, it’s a personal website.
  2. Kinetic uses the Foreign Function Interface to interact with C++ and Assembler. In general, the FFI enables pointer arithmetic, and is therefore able to subvert type safety. I haven’t yet come up with a better way for addressing a graphics adapter’s linear frame buffer. I’m sincerely interested in suggestions for how to deal with that.
  3. Nope, I haven’t posted any code yet. I’m not opposed to the idea of releasing snapshots in the future, when things are a bit more mature.
  4. There has been speculation as to how much of the operating system is written in Haskell. Here’s a rough breakdown. C++: Stuff for initializing the IDT and GDT, some bitmap routines (for performance), the FreeType library, as well as basic functions for supporting the GHC runtime. Haskell: PCI driver, mouse and keyboard driver, VMWare graphics adapter driver, most of the GUI.

Hope that helps to clarify a few things.

About these ads
Next Post
Leave a comment

8 Comments

  1. Gwern

     /  4 September, 2007

    “I haven’t yet come up with a better way for addressing a graphics adapter’s linear frame buffer. I’m sincerely interested in suggestions for how to deal with that.”

    You could treat it as an array, I think, and then use low-level functions to modify it. With proper type-checking, you could even have assurances you wouldn’t be going out of bounds. (, , and that sort of thing.)

  2. This is what I do right now. The trouble is that this is more or less an “honor code” solution — we could use information hiding to ensure that no one else has access to the pointer, but this doesn’t help us with the larger issue of ensuring the accessor genuinely respects the bounds.

    Ultimately, the size of the frame buffer (aka the array) is determined by the graphics resolution. This must remain in sync with the accessor function in order for type safety to be preserved.

    Now, I’m not especially bothered by this — in every trusted system, some things will have to be taken as “fundamental” — but it’s true that this is just one example of where this type of thing will take place in the kernel.

    I don’t know anything about type systems, but I’ve heard words like “dependent types” used within this context. But now we’re well outside the domain of maths that I know anything about :)

  3. Joseph Huang

     /  5 September, 2007

    Yes, dependent types are where it’s at. Check out epigram.

    BTW, try reading the exokernel papers if you’re interested in operating systems. Also read up on E, EROS and capability based security. You seem to be trying to do monad based security, which is probably much harder. And also check out uniqueness types, as an alternative to monads for I/O.

  4. guest

     /  5 September, 2007

    How about using Hash for the shell?
    Or atleast as the basis.

  5. Andy

     /  24 September, 2007

    Hi!

    Great to see your project! I really like the idea of Haskell being used for an OS. It seems to be particularly well-suited to the security side of things, that’s for sure.

    I thought I’d mention what may be a useful site for you (with what looks like some very cool Haskell code). Here it is –
    http://okmij.org/ftp/Computation/Continuations.html#zipper

    Look for the section called “Zipper-based file server/OS” – it sounds very cool. Oh, and by the way, all code on that site is public-domain (unless otherwise specified) – I’m pretty sure the above code is P.D.

    I was wondering – are you looking at releasing the code for Kinetic as public-domain (when it is released)? Would be awesome if that’s the case! Bye for now –
    - Andy

  6. “I was wondering – are you looking at releasing the code for Kinetic as public-domain (when it is released)?”

    I’m intending to do a code release once the source matures up a bit. As it stands, it’s going through some heavy refactoring, so it’s not really in a working state right now.

    This will probably take some time, though. I’m entering a very busy academic year, so it’s unlikely that there will be much motion on the project until December break.

    Zipper sounds really neat — I’m definitely going to take a deeper look at it later this week.

  7. Mark Bradley

     /  3 October, 2007

    Hi Tim,

    I’m posting to see if you can send me an email (neeja [dot] h [at] gmail [dot] com) regarding Kinetic, there are a few details I want to get. Mostly about you since I will be citing your work in my thesis if that is okay.

    -Markb

  1. Top Posts « WordPress.com

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: