Method for guaranteeing program correctness using fine-grained hardware speculative execution

摘要

A method for checking program correctness may include executing a program on a main hardware thread in speculative execution mode on a hardware execution context on a chip having a plurality of hardware execution contexts. In this mode, the main hardware thread's state is not committed to main memory. Correctness checks by a plurality of helper threads are executed in parallel to the main hardware thread. Each helper thread runs on a separate hardware execution context on the chip in parallel with the main hardware thread. The correctness checks determine a safe point in the program up to which the operations executed by the main hardware thread are correct. Once the main hardware thread reaches the safe point, the mode of execution of the main hardware thread is switched to non-speculative. The runtime then causes the main thread to re-enter speculative mode of execution.

主权项

1. A method for checking program correctness, comprising:
executing a program on a main hardware thread in speculative execution mode in which the main hardware thread's state is not committed to main memory, the main hardware thread executed on a hardware execution context in a computer system having a computer chip with a plurality of hardware execution contexts, the main hardware thread executing the program without correctness checks; spawning a plurality of helper threads to perform user selected set of checks, a number of the plurality of helper threads spawned based on at least a size of a region of the program set for checking; executing correctness checks by the plurality of helper threads, each helper thread running on a separate hardware execution context on the chip in parallel with the main hardware thread, wherein the plurality of helper threads execute code and check in a same block of the program the main hardware thread is executing, at least one of the plurality of helper threads running on a second core that is different from a first core that is running the main hardware thread, said plurality of threads determining a safe point in the program up to which said main hardware thread can reach without error at least by checking a multi-valued L2 cache, wherein the multi-valued L2 cache is configured to store multiple different data values for a single address and an L2 directory records a history of which threads have read or written a cache line, and communicating the safe point to a program runtime; and switching the main hardware thread's mode of execution to non-speculative at the safe point, the method further comprising switching back the main hardware thread into speculative execution mode and continuing the executing of correctness checks by the plurality of helper threads until a next safe point is reached, wherein the main hardware thread is switched into non-speculative execution mode.