Semantic Foundations for Real-World Systems

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

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.