Currently, real concurrent programs are too difficult to understand. Even expert programmers cannot reliably write bug-free high-performance concurrent algorithms, and researchers in programming languages and in formal verification are struggling to bring their work into the multi-core world. Modern hardware and languages -- especially x86, ARM, Power, C, C++, and Java -- are complex, often convoluted, systems with pervasive engineering trade-offs to achieve conflicting goals about cost, performance, usability, and backwards compatibility. In particular, they perform sophisticated optimisations that have visible effects on concurrent programs: the values read during a program's execution might not be explainable by any consistent, global ordering of the values written. In this talk, I will explain how my recent work on understanding concurrency addresses these problems. Crucially, my work relies on the application of formal mathematical specifications to real systems programs -- only formal specifications can accurately capture and clarify modern multi-core architectures. The key contributions are a precise, programmer-centric understanding of what these architectures are, and subsequent techniques to ensure that concurrent algorithms are robust, efficient, and bug-free. I will illustrate my approach using algorithms from the x86 version of the Linux kernel. I will also briefly describe the more complex concurrency found in C++ and on Power/ARM machines and finally, explain how we can understand the implementation of concurrent languages on concurrent hardware.