Redis crashes - a small rant about software reliability

> Sorry, the Sinatra based site is deployed with "ruby app.rb". Probably not enough..

Since you are running it as "ruby app.rb", I take it you aren't interested in doing an app server/web server/cache deployment. But if you aren't using thin, that's only a "gem install thin" away.

I don't really understand your driver argument, because when deploying Linux on an embedded system, you would only use the drivers you need... so you'd have the same amount of driver code as with any other kernel.

You say that you managed to "verify correctness" on QK, but clearly, that's not an accurate statement, since AFAIK seL4 is the only kernel that has ever been "proven correct" (and even for seL4, there are some gotchas there, AFAIK).

If you truly care about correctness, doing formal verification, model checking, etc. ...

The common perception is that model checking and formal verification are still just research areas that can't be used practically beyond toy problems. Again, seL4 is the only kernel I know of that has been "proven correct," and that has taken an insane amount of manpower that is not scalable to anything more complex than seL4. That seems to be evidence that there is something to the "common perception" I stated above.

lots of people use it so it must be stable

That's not really my argument. With Linux, there is an insane amount of testing going on all the time (I mean "informal" testing.. just people using it and reporting problems if they encounter any.. though there are also farms set up that test Linux, as well). Linux must be by far the most highly-tested software in history. On the other hand, you could use formal methods on some small kernel and maybe get some help (but again, far short of proving there are no bugs, AFAIK), but the level of testing will be many orders of magnitude less. Clearly, which one wins out depends on how good the actual state of the art in formal methods is, but my impression is that many orders of magnitude more testing will win out, unless the problem you are solving is very, very small.

The blog uses Redis as primary data store, unfortunately there is Ruby between the user and the DB ;-)

Btw here the problem was mine, I was running the Sinatra app wit "ruby app.rb", and Apache was mod_proxing to this running on port 4567.

By default mod proxy will suspend the connection 60 seconds with an error if the proxed thing returns something wrong. Idiotic default that can be avoided just with:

    ProxyPass / http://127.0.0.1:4567/ retry=0

See "retry=0".

Thanks for the feedback, this is currently a landing page we give to our customers we meet face to face. We're working on something more consistent to answer questions like yours.

quasardb is a key/value store.

It is (a lot) faster in a multi-client context that the engines you listed and can handle entries of any size (provided you have enough space on the servers, of course!).

It's fully symmetric which means the load is equally distributed and replicated on all the nodes (no master node).

If you have more question feel free to mail us (don't want to highjack this thread).

The entire QK[1] kernel, including all library code, is less that two thousand lines of C (and most of the library code isn't even used by the kernel itself, which is just 234 LOC). QK is a single-processor kernel (although still pre-emptive) and very well written and tested (in, literally, hundreds of millions of devices).

It was not difficult at all to run QK and it's supporting code through KLEE and exhaustively verify the properties of each function, thanks to a super-simple design and the many included assertions, preconditions, and postconditions, which KLEE helpfully proves are satisfied automatically. If I wanted a certified optimizing C compiler, I'd use CompCert[2] to compile QK, which would give me a certified kernel all the way to machine code. (I actually use Clang.)

I am familiar with the verified L4 kernel, and it is far more complex than the QK kernel I have verified. That people have already verified a kernel far more complex should be sufficient proof that a much simpler kernel can also have its correctness verified.

Stepping back, it's 2012: people should no longer be surprised when a small-but-meaningful codebase is certified correct. It's common enough now that you don't get published in a journal just because you did it.

[1] http://www.state-machine.com/qp/index.php

[2] http://compcert.inria.fr/