Program Equivalence Checking for the Facilitation of Quantum Offloading
- Resource Type
- Conference
- Authors
- Speer, Jon; Nurminen, Jukka K.
- Source
- 2021 IEEE 11th Annual Computing and Communication Workshop and Conference (CCWC) Computing and Communication Workshop and Conference (CCWC), 2021 IEEE 11th Annual. :1464-1470 Jan, 2021
- Subject
- Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Computing and Processing
Photonics and Electrooptics
Power, Energy and Industry Applications
Robotics and Control Systems
Signal Processing and Analysis
Computer science
Quantum algorithm
Conferences
Semantics
Task analysis
Software tools
Testing
Program Equivalence Checking
Quantum Computing
Quantum Offloading
Shor's Algorithm
- Language
Computational offloading involves the transfer of computational tasks to a separate device. We apply this concept to quantum computing, whereby particular algorithms (i.e. “quantum algorithms”) are automatically recognized and executed on a quantum computer. We propose a method that utilizes program equivalence checking to discern between code suited for execution on a conventional computer and a quantum computer. This process involves comparing a quantum algorithm's implementation with code written by a programmer, with semantic equivalence between the two implying that the programmer's code should be executed on a quantum computer instead of a conventional computer. Using a novel compiler optimization verification tool named CORK, we test for semantic equivalence between a portion of Shor's algorithm (the “prototype”) and various modified versions of this code (representing the arbitrary code written by a programmer). Some of the modified versions are intended to be semantically equivalent to the prototype while others semantically inequivalent. Our approach is able to correctly determine semantic equivalence or semantic inequivalence in a majority of cases.