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.
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
