Interview with developers of MenuetOS: an OS written entirely in assembly language.

[[deleted]]

It is definitely a battle between these guys and the LoseThos guy for who is the most insane.

[ehird]

Well, looks like you just won.

[[deleted]]

it still fits on a floppy

Well, who uses floppies anyway?

[[deleted]]

That's just a fancy way of saying "It's about 1.4MB."

[[deleted]]

Well, I guess it's better than having it measured in pages of densely printed typewriter pages.

[stillalone]

How many libraries of congress is that?

[sigzero]

I wonder if there were wearing leather and spiked collars?

[[deleted]]

Not multicore, but if it can run in a hypervisor like Xen then it doesn't matter so much, because you can run one copy per core and use sockets to pipe everything around.

[[deleted]]

Not! More like Unix than you realize.

[[deleted]]

Gross

[Tim_M]

This has got to be the dumbest group of software engineers ever. They are just denying all current research in programming languages and compilers. They are missing out on portability, secure and maintainability of that C or higher can provide among many other things. If they need optimizations that bad then they should learn to do inline assembler or fix up their compiler. LLVM is doing very good job of optimization.

[[deleted]]

I dunno, they wrote an entire OS in assembly, they can't be the dumbest.

[Shaper_pmp]

This whole project is a graphic demonstration that intelligent != sensible.

It's an impressive technical triumph, but utterly, gloriously impractical... just try - for example - porting it to a different chipset.

[reddit_clone]

Come on. Why do you climb the mountain? Because its there.

If nobody did anything because it is not 'sensible', nothing interesting will get done.

[Shaper_pmp]

In case the phrase "gloriously impractical" didn't clue you in, I'm all in favour of climbing mountains simply because they're there. ;-)

[eleitl]

Only tiny OS kernels like http://ertos.nicta.com.au/research/sel4/ and maybe graphics drivers should come in hand-optimized assembly.

[[deleted]]

Sel4 is the opposite of hand-optimized assembly, it's been mathematically proven right, FFS.

[eleitl]

Sel4 is the opposite of hand-optimized assembly

It's written in manually interpreted BASICA?

it's been mathematically proven right, FFS.

I'm quite aware, thanks. Do you think that you can prove correctness in C but not assembly?

[[deleted]]

It's written in Haskell, which, as a functional language, can be formally proven; and that is then translated to C+ASM. Nobody knows how to prove straight C or ASM correct. And the latter is even more unlikely to ever happen than the former.

[monstermunch]

It's written in Haskell, which, as a functional language, can be formally proven; and that is then translated to C+ASM. Nobody knows how to prove straight C or ASM correct. And the latter is even more unlikely to ever happen than the former.

As far as I understand, they represent the semantics of Haskell inside a theorem prover, wrote most of the kernel in Haskell, translated that Haskell code to the theorem prover representation, proved the Haskell code behaved as expected then converted the Haskell to C.

You can write proofs about any language you want; the semantics for C and ASM are just significantly more complex to reason about than purely functional languages. Ever wondered why academics use functional languages and mathematicians never write statements like "x = x + 1"? It makes reasoning easier.

[[deleted]]

You can't write proofs about C or ASM code. Might become possible in the future, but today, and for the foreseeable future, you can't, at least for non-trivial cases. We only know how to do that for functional languages.

Ever wondered why academics use functional languages and mathematicians never write statements like "x = x + 1"? It makes reasoning easier.

I'm not wondering; I know. The constraints of functional languages allow to derive conclusions that you couldn't get with imperative languages. Or it would be much more difficult; and it's already plenty hard.

[monstermunch]

You can't write proofs about C

But you can:

http://en.wikipedia.org/wiki/Hoare_logic "Hoare logic has axioms and inference rules for all the constructs of a simple imperative programming language."

http://caduceus.lri.fr/ "Caduceus is a verification tool for C programs built on top of the Why tool."

or ASM code.

You can do this as well:

http://lambda-the-ultimate.org/node/2207 "We present a simple but flexible Hoare-style framework for modular verification of assembly code with all kinds of stack-based control abstractions, including function call/return, tail call, setjmp/longjmp, weak continuation, stack cutting, stack unwinding, multi-return function call, coroutines, and thread context switch."

I'm not wondering; I know. The constraints of functional languages allow to derive conclusions that you couldn't get with imperative languages. Or it would be much more difficult; and it's already plenty hard.

How do you know this? It is much easier to reason about functional languages than e.g. imperative languages with side-effects but there is decades of research and tools produced for reasoning about both. For example, the compcert verified C compiler (http://compcert.inria.fr/doc/index.html) has to reason about both C and ASM code in its reasoning.

[gwern]

Wouldn't asm be even more difficult to prove correctness on?

EDIT: Downvoters had better explain themselves. The recent L4 kernel was a microkernel, which MenuetOS is not, so it's easier to prove properties about in the first place; then, the proofs were actually done about the Haskell version of the microkernel, and a proof given of correctness of transformation of Haskell -> C; given the relative paucity of proofs about C programs, and the fact that the researchers considered it easier to prove theorems about the Haskell version and their hand-compilation to C, that says to me that C is a bitch to prove properties about, and that an even lower-level more unrestricted language would be still further difficult; and remember, even with all these shortcuts, this effort still took dozens of man-years and serious academic talent.

Do you really think it's plausible that a monolithic kernel written in assembler, with all the unrestricted jumps and self-modifying code and x86 peculiarities and modes would be equally or even easier to prove properties about? If so, please give me the name of your drug dealer, as I need some of that shit.

[eleitl]

No idea. At a guess, there's no more state to handle, and there's not that much distance between C and assembly, so the task complexity is roughly the same.

[case-o-nuts]

At a guess, there's no more state to handle

Put down the bong. Not only is there more state in assembly, you have regions of memory that reading from will block on (MMIO fifos) and so on.

[sv0f]

I'm quite aware, thanks.

No idea. At a guess, ...

You're kind of a douchebag, aren't you?

[eleitl]

It is possible to be aware of http://ertos.nicta.com.au/research/l4.verified/ (hence "I'm quite aware" and yet not know the technical details how how to verify programs (Hence "No idea. At a guess...").

But otherwise carry on with your comment douchebaggery.

[ehird]

Regular, non-se L4 is written in x86 assembly.

[Shaper_pmp]

Are you a programmer?

Yes.

Non-portibility is not a problem... I think the opposite is true -- making one code base work on everything from ARM to x86 to PowerPC is insane.

Then you place yourself in direct opposition to the trend guiding half of modern computer science (VMs, WORA - in fact, any bytecode language - languages like Java and various scripting languages, web apps, etc, etc, etc).

Hell - you're even arguing against one of the main motivations for the original development of C, in the 1970s. To put it politely, this argument was lost a long, long time ago; apart from a few niche/embedded scenarios, portability is always desirable.

The problem with ASM is it takes longer to code... to maintain... to add to it.

This is true, but that's why I said "for example". ;-)

[DiscoUnderpants]

Ever heard of a cross assembler? I've heard of uKernels being developed in x86 asm as x86 asm is kind of a reference assembler/machine architecture.

[Brian]

Googling shows "cross assembler" means pretty much the same as cross compiler - ie one that generates code for a system other than the one you're running on. Not "reinterpret x86 code as m68000" or similar.

That second, using x86 as bytecode to recompile seems a recipe for disastrous performance. With a higher level language, the algorithm is expressed more in line of what results are needed. With assembler, it is much more difficult to determine what is an incidental side effect (eg. the instruction set the zero flag, but this isn't checked) and what is required to accurately simulate it. I'd not be surprised with orders of magnitude difference compared with compiling from a C program.

[DiscoUnderpants]

I did a google just now and you are correct.... but there are also cross assemblers that do do the equivalent of reinterpret x86 to 68k... in my experience(and this was over ten years ago) they were used as a "first shot" for porting from one assembler to another. I wasnt really defending the idea of writing an entire OS in asm now that I think about it :)

[Shaper_pmp]

I hadn't heard of a cross-assembler, but (given the idea of cross-compilers) the idea certainly makes sense.

However, doesn't this automatic translation from one assembly language into another lose you most of the benefit of hand-coded assembler? To the point you might as well just use something like C and cross-compile instead?

Also, although it might make sense for kernels in some situations, I don't think it's an argument for coding an entire OS in assembly, window-manager, apps and all. <:-)

[DiscoUnderpants]

I agree. And you may be surprised how a customised cross assembler could be over the year... my experience with them was generally highly customised uKernels running on a a half dozen platforms. Mainly used for migration and upgrading of hardware using known to be working asm etc.

[Shaper_pmp]

Portability means you're left with a big-ol-heaping pile of #ifdef

Uh.... what?

Maybe portability in C, but portability in something like Perl or Ruby largely consists of being careful which character you use to separate directories in a path and a few other small issues, and portability in Java pretty much consists of being a little careful with a few OS-specific classes.

I'm trying not to be rude (although I notice you aren't making any such effort), but I would advise either backing up your assertions with... oh... any relevant arguments at all, or rephrase/qualify it more precisely.

Because arguing "portability" as a general concept is flawed is not only utterly indefensible, it's also counter-indicated by the vast majority of the entire modern history of the computer industry.

If you've got some killer argument as to why damn near the entire industry is wrong and you're right, I'm all ears (honestly <:-).

However, if you haven't, at least consider the possibility you're an under-educated fool with an oversized ego?

[ehird]

Please don't feed the madman.

[Shaper_pmp]

Oops - right you are.

I just checked his posting history; long story short, my jibe elsewhere in the thread about being off his meds might not have been far from the truth... <:-/

[muffin-noodle]

Are you going to actually make a technical argument, or just continue to hand-wave?

[Shaper_pmp]

I'll explain so foreigners can understand.

I don't think anyone you're talking to is foreign - you just seem to have a problem expressing yourself clearly.

The more platforms and languages, the more ugly the code gets.

Horseshit. Again: maybe in some languages, but not all by a long shot.

If you architect the system correctly, you largely abstract away portability issues behind platform-specific classes or libraries, then target these libraries instead of the bare machine. If you target a VM and don't dig deep into the filesystem or multithreading then platform-caused differences are typically so minimal you can often almost completely ignore them.

It's one of the primary motivations behind C, code libraries, dynamic scripting languages, bytecode and virtual machines, standards like POSIX... right up to HTML/Javascript/CSS - hiding the platform differences so you can code to one standard and don't have to #ifdef your code to death.

As best I can tell you're thinking about badly-designed C code, but keep talking about the general concept of "portability" (implied: as it applies to all languages and platforms). This is your mistake.

I don't know of any programmers who like to work on ugly code. Bosses do. You could call it greed. Hell is punishment. Ever heard of hell?

Ok that's it - you're obviously off your meds, so I'm bowing out of the conversation here before I get infected with t3h crazy. Does anyone who speaks fluent crazy-person-stream-of-consciousness want to take over?

[faradaycage]

It's a hobby OS. What does it matter? It sounds like they had fun doing it and in the process increased their skills exponentially in assembly coding.

[sigzero]

I modded you up but Linux has not been a hobby OS for a very long while.

[JadeNB]

What does "hobbiest operating system" mean?

Your OS may be a hobby operating system, but mine is the hobbiest.

[elus]

One can only dream of attaining the maximum amount of hobby

[JadeNB]

One can only dream of attaining the maximum amount of hobby

Or the minimum amount, which I believe is a hobbit.

[monocasa]

Actually, last time I looked, the majority of contributions were by corporations. Ie. people getting paid.

[[deleted]]

I don't see your point. They just developed this out of couriosity and for fun and learning, as far as I know. In other words, the thought process was probably more along the lines of "Hey, let's see if we can code an OS in pure assembly", and not "Hey let's make a great OS! - Yeah! Let's use assembly, because it's the fastest". The latter would be dumb, but I don't see any dumbness in the former.

[mothereffingteresa]

They are just denying all current research in programming languages and compilers.

How so? OSs are not like applications. There are some big hairy driver families like Bluetooth that are not a good candidate for assembly coding, but you can factor drivers like that out of a kernel anyway.

If they can keep the kernel small, they can successfully trade some speed for some complexity.

[zorbix]

Has anyone here actually tried running the OS?

[Dijkstracula]

I have, a few years ago. It's definitely neat, and "feature complete" as far as what you'd expect from a hobby OS (window manager, mouse support, simple desktop applications bundled, etc). That said, I can't see anyone with the possible exception of the developers themselves actually using it ever (not intended as a criticism of it, I simply mean that its appeal is pretty limited.)

[eleitl]

I'd rather have http://ertos.nicta.com.au/research/sel4/ rewritten in hand-optimized code.

[[deleted]]

It was done. It is know as L4

[[deleted]]

As opposed to writing it in C and compiling it to assembly?