Multiprocessors: From Microarchitecture to Semantic Theory

Modern computers have become predominantly multicore, providing programmers with many simultaneously-executing threads of execution sharing the system memory. Concurrent programming is challenging, and this trend in hardware should have been an ideal application target for previous academic work on software verification. Concurrent programming has been extensively studied, with the development of areas such as model checking, process calculi, separation logic, and rely-guarantee reasoning. Unfortunately, realistic architectures violate a key assumption of most such work, that all threads have a consistent view of memory, an assumption often referred to as Sequential Consistency. Instead, programmers are actually faced with a Relaxed Memory Model , with only approximate consistency, making programming and verification significantly more challenging.Relaxed memory models arise, ultimately, from hardware (and compiler) implementation features designed for performance. Unfortunately, there is no clear understanding of how the microarchitectural choices made in hardware implementations lead to programmer-observable consequences. This is an instance of a more general problem, that modern hardware is too complex to understand without formal proofs, as witnessed by a succession of errata in deployed processors. Hardware verification is itself a field that has received a great deal of study. However, the field has still not reached the point of verifying global semantic properties, such as relaxed memory models, that emerge from the interaction of multiple disparate subsystems, each of which suffers from imprecise specifications.I propose to create a general theory of the programmer-observable behaviour which emerges from the microarchitectural choices and optimizations made in multiprocessor implementations. I will develop abstract mathematical models of the implementations, and explain with proof the observable consequences of those implementations. With specifications derived from that theory, I will go on to study the hardware verification problem, establishing techniques and methods for verifying global programmer-visible properties. Throughout, I will address not just safety properties, but also progress and liveness properties that sophisticated programmers rely on.Such a general theory is critical for a better understanding of multiprocessor semantics, by both programmers and hardware implementers, and for enabling these different communities to communicate their knowledge to each other. It is also an essential prerequisite for sound theories of concurrent programming. An improved understanding and communication of these issues is imperative for reliable multiprocessor usage.

The beneficiaries of this research in the larger world include practitioners of concurrent programming, and of computer architecture, and of the verification of both, within both academia and industry. This will in the medium term benefit the users of shared memory multiprocessors, who will find their systems becoming more reliable. Such users constitute a huge and still growing section of the general public, since desktops, mobile devices, and servers are steadily becoming multiprocessor. As an indicative point for the time required for benefits to become available to the general public, hardware designs take on the order of five years to become publicly available. The academic beneficiaries are listed in a separate section, and I note that there already exists very strong links between the academic and industrial community in each of these fields, leading to an easy exchange of knowledge within each field. I note some additional points relevant to industrial practitioners here. Modern hardware architectures are extremely complex, and also extremely difficult to change if found not to be correct. The major processor vendors, including Intel, AMD, IBM, and ARM, have already deployed a huge number of multiprocessors, in high-performance systems, in commodity consumer computers, and in the embedded market, with even mobile phones starting to become multiprocessor. This trend will intensify as low-power and high-performance devices enjoy greater demand, and it becomes critical to remove bugs and inconsistencies at an early stage, and give precise guarantees about multiprocessors to the programmers that develop systems above them. Mistakes can be very expensive, in terms of both money and reputation. Key improvements can be made by using mathematical theory at early stages of the design process, for example, by helping cache-protocol designers understand the consequences of the choices they make on programmer-observable behaviour. I will engage with the hardware-design community, particularly with my project partners in IBM, as also the large expert community in the Austin industrial area. I also have a nascent relationships with ARM in Cambridge, which I hope to build upon. The real-world expertise and experience provided by my industrial contacts will complement my expertise in semantics and mechanized mathematics. The proposed work will provide methods and techniques of verification, and example formal proofs of concrete implementations as case studies. I will make these publicly available in the scientific literature, and via the web.