The Game Semantics of the Rust Programming Language

本项目属于EPSRC编程语言和编译器研究领域。Rust是一种现代系统编程语言，被设计为C++等流行语言的替代品。系统编程需要高性能的代码，以及能够轻松与硬件交互的语言。与此同时，Rust试图满足安全要求，即任何编译的程序都表现良好，例如释放不再需要的内存。内存安全语言通常包含一个称为垃圾回收的功能，该功能与用户的程序一起运行以释放未使用的内存。不出所料，这会导致较差的性能，因此Rust通过一个高级的输入系统来避免这种情况，该系统跟踪程序中谁拥有值，因此可以将它们识别为未使用的值。为了处理这个系统限制太多而无法解决问题的情况，Rust提供了一个“不安全”的结构，这让程序承担了证明他们的代码是安全的负担。这个项目的主要目标是通过游戏语义学的镜头来理解Rust语言的语义。编程语言的语义为用该语言编写的程序提供了数学意义。游戏语义学是一种基于这样一种观点的风格，即程序的一部分(术语)可以被建模为它与环境一起玩的问答游戏中的一种策略。在过去的25年里，游戏语义学已被证明是一个强大的范例，为具有许多不同功能的语言提供了结果。Rust的游戏语义还有待探索，因此这个项目将研究Rust的“所有权”系统如何在术语的策略中表现出来。要对使用“unSafe”构造的程序进行推理，我们需要在策略中显式处理未初始化值或悬空指针等概念。这是我们研究方法的另一个新奇之处，因为游戏语义学通常用于的抽象语言是安全的。我们打算使用的技术之一是操作游戏语义学，这只在顺序设置中进行了探索。在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.