Formally defining and verifying Master/Slave Speculative Parallelization

Pierre Salverda, Grigore Roşu, Craig Zilles

Research output: Contribution to journalConference article

Abstract

Master/Slave Speculative Parallelization (MSSP) is a new execution paradigm that decouples the issues of performance and correctness in microprocessor design and implementation. MSSP uses a fast, not necessarily correct, master processor to speculatively split a program into tasks, which are executed independently and concurrently on slower, but correct, slave processors. This work reports on the first steps in our efforts to formally validate that overall correctness can be achieved in MSSP despite a lack of correctness guarantees in its performance-critical parts. We describe three levels of an abstract model for MSSP, each refining the next and each preserving equivalence to a sequential machine. Equivalence is established in terms of a jumping refinement, a notion we introduce to describe equivalence at specific places of interest in the code. We also report on experiences and insights gained from this exercise. In particular, we show how formalizing MSSP facilitated a deeper understanding of performance-correctness decoupling and its attendant trade-offs, all key features of the MSSP paradigm. Moreover, formalization revealed all assumptions underpinning correctness, which, being specified abstractly, can be understood in an implementation-independent way. We found these results so valuable that we plan to advance MSSP's formalization in parallel with its subsequent design iterations.

Original languageEnglish (US)
Pages (from-to)123-138
Number of pages16
JournalLecture Notes in Computer Science
Volume3582
DOIs
StatePublished - Jan 1 2005
EventInternational Symposium of Formal Methods Europe, FM 2005 - Newcastle, United Kingdom
Duration: Jul 18 2005Jul 22 2005

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Formally defining and verifying Master/Slave Speculative Parallelization'. Together they form a unique fingerprint.

  • Cite this