7 ms·

Linux Kernel Modules in Haskell (2009)

90 points by tikhonj 13y ago

chas 13y ago
This is really neat, but I am very wary of building kernel modules with garbage collected languages especially ones like Haskell, which can has very difficult to reason about runtime characteristics due to laziness. One approach that I find much more promising is using Haskell (or other robust and semantically easy to reason about and easy to verify languages) to generate C code which then can be used with normal toolchains for low-level development. Galois is doing a lot of work in this area that looks very promising. One of their projects is an autopilot system called SMACCMPilot[0] that uses a Haskell eDSL called Ivory[1] to generate safe C code. I am particularly excited about its integration with FreeRTOS tasks using the Tower Language[2] (another Haskell eDSL). This makes it possible to generate code that can be reasoned about with Haskell but has the runtime characteristics of C. This is particularly interesting because embedded systems code is notoriously non-composable and difficult to reason about due to the enormous shared state of the hardware itself and the highly concurrent nature of interrupt-driven design. Embedded C makes a good target for this sort of design and analysis though, because it has very constrained memory usage (developers typically eschew dynamic allocation), very subtle potential issues (debugging race conditions with LEDs sucks), and very serious consequences for errors[3]. [0]http://smaccmpilot.org/index.html http://smaccmpilot.org/index.html [1]http://smaccmpilot.org/languages/ivory-introduction.html http://smaccmpilot.org/languages/ivory-introduction.html [2]http://smaccmpilot.org/languages/tower-overview.html http://smaccmpilot.org/languages/tower-overview.html [3]http://en.wikipedia.org/wiki/Therac-25 http://en.wikipedia.org/wiki/Therac-25
- DanWaterworth 13y ago
  Galois are doing lots of interesting things in this space, including HaLVM, which allows you to write Haskell programs that run without an OS [1] [1] http://corp.galois.com/halvm http://corp.galois.com/halvm
  - chas 13y ago
    Absolutely! I am very interested by their approach in this area because integration with existing infrastructure is essential for practical work in this area, but reasoning about existing infrastructure is a lot harder than it needs to be. This is a relatively old presentation of theirs, but it has a decent overview of what they have used Haskell for. http://www.cse.chalmers.se/edu/year/2010/course/TDA555/Material/Guest1/magnus.pdf http://www.cse.chalmers.se/edu/year/2010/course/TDA555/Mater...
- perlgeek 13y ago
  But if you generate C code from Haskell, don't you have the same problem as before that it's difficult to reason about runtime characteristics due to laziness?
  - chas 13y ago
    Not really. Haskell is basically used as a compiler from a DSL to C. Compilers running on general purpose systems are much less sensitive to timing and memory use than embedded systems and kernel drivers, so it isn't that big of a deal. The generated C code is the only thing that executes on the target device so you get the same performance that you would expect from C code.
  - freyrs3 13y ago
    The emitted code need not be lazy, and most often isn't. To a lesser extent the EDSL technique is also the technique that Accelerate uses to build fast array computations. [1]: https://speakerdeck.com/mchakravarty/embedded-languages-for-high-performance-computing-in-haskell https://speakerdeck.com/mchakravarty/embedded-languages-for-...
- chongli 13y ago
  This is really neat, but I am very wary of building kernel modules with garbage collected languages especially ones like Haskell, which can has very difficult to reason about runtime characteristics due to laziness. This is FUD, repeated ad nauseum all over the internet as a misinterpretation of what Simon Peyton Jones said once during a talk. In case you hadn't noticed, there appears to be a tradition in programmer circles of picking SPJ quotes and turning them into memes. "Haskell is useless!" and "Avoid success at all costs!" are some others. The reality is far less extreme than most people think. It is not at all unreasonable to write low-level code such as device drivers in Haskell. This has actually been done as part of the HaLVM project.
  - mestonlawest 13y ago
    SPJ is a fool for making those 'clever' statements like "Haskell is useless!", because most people won't stick around to hear the twist explanation.
    - freyrs3 13y ago
      I think you have it backwards. If someone forms opinions on languages based on out of context quotations then they are the fool, not SPJ.
    - phaer 13y ago
      The explanation of this particular quote is like 5 minutes long on YouTube. If you don't spend that much time to listen to an argument, it's unlikely that you have a well founded opinion on programming languages anyway.
    - efnx 13y ago
      I don't think at the time he was trying to be clever. If you watch the talk you'll see it makes a lot of sense to make this statement in its context. Also - Haskell will either be very popular or not, based on its merits in industry. I doubt the fallout from these type of statements will amount to much in the long run.
  - cwzwarich 13y ago
- pjmlp 13y ago
  > This is really neat, but I am very wary of building kernel modules with garbage collected languages Native Oberon, Spin, Singularity, ...
taeric 13y ago
This is incredibly neat and I do not at all mean to discourage the development of more tools. However, is this really that much more capable than considering all of the other tooling that can help in writing a kernel module in C? That is, you have more than just the C compiler at your disposal nowdays. Valgrind and such. Simply put, how much more capable is this? Certainly more concise and has some aesthetic appeal. Just curious if it brings a lot more to the table.
- Peaker 13y ago
  One of the main uses of valgrind is to discover undefined behavior. Haskell doesn't have undefined behavior, so you don't need it. I don't think the C tooling is that great. Haskell has some neat tooling of its own.
  - taeric 13y ago
    I think you are misrepresenting valgrind some. Just going by the bullet list on their homepage, they do more than just undefined. Offering fairly nice analysis at the cache level. Also, has support for finding threading errors. Note, this isn't just a "do mutexes work" sort of thing, but offers analysis that shared memory is safely shared. (And, from my understanding, this doesn't require modification of the code to make it slower/larger.) So, this really doesn't answer my question. I can't but agree that the tooling in Haskell is above that of plain C. However, what class of bugs will be prevented in the kernel, that isn't already fairly well handled with existing tooling. Consider that the kernel is actually fairly solid code, if I'm not off my rocker.
    - codygman 13y ago
      Wouldn't "class of bugs prevented by tooling" not be quite as good as "class of bugs disallowed by programming language"?
      - agentultra 13y ago
        You might end up in the trap of only writing correct bugs.
ZirconCode 13y ago
I'm waiting for Ruby. Or JavaScript. It's going to happen some day. This reminds me a lot of xmonad. I guess higher level languages are migrating downwards to the system level slowly.
- tmhedberg 13y ago
  It seems like kernel-space code would be one of the worst possible environments in which to use a dynamic language. A runtime error in that context can easily bring down the entire system; you're really better off sticking to languages with at least a semblance of static safety. Haskell may be a high-level language, but it's also a significant improvement over C when it comes to compile-time safety, unlike Ruby and JavaScript, which have none at all.
  - regularfry 13y ago
    The Lisp Machines would seem to be the counterpoint to that point of view.
  - mokus 13y ago
    The difference between catching types at runtime or compile time is much less important than the common feature of catching type errors at all. A runtime type error in C simply trashes another subsystem's data. A runtime type error in Python or Ruby is caught, so can theoretically be prevented from cratering the entire system. Sure, I (as a heavy Haskell user) would rather catch such things at compile time, but given the choice between catching them at runtime and not catching them at all, I'd almost never choose the latter unless there are other overriding concerns.
    - hderms 13y ago
      C compilers catch plenty of type errors. As soon as you start casting things into different types you have the possibility of re-introducing type errors, but presumably you're casting things for a good reason in the first place, and therefore understand the tradeoff.
- 13y ago
tspradeepkumar 13y ago
LKM in Haskell is something i was searching for. But in my Linux system, its gives me error and in fedora i compiled it successfully, but there was some memory issue....while doing it in ubuntu... nyway will another time....
S4M 13y ago
Slightly OT, but does someone has an introduction on how to build a minimal kernel for people who have absolutely no clue on how this works?
- maaku 13y ago
  Get the Minix book: http://www.amazon.com/Operating-Systems-Design-Implementation-Edition/dp/0131429388 http://www.amazon.com/Operating-Systems-Design-Implementatio...
- fotcorn 13y ago
  http://wiki.osdev.org/Main_Page http://wiki.osdev.org/Main_Page is very good. My own kernel (https://github.com/fotcorn/kernel https://github.com/fotcorn/kernel) is hacked together with code from osdev.org.
- Sodel 13y ago
  This tutorial fits the bill, and it's not too long. I worked through it when I was first learning C. http://www.osdever.net/bkerndev/Docs/intro.htm http://www.osdever.net/bkerndev/Docs/intro.htm

90 points by tikhonj 13y ago

chas 13y ago

This is really neat, but I am very wary of building kernel modules with garbage collected languages especially ones like Haskell, which can has very difficult to reason about runtime characteristics due to laziness. One approach that I find much more promising is using Haskell (or other robust and semantically easy to reason about and easy to verify languages) to generate C code which then can be used with normal toolchains for low-level development. Galois is doing a lot of work in this area that looks very promising. One of their projects is an autopilot system called SMACCMPilot[0] that uses a Haskell eDSL called Ivory[1] to generate safe C code. I am particularly excited about its integration with FreeRTOS tasks using the Tower Language[2] (another Haskell eDSL). This makes it possible to generate code that can be reasoned about with Haskell but has the runtime characteristics of C. This is particularly interesting because embedded systems code is notoriously non-composable and difficult to reason about due to the enormous shared state of the hardware itself and the highly concurrent nature of interrupt-driven design. Embedded C makes a good target for this sort of design and analysis though, because it has very constrained memory usage (developers typically eschew dynamic allocation), very subtle potential issues (debugging race conditions with LEDs sucks), and very serious consequences for errors[3]. [0]http://smaccmpilot.org/index.html http://smaccmpilot.org/index.html [1]http://smaccmpilot.org/languages/ivory-introduction.html http://smaccmpilot.org/languages/ivory-introduction.html [2]http://smaccmpilot.org/languages/tower-overview.html http://smaccmpilot.org/languages/tower-overview.html [3]http://en.wikipedia.org/wiki/Therac-25 http://en.wikipedia.org/wiki/Therac-25

DanWaterworth 13y ago
Galois are doing lots of interesting things in this space, including HaLVM, which allows you to write Haskell programs that run without an OS [1] [1] http://corp.galois.com/halvm http://corp.galois.com/halvm
- chas 13y ago
  Absolutely! I am very interested by their approach in this area because integration with existing infrastructure is essential for practical work in this area, but reasoning about existing infrastructure is a lot harder than it needs to be. This is a relatively old presentation of theirs, but it has a decent overview of what they have used Haskell for. http://www.cse.chalmers.se/edu/year/2010/course/TDA555/Material/Guest1/magnus.pdf http://www.cse.chalmers.se/edu/year/2010/course/TDA555/Mater...
perlgeek 13y ago
But if you generate C code from Haskell, don't you have the same problem as before that it's difficult to reason about runtime characteristics due to laziness?
- chas 13y ago
  Not really. Haskell is basically used as a compiler from a DSL to C. Compilers running on general purpose systems are much less sensitive to timing and memory use than embedded systems and kernel drivers, so it isn't that big of a deal. The generated C code is the only thing that executes on the target device so you get the same performance that you would expect from C code.
- freyrs3 13y ago
  The emitted code need not be lazy, and most often isn't. To a lesser extent the EDSL technique is also the technique that Accelerate uses to build fast array computations. [1]: https://speakerdeck.com/mchakravarty/embedded-languages-for-high-performance-computing-in-haskell https://speakerdeck.com/mchakravarty/embedded-languages-for-...
chongli 13y ago
This is really neat, but I am very wary of building kernel modules with garbage collected languages especially ones like Haskell, which can has very difficult to reason about runtime characteristics due to laziness. This is FUD, repeated ad nauseum all over the internet as a misinterpretation of what Simon Peyton Jones said once during a talk. In case you hadn't noticed, there appears to be a tradition in programmer circles of picking SPJ quotes and turning them into memes. "Haskell is useless!" and "Avoid success at all costs!" are some others. The reality is far less extreme than most people think. It is not at all unreasonable to write low-level code such as device drivers in Haskell. This has actually been done as part of the HaLVM project.
- mestonlawest 13y ago
  SPJ is a fool for making those 'clever' statements like "Haskell is useless!", because most people won't stick around to hear the twist explanation.
  - freyrs3 13y ago
    I think you have it backwards. If someone forms opinions on languages based on out of context quotations then they are the fool, not SPJ.
  - phaer 13y ago
    The explanation of this particular quote is like 5 minutes long on YouTube. If you don't spend that much time to listen to an argument, it's unlikely that you have a well founded opinion on programming languages anyway.
  - efnx 13y ago
    I don't think at the time he was trying to be clever. If you watch the talk you'll see it makes a lot of sense to make this statement in its context. Also - Haskell will either be very popular or not, based on its merits in industry. I doubt the fallout from these type of statements will amount to much in the long run.
- cwzwarich 13y ago
pjmlp 13y ago
> This is really neat, but I am very wary of building kernel modules with garbage collected languages Native Oberon, Spin, Singularity, ...

taeric 13y ago

This is incredibly neat and I do not at all mean to discourage the development of more tools. However, is this really that much more capable than considering all of the other tooling that can help in writing a kernel module in C? That is, you have more than just the C compiler at your disposal nowdays. Valgrind and such. Simply put, how much more capable is this? Certainly more concise and has some aesthetic appeal. Just curious if it brings a lot more to the table.

Peaker 13y ago
One of the main uses of valgrind is to discover undefined behavior. Haskell doesn't have undefined behavior, so you don't need it. I don't think the C tooling is that great. Haskell has some neat tooling of its own.
- taeric 13y ago
  I think you are misrepresenting valgrind some. Just going by the bullet list on their homepage, they do more than just undefined. Offering fairly nice analysis at the cache level. Also, has support for finding threading errors. Note, this isn't just a "do mutexes work" sort of thing, but offers analysis that shared memory is safely shared. (And, from my understanding, this doesn't require modification of the code to make it slower/larger.) So, this really doesn't answer my question. I can't but agree that the tooling in Haskell is above that of plain C. However, what class of bugs will be prevented in the kernel, that isn't already fairly well handled with existing tooling. Consider that the kernel is actually fairly solid code, if I'm not off my rocker.
  - codygman 13y ago
    Wouldn't "class of bugs prevented by tooling" not be quite as good as "class of bugs disallowed by programming language"?
    - agentultra 13y ago
      You might end up in the trap of only writing correct bugs.

ZirconCode 13y ago

I'm waiting for Ruby. Or JavaScript. It's going to happen some day. This reminds me a lot of xmonad. I guess higher level languages are migrating downwards to the system level slowly.

tmhedberg 13y ago
It seems like kernel-space code would be one of the worst possible environments in which to use a dynamic language. A runtime error in that context can easily bring down the entire system; you're really better off sticking to languages with at least a semblance of static safety. Haskell may be a high-level language, but it's also a significant improvement over C when it comes to compile-time safety, unlike Ruby and JavaScript, which have none at all.
- regularfry 13y ago
  The Lisp Machines would seem to be the counterpoint to that point of view.
- mokus 13y ago
  The difference between catching types at runtime or compile time is much less important than the common feature of catching type errors at all. A runtime type error in C simply trashes another subsystem's data. A runtime type error in Python or Ruby is caught, so can theoretically be prevented from cratering the entire system. Sure, I (as a heavy Haskell user) would rather catch such things at compile time, but given the choice between catching them at runtime and not catching them at all, I'd almost never choose the latter unless there are other overriding concerns.
  - hderms 13y ago
    C compilers catch plenty of type errors. As soon as you start casting things into different types you have the possibility of re-introducing type errors, but presumably you're casting things for a good reason in the first place, and therefore understand the tradeoff.
13y ago

tspradeepkumar 13y ago

LKM in Haskell is something i was searching for. But in my Linux system, its gives me error and in fedora i compiled it successfully, but there was some memory issue....while doing it in ubuntu... nyway will another time....

S4M 13y ago

Slightly OT, but does someone has an introduction on how to build a minimal kernel for people who have absolutely no clue on how this works?

maaku 13y ago
Get the Minix book: http://www.amazon.com/Operating-Systems-Design-Implementation-Edition/dp/0131429388 http://www.amazon.com/Operating-Systems-Design-Implementatio...
fotcorn 13y ago
http://wiki.osdev.org/Main_Page http://wiki.osdev.org/Main_Page is very good. My own kernel (https://github.com/fotcorn/kernel https://github.com/fotcorn/kernel) is hacked together with code from osdev.org.
Sodel 13y ago
This tutorial fits the bill, and it's not too long. I worked through it when I was first learning C. http://www.osdever.net/bkerndev/Docs/intro.htm http://www.osdever.net/bkerndev/Docs/intro.htm