Improved tristate number multiplication with formal proof and precision
Improved Tristate Multiplication With Formalization in Rocq
Logic in Computer Science
Summary
Multiplying numbers that have a special three-state form is tricky, and getting exact answers quickly is important for computers like Linux. The authors created a new way to multiply these tristate numbers that is more accurate than the previous method used in the Linux kernel. They also made sure this new method is reliable by proving it mathematically with a tool called Rocq. Their method works equally fast as before but gives better results almost all the time, and it applies to numbers of any size.
What this means in practice
- •For operating system developers: Integrate improved tristate multiplication to increase accuracy of computations within the Linux kernel without sacrificing performance.
- •For hardware verification engineers: Use formally verified multiplication algorithms to enhance the reliability of hardware models involving tristate values.
Authors
Nandakumar Edamana, Piyush P Kurur, Unnikrishnan Cheramangalath
Abstract
We give a new multiplication algorithm for tristate numbers improving upon the state-of-the-art implementation from the Linux kernel in terms of precision and formal proofs. Our algorithm is significantly more precise as shown by experimental evaluation (at the peak, giving better results in 95.59% cases compared to the previous work for 31-bit samples). Importantly, we achieve this additional precision with performance comparable to the previous algorithm, as demonstrated by benchmarks. Finally, we formalize and prove the soundness of the algorithm in the Rocq proof assistant, adding to the trust in the resulting implementation. Our algorithm is now part of the upstream Linux kernel. Our soundness proof in Rocq for the new multiplication algorithm works for all bit widths, while the SAT/SMT-based machine-checked proof accompanying the previous algorithm was restricted to 8 bits. We also provide Rocq proofs for the soundness and optimality of the newly added tnum union operation and the existing tnum addition algorithm from the Linux kernel. Our optimality proof for tnum addition presents a simpler and straightforward lemma compared to prior work.