Abstract
The verification of increasingly complex multiprocessor systems has become a formidable challenge. Given the complexity of each of the multi-processor components and the complex interactions between them, simulation may no longer provide the desired level of coverage to detect possible starvation and deadlocks. The Formal Verification Group at Hewlett-Packard has used a combination of model checking and theorem proving techniques with great effect to analyse the correctness of the Runway bus arbitration protocols in models representing several members of the HP 9000 K-CLASS servers and J-CLASS workstations. This paper presents some basic ideas behind this verification methodology, highlights its strengths and shortcomings, and discusses how it can be used to enhance the existing system-verification methodology.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bryg W., Chan K., Fiduccia N., ‘A High-Performance, Low-Cost Multiprocessor Bus for Workstations and Midrange Servers', Hewlett-Packard Journal, 47 (l), February 1996.
Bainbridge S., Camilleri A., Fleming R., ‘Theorem Proving as an Industrial Tool for System Level Design', in Theorem Provers in Circuit Design, Stavridou V., Melham T., Boute R. (eds.), North-Holland, 1992, pp. 253–274, Proceedings of the IFIP TC 10/WG 10.2 International Conference, Nijmegen, 22–24 June, 1992.
Camilleri A., Fleming R., Odineal R., Prekeges D., ‘Formal Verification of Liveness of a Multi-Processor Bus Protocol', pp. 409–412, Proceedings of the 1993 HP Design Technology Conference, Portland, 25–28 May, 1993. HP Confidential.
Corella F., Shaw R., Zhang C., ‘A formal proof of absence of deadlock for any acyclic network of PCI buses', Proceedings of 13th International Conference on Computer Hardware Description Languages and their Applications, Chapman & Hall, 1997.
Datamation Magazine, February 1997.
Gordon M. J. C., Melham T. F., Introduction to HOL — A theorem proving environment for higher order logic, Cambridge University Press, 1993.
Harkness C., Wolf, E., ‘Verifying the Summit Bus Converter Protocols with Symbolic Model Checking', Formal Methods in System Design, 4 (2), pp. 83–97, February 1994.
Hennessy J., Patterson D., Computer Architecture: A Quantitative Approach, Morgan Kaufmann Publishers, Inc., 1990.
McMillan K. L., Symbolic Model Checking, Kluwer Academic Publishers, 1993.
McMillan K. L., Schwalbe J., ‘Formal Verification of the Encore Gigamax Cache Consistency Protocol', in International Symposium on Shared Memory Multiprocessors, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Camilleri, A.J. (1997). A hybrid approach to verifying liveness in a symmetric multi-processor. In: Gunter, E.L., Felty, A. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1997. Lecture Notes in Computer Science, vol 1275. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028385
Download citation
DOI: https://doi.org/10.1007/BFb0028385
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63379-2
Online ISBN: 978-3-540-69526-4
eBook Packages: Springer Book Archive