- Formal program verification for a smart network interface controller
- Project Year:
2020
- REU Student (s):
Lance Tan | Yale University CT
- Student 1 Institution:
Yale University
- Project Mentor:
Srinivas Narayana
- Project Mentor Area:
Computer Science
- Project Abstract:
The network interface card (NIC) is the hardware component that connects a computer, such as a laptop, server, or datacenter, to the internet. The NIC sits in the path of the data moving in and out of your machine, allowing it to compute over the data as it transits. For example, a NIC might automatically compress data going in and out of your machine to save bandwidth and reduce download time. With the advent of software-defined networking, along with ever-increasing network bandwidths, NICs have become increasingly flexible in the computations they support, and their architectures more complicated. The Netronome NFP-6000 is one example of these "smart NICs". We present a formal specification of arithmetic and logic instructions for the Netronome NFP-6000, and a programmatic framework for interpreting and formally validating Netronome programs. This work brings us closer to a superoptimizing compiler for Netronome smart NIC programs, and will help further understanding of the capabilities and limitations of hardware acceleration using NICs.
