secret sauce

Jiří tells me


Last friday, my research accidentally met its goal of finding bugs - or at least, in one very specific case.

I was looking into ways for my code to generate keyboard interrupts+input - it turns out simics has a nice interface in the kbd0.key_event attribute - and testing it by triggering some hard-coded keyboard input when the kernel reaches a particular (also hard-coded) point in the fork() path. the input was "mandelbrot\n", which (being received by the shell) should cause the so-named test to start running - except the input would be repeated when fork() runs again, so the kernel's readline() logic would have to deal with multiple inputted lines while another program is writing to the console at the same time.

Here's what pathos, the 410 reference kernel, does:

And what BrOS, the student kernel of Eric Faust (who is periodically keeping me company and scoffing at my code), does:

Slightly different, and not in agreement with the Pebbles specification, though Eric claims it's misdesigned rather than buggy. Finally, here's what POBBLES, my own student kernel, does:

Note the top-left character - that is where every single character of the mandelbrot fractal is being drawn. Also, the input string (rather, parts thereof) is drawn five times, despite only being issued twice. No "misdesign" would cause that...


Hello! This is the project blog for Ben Blum's 5th year master's project at CMU, under the advisory of Garth Gibson and working with Jiří Šimša.

Jiří has a project called dBug, which does runtime concurrency verification on userland programs by interposing itself between the application under test and the dynamic libraries, thereby to control the nondeterministic aspects of the program's execution. I hope to extend these same ideas to work in kernel-space, where concurrency issues can be much more intricate and subtle.

15-410 - Operating System Design and Implementation - is a class at CMU where students, in a six-week-long project, implement a small UNIX-like kernel, called Pebbles, from the ground up. Students do most of their development in Simics, an x86 simulator, and typically produce code which has many race conditions, which have to be spotted either by the student during the project or by the grader after the project.

I aim to develop a system for race condition detection on Pebbles kernels in the form of a Simics module, to be used by the 410 course staff to help grade student submissions and by the students to help debug their code, and hopefully to serve as a starting point for similar tools in more complicated environments (i.e., industrial kernels such as Linux).

The project is called landslide because it shows that pebbles kernels are not as stable as one might hope.