Practical Verification in Practice: Enabling Performance on Modern Hardware after Moore’s Law

In the post-Moore's Law era, hardware tends to be heterogeneous multi-core. Highly reliable and high-performance multi-core concurrency control is the key to efficiently leverage multi-core machines. However, weak memory consistency, big.LITTLE cores, and NUMA of modern multi-core architectures bring new challenges to multicore concurrency control including inter-core synchronous and asynchronous communication. This talk will introduce some of Huawei DRC's recent industrial practices in applying formal methods to build a provable multi-core concurrency library. With the effective support of formal verification and optimization tools, programmers have the confidence to aggressively design and optimize concurrency algorithms, and this can effectively improve the performance of the concurrency library while providing correctness guarantee.