Verification of a Rust Implementation of Knuth’s Dancing Links using ACL2: Abstract and Introduction
:::info
Author:
(1) David S. Hardin, Cedar Rapids, IA USA [email protected].
:::
Table of Links
Abstract and Introduction
Dancing Links
The Rust Programming Language
RAC: Hardware/Software Co-Assurance at Scale
Rust and RAR
Dancing Links in Rust
Related Work
Conclusion, Acknowledgments, and References
Abstract
“Dancing Links” connotes an optimization to a circular doubly-linked list data structure implementation which provides for fast list element removal and restoration. The Dancing Links optimization is used primarily in fast algorithms to find exact covers, and has been popularized by Knuth in Volume 4B of his seminal series The Art of Computer Programming. We describe an implementation of the Dancing Links optimization in the Rust programming language, as well as its formal verification using the ACL2 theorem prover. Rust has garnered significant endorsement in the past few years as a modern, memory-safe successor to C/C++ at companies such as Amazon, Google, and Microsoft, and is being integrated into both the Linux and Windows operating system kernels. Our interest in Rust stems from its potential as a hardware/software co-assurance language, with application to critical systems. 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 previous work, we described our initial implementation of a RAR toolchain, wherein 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, describe our improved prototype RAR toolchain, and detail the design and verification of a circular doublylinked list data structure employing the Dancing Links optimization in RAR, with full proofs of functional correctness accomplished using the ACL2 theorem prover.
1 Introduction
The exact cover problem [17], in its simplest form, attempts to find, for an n × m matrix with binary elements, all of the subsets of the rows of the matrix such that all the column sums are exactly one. This basic notion naturally extends to matrix elements that are in some numerical range; indeed, the popular puzzle game Sudoku is an extended exact cover problem for a 9× 9 matrix with element values in the range of 1 to 9, inclusive.
\
The exact cover problem is NP-complete, but computer scientists have devised recursive, nondeterministic backtracking algorithms to find exact covers. One such procedure is Knuth’s Algorithm X, described in [17]. In this algorithm, elements of the matrix are connected via circular doubly-linked lists, and individual elements are removed, or restored, as the algorithm proceeds, undergoing backtracking, etc. As these removals and restorations out of/into the list are quite common, making these operations efficient is a laudable goal. This is where Knuth’s “Dancing Links” comes in, resulting in an optimized algorithm for finding exact covers which Knuth calls DLX (Dancing Links applied to algorithm X).
\
:::info
This paper is available on arxiv under CC 4.0 license.
:::
\
Welcome to Billionaire Club Co LLC, your gateway to a brand-new social media experience! Sign up today and dive into over 10,000 fresh daily articles and videos curated just for your enjoyment. Enjoy the ad free experience, unlimited content interactions, and get that coveted blue check verification—all for just $1 a month!
Account Frozen
Your account is frozen. You can still view content but cannot interact with it.
Please go to your settings to update your account status.
Open Profile Settings