Author:
(1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Table of Links 1 Introduction 2 Dancing Links 3 The Rust Programming Language 4 RAC: Hardware/Software Co-Assurance at Scale 5 Rust and RAR 5.1 Restricted Algorithmic Rust 6 Dancing Links in Rust and 6.1 Definitions 6.2 Translation to ACL2 6.3 Dancing Links Theorems 7 Related Work 8 Conclusion 9 Acknowledgments and References 5 Rust and RAR The Rust Programming Language [16] is a modern, high-level programming language designed to combine the code generation efficiency of C/C++ with drastically improved type safety and memory management features. A distinguishing feature of Rust is that a non-scalar object may only have one owner. For example, one cannot assign a reference to an object in a local variable, and then pass that reference to a function. This restriction is similar to those imposed on ACL2 single-threaded objects (stobjs) [4], with the additional complexities of enforcing such “single-owner” restrictions in the context of a generalpurpose, imperative programming language. The Rust runtime performs array bounds checking, as well as arithmetic overflow checking (the latter can be disabled by a build environment setting). In most other ways, Rust is a fairly conventional modern programming language, with interfaces (called traits), lambdas (termed closures), and pattern matching, as well as a macro capability. Also in keeping with other modern programming language ecosystems, Rust features a language-specific build and package management sytem, named cargo. 5.1 Restricted Algorithmic Rust As we wish to utilize the RAC toolchain as a backend in our initial work, Restricted Algorithmic Rust is semantically equivalent to RAC. Thus, we adopt the same semantic restrictions as described in Russinoff’s book. Additionally, in order to enable translation to RAC, as well as to ease the transition from C/C++, RAR supports a commonly used macro that provides a C-like for loop in Rust. Note that, despite the restrictions, RAR code is proper Rust; it compiles to binary using the standard Rust compiler. RAR is transpiled to RAC via a source-to-source translator, as depicted in Fig. 3. Our transpiler is based on the plex parser and lexer generator [28] source code. We thus call our transpiler Plexi, a nickname given to a famous (and now highly sought-after) line of Marshall guitar amplifiers of the mid-1960s. Plexi performs lexical and syntactic transformations that convert RAR code to RAC code. Recent improvements in the plexi tool include better handling of array declarations, as well as providing support for Rust const declarations. The generated RAC code can then be compiled using a C/C++ compiler, fed to an HLS-based FPGA compiler, as well as translated to ACL2 via the RAC ACL2 translator, as illustrated in Fig. 3. This paper is available on arxiv under CC BY 4.0 DEED license. Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Author: Author: (1) David S. Hardin, Cedar Rapids, IA USA (david.s.hardin@gmail.com). Table of Links 1 Introduction 1 Introduction 2 Dancing Links 2 Dancing Links 3 The Rust Programming Language 3 The Rust Programming Language 4 RAC: Hardware/Software Co-Assurance at Scale 4 RAC: Hardware/Software Co-Assurance at Scale 5 Rust and RAR 5 Rust and RAR 5.1 Restricted Algorithmic Rust 5.1 Restricted Algorithmic Rust 6 Dancing Links in Rust and 6.1 Definitions 6 Dancing Links in Rust and 6.1 Definitions 6.2 Translation to ACL2 6.2 Translation to ACL2 6.3 Dancing Links Theorems 6.3 Dancing Links Theorems 7 Related Work 7 Related Work 8 Conclusion 8 Conclusion 9 Acknowledgments and References 9 Acknowledgments and References 5 Rust and RAR The Rust Programming Language [16] is a modern, high-level programming language designed to combine the code generation efficiency of C/C++ with drastically improved type safety and memory management features. A distinguishing feature of Rust is that a non-scalar object may only have one owner. For example, one cannot assign a reference to an object in a local variable, and then pass that reference to a function. This restriction is similar to those imposed on ACL2 single-threaded objects (stobjs) [4], with the additional complexities of enforcing such “single-owner” restrictions in the context of a generalpurpose, imperative programming language. The Rust runtime performs array bounds checking, as well as arithmetic overflow checking (the latter can be disabled by a build environment setting). In most other ways, Rust is a fairly conventional modern programming language, with interfaces (called traits), lambdas (termed closures), and pattern matching, as well as a macro capability. Also in keeping with other modern programming language ecosystems, Rust features a language-specific build and package management sytem, named cargo. 5.1 Restricted Algorithmic Rust As we wish to utilize the RAC toolchain as a backend in our initial work, Restricted Algorithmic Rust is semantically equivalent to RAC. Thus, we adopt the same semantic restrictions as described in Russinoff’s book. Additionally, in order to enable translation to RAC, as well as to ease the transition from C/C++, RAR supports a commonly used macro that provides a C-like for loop in Rust. Note that, despite the restrictions, RAR code is proper Rust; it compiles to binary using the standard Rust compiler. RAR is transpiled to RAC via a source-to-source translator, as depicted in Fig. 3. Our transpiler is based on the plex parser and lexer generator [28] source code. We thus call our transpiler Plexi, a nickname given to a famous (and now highly sought-after) line of Marshall guitar amplifiers of the mid-1960s. Plexi performs lexical and syntactic transformations that convert RAR code to RAC code. Recent improvements in the plexi tool include better handling of array declarations, as well as providing support for Rust const declarations. The generated RAC code can then be compiled using a C/C++ compiler, fed to an HLS-based FPGA compiler, as well as translated to ACL2 via the RAC ACL2 translator, as illustrated in Fig. 3. This paper is available on arxiv under CC BY 4.0 DEED license. This paper is available on arxiv under CC BY 4.0 DEED license. available on arxiv

Part of HackerNoon's growing list of open-source research papers, promoting free access to academic material.

Scaling Hardware/Software Co-Assurance with Restricted Algorithmic C

Read My Stories

Too Long; Didn't Read

Make resilience your competitive advantage

RRR—Rust, RAR, and RAC: The Trifecta for Co-Design Excellence

About Author

Comments

TOPICS

THIS ARTICLE WAS FEATURED IN

Related Stories

Untitled Story

Future Work in Rust Co-Assurance

Scaling Hardware/Software Co-Assurance with Restricted Algorithmic C

The Case for Rust Programming as a Game-Changer for High-Level Synthesis

The Algorithm That Makes Data Dance—and Solve Complex Problems Fast

Simplifying Circular Data Structures with Rust’s RAR Subset

Future Work in Rust Co-Assurance

Scaling Hardware/Software Co-Assurance with Restricted Algorithmic C

The Case for Rust Programming as a Game-Changer for High-Level Synthesis

The Algorithm That Makes Data Dance—and Solve Complex Problems Fast

Simplifying Circular Data Structures with Rust’s RAR Subset

Light-Mode

Classic

Newspaper

Dark-Mode

Neon Noir

Minty

HN StartUps