论文标题
使用Rust编程语言和ACL2的硬件/软件共同保证
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2
论文作者
论文摘要
生锈的编程语言引起了人们的兴趣并用作现代，类型的安全性，可保险和可能正式分析的编程语言。我们对Rust的兴趣源于其作为硬件/软件共同提供语言的潜力，并应用于自动驾驶汽车等关键系统。我们报告了Rust作为高级合成（HLS）语言的首次已知用途。大多数现有的HLS语言是C的子集。基于Rust的HLS为硬件和软件实现带来高保证的单一现代，类型和内存安全的表达语言。作为对RUST作为HLS的适用性的研究，我们精心制作了Rust子集，灵感来自Russinoff受限算法C（RAC）的启发，我们已经想象中命名为受限的算法算法Rust或RAR。在首次实施RAR工具链时，我们只需将RAR源转移到RAC中。通过这样做，我们利用了许多现有的硬件/软件共同保证工具，并以最少的时间和精力投资。在本文中，我们描述了RAR RUST子集，详细介绍了我们的原型RAR工具链，并描述了用RAR编写的几种代表性算法和数据结构的实现和验证，并使用ACL2定理示意剂进行了正确性的证明。
The Rust programming language has garnered significant interest and use as a modern, type-safe, memory-safe, and potentially formally analyzable programming language. Our interest in Rust stems from its potential as a hardware/software co-assurance language, with application to critical systems such as autonomous vehicles. We report on the first known use of Rust as a High-Level Synthesis (HLS) language. Most incumbent HLS languages are a subset of C. A Rust-based HLS brings a single modern, type-safe, and memory-safe expression language for both hardware and software realizations with high assurance. As a a study of the suitability of Rust as an HLS, we have crafted a Rust subset, inspired by Russinoff's Restricted Algorithmic C (RAC), which we have imaginatively named Restricted Algorithmic Rust, or RAR. In our first implementation of a RAR toolchain, we simply transpile the RAR source into RAC. By so doing, we leverage a number of existing hardware/software co-assurance tools with a minimum investment of time and effort. In this paper, we describe the RAR Rust subset, detail our prototype RAR toolchain, and describe the implementation and verification of several representative algorithms and data structures written in RAR, with proofs of correctness conducted using the ACL2 theorem prover.
