Diogo Behrens

Enabling Performance on Modern Hardware with Practical Verification

Modern commodity hardware is diverse. Different core pairs within the same processor may communicate with different speeds due to deep memory hierarchies. Groups of cores can even have different processing and energy consumption specifications such as big.LITTLE architectures. Moreover, memory operations can be reordered in a multitude of ways.

To build efficient systems, one cannot treat cores as homogeneous, exchangeable processing units. Algorithms, specially concurrent algorithms, have to be aware of the hardware heterogeneity to be able to exploit it. Unfortunately, awareness has an intrinsic cost: complexity.

In this talk, we argue that some level of formal verification is a requisite for system builders willing to take the next step in the design of concurrent algorithms. Without that, systems are doomed to fail in the most unpredictable and unreproducible ways. We review and connect a few of our success stories and draw a path for the future work.

back to overview

Watch Recording


Diogo Behrens is research engineer at Huawei Dresden Research Center, currently leading the System Software Concurrency team. Before joining Huawei in 2019, Diogo was software engineer with focus on stream data processing. He holds a PhD from TU Dresden.