Jonas Oberhauser

From the roots to the sky: end to end concurrency verification in DresdenRC

The verification needs of single-threaded code can often be met by extensive testing. On the other hand, the nondeterminism and combinatorial explosion of concurrent and weak-memory model code imply that tests that succeed on one machine under a specific load may fail if machine or load change, and those failures often can't be reproduced in a test setting.

In this talk we summarize the experience of DresdenRC in trying to create a stable concurrency stack over the past three years, and its mission to extend this stack all the way down to the hardware and up to the application layer.

back to overview

Watch Recording
Speaker Image
 

Biography

Jonas Oberhauser is a full-stack concurrency verification researcher. He has worked on weak memory model theory and verification technology for industrial concurrent libraries, applications, weak-memory model compiler mappings, and hardware. Some of these technologies have been used to find and repair extremely subtle bugs or push the performance envelope by enabling engineers to design more complex systems and better leverage modern hardware features.
Footer

Imprint / Privacy