Formal Verification of MSSP

Salverda, Pierre M.; Zilles, Craig

Permalink

https://hdl.handle.net/2142/10770 Copy

Description

Title

Formal Verification of MSSP

Author(s)

• Salverda, Pierre M.
• Zilles, Craig

Issue Date

2003-12

Keyword(s)

• parallel computing
• execution models

Abstract

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.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/10770

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections