Zilles. Formally defining and verifying master/slave speculative parallelization

Abstract. Master/Slave Speculative Parallelization (MSSP) is a new paradigm aiming at decoupling performance and correctness in microprocessor design and implementation. It is based on the idea that a speculative master processor splits the code and distributes tasks to independent slave processors, which can commit their results only under specific conditions. This work reports the first steps in our efforts to formally validate the MSSP paradigm. We describe three levels of jumping refinement in its design, each preserving its equivalence to a sequential machine, that is, equivalence observed at specific places of interest in the code. Formalizing MSSP facilitated a deeper understanding of the subtle performance vs. correctness trade-offs and, most importantly, revealed all the implementation-independent assumptions underpinning MSSP’s correctness. We found these aspects so valuable that we plan to advance MSSP’s formalization in parallel with its design in order to guide us towards correct choices, rather than as a “post-mortem ” exercise with the only goal of finding errors in an already existing design.