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.
This work was supported in part by a grant from Intel and National Science Foundation grants CCR-0311340 and CCF-0347260.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Arvind, Shen, X.: Using term rewriting systems to design and verify processors. IEEE Micro 9(3), 36–46 (1999)
Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: Maude 2.0 Manual (2003), http://maude.cs.uiuc.edu/manual
Clavel, M., Durán, F., Eker, S., Meseguer, J.: Building equational proving tools by reflection in rewriting logic. In: CAFE: An Industrial-Strength Algebraic Formal Method. Elsevier, Amsterdam (2000)
Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: Proc. IEEE International Conference on Computer Design: VLSI in Computers and Processors, October 1992, pp. 522–525 (1992)
Lamport, L.: What good is temporal logic? In: Information Processing 1983: Proc. IFIP 9th World Congress, September 1983, pp. 657–668 (1983)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Salverda, P., Roşu, G., Zilles, C.: Maude formalization of MSSP, http://fsl.cs.uiuc.edu/mssp
Salverda, P., Zilles, C.: Formal verification of MSSP. Technical Report UIUCDCS-R-2003-2384, University of Illinois at Urbana-Champaign (December 2003)
Sawada, J., Hunt, W.A.: Trace table based approach for pipelined microprocessor verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 364–375. Springer, Heidelberg (1997)
Sawada, J., Hunt, W.A.: Processor verification with precise exceptions and speculative execution. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 135–146. Springer, Heidelberg (1998)
Sohi, G., Breach, S., Vijaykumar, T.: Multiscalar processors. In: Proc. 22nd Annual International Symposium on Computer Architecture, June 1995, pp. 414–425 (1995)
Zilles, C.: Master/slave speculative parallelization and approximate code. PhD thesis, University of Winsconsin - Madison (2002)
Zilles, C., Sohi, G.: Master/slave speculative parallelization. In: Proc. 35th Annual ACM/IEEE International Symposium on Microarchitecture, November 2002, pp. 85–96 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Salverda, P., Roşu, G., Zilles, C. (2005). Formally Defining and Verifying Master/Slave Speculative Parallelization. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_10
Download citation
DOI: https://doi.org/10.1007/11526841_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)