Linux Kernel Modules in Haskell (2009) | Hacker News Reader

Linux Kernel Modules in Haskell (2009)

tommd.wordpress.com

90 pointstikhonj48 comments

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

[1]http://smaccmpilot.org/languages/ivory-introduction.html

[2]http://smaccmpilot.org/languages/tower-overview.html

[3]http://en.wikipedia.org/wiki/Therac-25

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.

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

I think you have this backwards. People have been saying that laziness has unpredictable performance characteristics (especially when it comes to space usage) as long as there have been lazy functional languages. SPJ was referring to that common sentiment; it didn't somehow materialize because of comment he made during a talk.

There was an era where space complexity and space usage semantics were a big deal in functional programming, e.g. the work on giving a precise definition of "tail call optimization" and the emphasis on space safety that has since been present in the strict functional programming world. In contrast, there is no standard space semantics for lazy languages, and certainly none that GHC respects. It's tricky when simple CSE can dramatically alter the space complexity of your program, e.g.

https://ghc.haskell.org/trac/ghc/ticket/947 https://ghc.haskell.org/trac/ghc/ticket/1752

I didn't say there wasn't any difficulty, I said it was FUD. It is true that there is more mental overhead in reasoning about space usage in a lazy language. It is not true that this is unpredictable. If that were the case, it would be a complete crapshoot for people to write code in a lazy language. Luckily, a basic understanding of Haskell's evaluation model gives one the ability to predict space usage and know reliably what sort of anti-patterns to avoid (such as the infamous lazy foldl).

The problem with FUD is that it takes reasonable statements and exaggerates them to an unreasonable degree. People repeat the word "difficult", eventually someone starts using "very difficult", sooner or later people start throwing around "impossible".

It's not just the evaluation model; you have to know whether the compiler will perform transformations behind your back that increase space usage. If you were to impose a space semantics on the compiler and require that it preserve the semantics, a lot of optimizations would have to be disabled for lazy expressions.

It's not surprising that people manage to produce lots of working programs despite this, though. Almost all life-critical software is written in completely unsafe languages.

the compiler will perform transformations behind your back that increase space usage

This is not exclusive to Haskell; even C compilers will do this with jump tables and so on.

Jump tables don't increase asymptotic space complexity, whereas some of GHC's optimizations will. You can also see how much jump tables increased the space usage of your program by inspecting the size of the compiled binary.

I'm not proficient in Haskell, just a bystander, but this isn't the sentiment I get from reading Neil Mitchell's posts on the subject:

http://queue.acm.org/detail.cfm?id=2538488

http://neilmitchell.blogspot.com/2013/02/chasing-space-leak-...

He appears to use profiling tools and "try them all and see which produces the most useful information", to me that sounds very different from reasoning.

Try this:

http://blog.ezyang.com/2011/05/anatomy-of-a-thunk-leak/

and particularly this:

http://blog.ezyang.com/2011/05/an-insufficiently-lazy-map/

One point I'd like to mention: just because it seems complex and intimidating for beginners/outsiders does not mean it is intractable for experienced programmers.

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.

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.

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.

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.

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

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/Mater...

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?

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.

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

> This is really neat, but I am very wary of building kernel modules with garbage collected languages

Native Oberon, Spin, Singularity, ...

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.

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.

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.

Wouldn't "class of bugs prevented by tooling" not be quite as good as "class of bugs disallowed by programming language"?

The problem is that, from a pragmatic perspective, you have to balance the benefits of a safer language and the cost of "explaining" to it that what you're doing is safe. If you want to make it accept a particular construct as "safe", you have to feed it with a lot more information, whereas in a more permissive language you can just be imperative and tell it "I know it's ok, just do it". The tooling approach is, it seems, more attractive because it adds a bit of safety at a moderate cost.

The tooling approach is, it seems, more attractive because it adds a bit of safety at a moderate cost.

There's one cost you've ignored: feedback time. A type-checker can be run on the fly with tools such as flymake. Debugging tools and tests are (orders of magnitude) slower to run and thus dramatically slow down the feedback cycle between bug detection and bug fix. This is especially prevalent when doing major refactoring work and the code is a long way from working again.

I guess I'm different in that I prefer to have a substantial amount of safety with "safe" code. If it's something that doesn't require that safety, it seems that something truly dynamic like lisp or racket is best.

For intstance, languages with weak static typing seem to lead to "stringly typed" solutions.

Right, which is why I was asking which class of bugs are we talking about. If "undefined" is the only class that this would remove, it sounds less than compelling. Especially if it in any way impedes considering the logic of what is actually getting done. (I mean, correct me if I'm wrong and "undefined" is actually a large part of the problems that afflict writing code for the kernel.)

You might end up in the trap of only writing correct bugs.

Correct bugs, logic errors I'm assuming, are a better problem to have than logic errors + undefined behavior in my opinion.

Undefined behavior is a perfectly acceptable abstraction [1].

The C specification is pretty clear on what it has purposefully left undefined which has made it rather resilient to changes in underlying hardware architectures.

Must be why Haskell's run-time support is written in C [2]

[1] http://thoughtmesh.net/publish/367.php [2] https://github.com/ghc/ghc/tree/master/rts

Undefined behavior has advantages, of course. The C language is excellent at certain things, too.

However, not every kernel driver and not every application needs the benefit of C or undefined behavior.

The fact that Haskell's RTS is written in C is evidence that the kind of code in RTS's has more to gain from C than from Haskell. Some parts of drivers might also be best written in C.

I will have to check that video out. I'm aware that Haskell's run-time support is written in C and I don't believe that is a mistake.

Right tool for the job after all. For many use cases in my experience though, you don't want undefined behavior.

With rich types, you can get rid of the correct bugs, too.

You can encode an arbitrary amount of information into a verified, proven specification.

The specification is orders of magnitude smaller and simpler than the actual code, so much easier to get correct.

I've heard that before.

"Proven," in as far as you trust the axioms and assumptions made by the Haskell compiler. It's an important distinction because you must assume that the 50k lines of C code that get compiled and statically linked into your Haskell programs is also, "correct," by extension despite it living outside the set of axioms and assumptions your program has been proven within.

Don't get me wrong, Haskell is a neat language, I just don't accept its trade-offs for most of the work I do.

That's certainly a valid opinion, but I believe you may be doing yourself a disservice by not trying to use Haskell in some of that work you do. However I can't say that for sure yet, I'm still evaluating how useful Haskell is for me in my "real world" tasks.

Thus far I've been able to accomplish things rather easily, but I don't believe I've written enough to form a solid opinion yet.

As far as the Haskell compiler living outside of that set of axioms and assumptions my program has been proven with, that is something that does needle me a little but it seems to be a smaller hole than most languages are working with.

Sure, you'll hit an underlying platform bug, once in a few years, whether in the RTS or the OS..

But you'll prevent orders of magnitude more bugs that would waste your time debugging in the best case, or hit production in a slightly worse case.

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

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.

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.

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.

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.

The Lisp Machines would seem to be the counterpoint to that point of view.

NetBSD supports Lua in the kernel

It won't because there is next to zero benefit in doing so, while it would have a significant cost. Besides, system programming and application programming are very different domains, that attract very different programmers. Just look at the date on the article, and do a quick search on this topic. You'll see that there is no follow-up.

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?

http://wiki.osdev.org/Main_Page is very good.

My own kernel (https://github.com/fotcorn/kernel) is hacked together with code from osdev.org.

Get the Minix book:

http://www.amazon.com/Operating-Systems-Design-Implementatio...

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

Reply on news.ycombinator.com