The Game Semantics of the Rust Programming Language

这个项目属于EPSRC编程语言和编译器研究领域。Rust是一种现代系统编程语言，被设计为c++等流行语言的替代品。系统编程需要高性能的代码，以及一种能够轻松与硬件交互的语言。同时，Rust试图满足对安全性的要求，即任何编译后的程序都表现良好，例如释放不再需要的内存。内存安全语言通常包含一个称为垃圾收集的特性，它与用户的程序一起运行以释放未使用的内存。不出所料，这会导致较差的性能，因此Rust通过一个高级的类型系统来避免这种情况，该系统可以跟踪谁“拥有”程序中的值，这样它们就可以被识别为未使用。为了处理这个系统限制太大而无法解决问题的情况，Rust提供了一个“不安全”的结构，它把证明它们的代码是安全的负担放在程序上。这个项目的主要目标是通过游戏语义来理解Rust语言的语义。编程语言的语义赋予用该语言编写的程序以数学意义。游戏语义学是一种基于这样一种理念的风格，即程序的一部分（一个术语）可以被建模为与环境进行问答游戏的策略。在过去的25年里，游戏语义已经被证明是一个强大的范例，为具有许多不同功能的语言提供了结果。Rust的游戏语义尚未被探索，所以这个项目将研究Rust的“所有权”系统如何在术语策略中体现出来。为了解释使用“不安全”结构的程序，我们需要显式地处理诸如未初始化值或悬空指针之类的策略概念。这是我们研究方法的另一个新奇之处，因为游戏语义通常使用的抽象语言是安全的。我们打算使用的技术之一是操作游戏语义，这只在顺序设置中被探索过。在Rust中处理并发会促使这种技术泛化，它也将适用于Rust之外。有了语义模型，我们就可以把注意力转向下一个目标——利用这个模型开发推理技术。语义学中的一个规范问题是上下文等价——本质上是问一个术语是否可以随处替换另一个术语。游戏语义已经被用于在各种环境中解决这个问题，并且应该在这里产生令人满意的结果。另一类问题是验证问题——证明一个程序满足一个特定的属性。在Rust中出现了一个很自然的例子，表明“不安全”结构中的代码实际上是安全的。Rust最近的工作已经建立了一种技术来生成使用“不安全”的库必须满足的条件，以确保安全，并提供了一个框架来执行这些证明。然而，开发这些证明仍然需要熟练的人为干预，这使得它们无法广泛使用。利用游戏语义的技术已经为其他设置中的程序验证产生了自动方法，因此希望这里的情况也是如此。要实现这一点，需要对满足这些逻辑定义的条件如何约束术语策略进行新颖的研究，将来自不同语义领域的想法结合在一起。一旦为Rust程序的推理设计了合理的数学技术，就可以应用这些技术来创建用于验证问题的实用工具。这个项目的最终目标是基于这些技术生产原型工具，并在代表性实例上评估它们的效率。其他寻求平衡性能和安全性的语言，如Carbon，很可能会采用与Rust类似的技术，使这项工作更广泛地适用。

This project falls into the EPSRC Programming Languages and Compilers research area.Rust is a modern systems programming language which is designed as an alternative to popular languages like C++. Systems programming demands high-performance code, and a language able to interact with the hardware easily. At the same time, Rust tries to meet demands for safety, which is that any program which compiles is well behaved, such as freeing memory which is not longer needed. Memory safe languages often incorporate a feature called a garbage collection, which runs alongside the user's program to free unused memory. This, unsurprisingly, leads to poor performance, and so Rust avoids this by having an advanced typing system which tracks who 'owns' values in the program, so they can be identified as unused. To handle cases where this system is too restrictive to solve the problem, Rust offers an 'unsafe' construct, which puts the burden on the program to prove that their code is safe. The key objective of this project is to understand the semantics of the Rust language through the lens of game semantics. The semantics of a programming language gives a mathematical meaning to programs written in that language. Game semantics is a style based on the idea that a part of a program (a term) can be modelled as a strategy in a game of question and answer it plays with its environment. Over the last 25 years, game semantics has proven to be a powerful paradigm, providing results for languages with many diverse features. Game semantics for Rust have yet to be explored, and so this project will investigate how the 'ownership' system of Rust manifests itself in the strategies of terms. To reason about programs using the 'unsafe' construct, we will need to explicitly handle in strategies notions like uninitialized values or dangling pointers. This is a another novelty of our research methodology, as the abstract languages game semantics is normally used for are safe. One of the techniques we intend to use is operational game semantics, which has only been explored in the sequential setting. Handling concurrency in Rust would motivate generalising this technique, which will also be applicable outside of Rust.With a semantic model at hand, we can then turn our attention to the next aim - developing reasoning techniques exploiting this model. A canonical problem in semantics is contextual equivalence - essentially asking if one term can be substituted for another everywhere. Game semantics has been used to solve this problem in a variety of settings, and should yield satisfying results here. Another type of problem is that of verification - proving that a program satisfies a particular property. A natural instance of this arises in Rust from showing that code in an 'unsafe' construct is in fact safe. Recent work on Rust has established a technique to generate conditions a library using 'unsafe' must meet in order to be safe, and provides a framework for conducting these proofs. However, developing these proofs still requires skilled human intervention, making them impractical for widespread use. Techniques exploiting game semantics have produced automatic methods for program verification in other settings, and so it is hoped the same will be the case here. Achieving this would involve a novel investigation of how satisfying these logically defined conditions constrain the strategies of terms, bringing together ideas from different areas of semantics. Once sound mathematical techniques have been devised for reasoning about Rust programs, these can be applied to create practical tools for verification problems. A final aim of this project is to produce prototype tools based upon these techniques, and assess their efficiency on representative instances. It is likely that other languages seeking to balance performance with safety, such as Carbon, will adopt a similar techniques to Rust, making this work more widely applicable.