Formal Verification of MSSP

MSSP is a new execution paradigm that achieves high performance by removing correctness constraints from the critical path. A collection of concurrently executing slave processors, which are not on the critical path, check the operation of a single master processor, whose execution is on the critical path, but is fast because it need not be correct. This report formally verifies that such an execution model works, in the sense that it correctly achieves a sequential execution of the application code. We describe abstract models of both the sequential and MSSP execution paradigms, and distill from these the fundamental aspects of functionality that are needed to establish their equivalence. The verification itself is an iterative process. We begin with a number of high-level assumptions, which we use to prove some very basic results, and then successively refine our formalisms to argue that our initial assumptions are indeed reasonable. In formally reasoning about MSSP, we achieve a number of goals. First, and most importantly, we demonstrate that MSSP is indeed equivalent to sequential execution. Second, we derive an abstract model of MSSP execution, which permits us to distill the fundamental properties of an MSSP machine that are necessary for correct operation. Having thus enumerated those properties, we facilitate reasoning about the impacts on correctness (and hence the feasibility) of new design ideas. Finally, we show that operation of the master---which is not guaranteed to be correct---does not compromise overall correctness. We thus demonstrate that an architecture in which performance and correctness are pursued as distinct design goals is indeed viable, at least from the point of view of maintaining correctness irrespective of the activity of the performance sub-component