Software Analysis for Weak Memory Models

Michael Tautschnig

In order to achieve optimal throughput on multi-core systems, systems software uses lock-free concurrent code. On the hardware side, multi-core processors optimize performance by relaxing memory consistency constraints. As language memory models are agnostic to the details of hardware memory models, a sound and precise software verification of systems code needs to take into account these hardware characteristics.

In this talk I will summarize recent work laying the foundations for software verification by establishing a class of sound data-flow analyses, and will then describe an approach for actual software verification with respect to relaxed memory consistency models.