The Game Semantics of the Rust Programming Language

Rust 编程语言的游戏语义

• 批准号: 2742896
• 金额: --
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2022
• 资助国家: 英国
• 起止时间: 2022 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2742896
• 关键词: Game; Semantics; Rust; Programming; Language

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.

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