Semantic Foundations for Real-World Systems

计算机系统已经普及了很多年，但是尽管如此，尽管投入了巨大的资源来构建它们，它们仍然通常是不安全的，容易发生故障，并且难以使用。与其他工程行业的产品形成鲜明对比的是，重大故障是司空见惯的，处理这些故障以及日常较小的缺陷需要付出巨大的经济和社会成本。核心的技术困难是系统的复杂性：行为的范围、大规模和旧设计选择的遗留问题结合在一起，使得很难很好地理解这些系统，从而很好地设计它们。我的主要研究目标是开发足以用于坚实系统构建的智能工具，类似于更传统的工程学科的应用数学。这必须以实际系统为基础——不可能在理论上孤立地完成。我的方法，正如Track Record中所记录的那样，是关注用于构建系统的抽象层次中的关键衔接点：编程语言、处理器指令集、网络协议等等。在快速变化的环境中，这些是相对稳定的点，对所有系统开发都是至关重要的，并且足够小，一个适度的团队可以处理它们。每一种都需要不同的研究：新的语言结构、新的规范、推理和测试技术等等。在这篇论文中，我将继续研究这种方法，重点关注在现代多处理器复杂的宽松内存模型之上构建计算机系统的问题。多处理器系统现在是标准的（因为顺序处理器的进一步加速最近变得不切实际），但是编程它们是非常具有挑战性的。一个关键的困难是，这些系统不提供顺序一致的记忆，其中事件似乎以单一的全局时间顺序发生，而是允许微妙的重新排序，使得直观的全局时间推理不可靠。以前在计算机科学领域的许多工作，包括编程语言、程序逻辑、并发理论、模型检查等，都做出了现在不现实的顺序一致性假设，现在必须在这个更复杂的环境中重新审视它。我将开发考虑这种重新排序的真实世界多处理器行为的精确数学模型，并在此基础上开发语义和推理技术。使用这些工具，我将考虑高性能并发算法的验证（如在操作系统和管理程序内核中使用的）、高级语言的设计以及这些语言在真实机器上的验证编译。这将使未来的应用能够在高置信度和高性能的基板上开发。它还应该对计算机科学研究产生更广泛的有益影响，将数学上有充分基础的理论和系统构建实践结合起来。

Computer systems have been pervasive for many years, but despite this, and despite the huge resources devoted to their construction, they are still typically insecure, prone to failure, and hard to use. Major failures are commonplace, in sharp contrast with the products of other engineering industries, and dealing with them, and with the day-to-day lesser flaws, has huge economic and social costs. The core technical difficulty is system complexity: the range of behavior, the large scale, and the legacy of old design choices combine to make it hard to understand these systems well enough to engineer them well. My main research goal is to develop intellectual tools that suffice for solid system-building, analogous to the applied mathematics of more traditional engineering disciplines. This must be grounded on real systems - it cannot be done in theoretical isolation. My approach, as documented in the Track Record, is to focus on the key articulation points in the hierarchy of abstractions used to build systems: programming languages, processor instruction sets, network protocols, and so forth. These are relatively stable points in a rapidly changing environment, are critical to all system development, and are small enough that a modest team can address them. Each demands different research: new language constructs, new specification, reasoning, and testing techniques, and so forth. In this Fellowship I will pursue this approach, focussing on the problems in building computer systems above the intricate relaxed memory models of modern multiprocessors. Multiprocessor systems are now the norm (as further speed-up of sequential processors has recently become impractical), but programming them is very challenging. A key difficulty is that these systems do not provide a sequentially consistent memory, in which events appear to occur in a single global time order, but instead permit subtle reorderings, rendering intuitive global-time reasoning unsound. Much previous work across a range of Computer Science, in programming languages, program logics, concurrency theory, model checking, and so on, makes the now-unrealistic assumption of sequential consistency, and it must now be revisited in this more complex setting.I will develop precise mathematical models of the behavior of real-world multiprocessors that take such reorderings into account, and develop semantics and reasoning techniques above them. Using those, I will consider the verification of high-performance concurrent algorithms (as used in operating system and hypervisor kernels), the design of higher-level languages, and verified compilation of those languages to real machines. This will enable future applications to be developed above a high-confidence and high-performance substrate. It should also have a broader beneficial effect on research in Computer Science, drawing together mathematically well-founded theory and systems-building practice.