andikleen3

An eternity ago a particular Linux kernel developer gave a series of "Why user space sucks" talks at Linux conferences. It was just going through strace logs and making fun of particularly bad examples.

Here's one instance: https://www.kernel.org/doc/ols/2006/ols2006v1-pages-441-450....

At some point I stared a lot at instruction level traces with Processor Trace or LBRs and usually I found some bad sequences in many programs, where things are implemented very inefficiently.

You just have to be very careful with the algorithms in that paper, they had some serious problems (apart from their basic inability to deal with faster links). I like this old but fairly damning analysis from an early Linux TCP developer:

https://ftp.gwdg.de/pub/linux/tux/net/ip-routing/README.rto

I can confirm the issues with formal methods.

I was working on a new type of locking mechanism and thought I would be smart by modelling it in spin [http://spinroot.com], which has been used for these kind of things before.

I ended up with a model that was proven in spin, but still failed in real code.

Given that's anecdata with a sample size of 1, but still was a valuable experience to me.

I maintain a tool that reports errors on Linux systems with ECC memory, and also a website describing the tool (http://mcelog.org). I wrote about patterns in the access logs correlated to time some time ago in my blog:

http://halobates.de/blog/p/181