In the past few years, computer processors have reached a speed limit imposed by semiconductor physics. Before, increased performance came from running a single program faster, but now it comes from running more programs concurrently, on multiple "cores". Multi-core processors also support low-power applications, and are becoming popular on mobile devices, such as smart phones, where several slow cores use less battery power than a single fast core. To write software for multi-core processors, programmers must decompose tasks into cooperating programs, ideally one per core. However, even experts cannot write these programs without tremendous effort, and the programs often have subtle bugs. Programmers have not been given the intellectual tools necessary for managing the complexity of multi-core computation. This project focuses on a critical challenge posed by multi-core processors: their relaxed memory models. Conceptually, the processor's cores are connected to a single memory, and programs running on different cores communicate by writing data to the memory for others to read. In reality, the processor achieves good performance by not giving the programmer a globally consistent picture of the memory: at any point in time the cores can appear to disagree on its contents. The processor does make some guarantees about the memory, so that the programmer can write working programs, but it carefully avoids making others. A relaxed memory model specifies which guarantees are made and which are not. Our objectives are to improve the theory of relaxed memory models, and to apply this theory to a new model that is easier to understand in practice. Most of the time, programming in a high-level language should have advantages over programming in the processor's low-level assembly language: advantages in, for example, reliability, security, and cost of development. However, this is not the case with relaxed memory models: the high-level language is more complicated because it has to account for the variety of significantly different processors that the high-level language can be compiled to, and it has to account for the compiler's optimisations too. The primary tension is between usability/security (for example, that sensitive data will not be leaked by a malicious program forging pointers to the data) and efficiency, with the latter driving existing designs. The Java Memory Model attempts to give basic security guarantees, but several underlying flaws have been discovered. On the other extreme, the new C and C++ models make no attempt to provide security guarantees. The design space for relaxed memory models has not been thoroughly explored. In this project, we will design a relaxed memory model for a high level language that gives stronger guarantees to programmers, making it easier to write, reason about, and verify concurrent programs. Our approach to the design combines a focus on real-world concurrent algorithms, to ensure that it is practical, with mathematical rigor, to ensure that it supports robust reasoning principles that will ultimately help programmers to understand it and to write high quality concurrent software systems.