A simple method for extracting models for protocol code

ABSTRACT

The use of model checking for validation requires that models of the underlying system be created. Creating such models is both difficult and error prone and as a result, verification is rarely used despite its advantages. In this paper, we present a method for automatically extracting models from low level software implementations. Our method is based on the use of an extensible compiler system, xg++, to perform the extraction. The extracted model is combined with a model of the hardware, a description of correctness, and an initial state. The whole model is then checked with the Murϕ model checker. As a case study, we apply our method to the cache coherence protocols of the Stanford FLASH multiprocessor. Our system has a number of advantages. First, it reduces the cost of creating models, which allows model checking to be used more frequently. Second, it increases the effectiveness of model checking since the automatically extracted models are more accurate and faithful to the underlying implementation. We found a total of 8 errors using our system. Two errors were global resource errors, which would be difficult to find through any other means. We feel the approach is applicable to other low level systems.

REFERENCES

• 1: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 2: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 3: T. Ball and S. K. Rajamani. Checking temporal properties of software with boolean programs. In Proc. of the Workshop on Advances in Verification (with CAV 2000), 2000.
• 4: Satish Chandra , Bradley Richards , James R. Larus, Teapot: A Domain-Specific Language for Writing Cache Coherence Protocols, IEEE Transactions on Software Engineering, v.25 n.3, p.317-333, May 1999 [doi>10.1109/32.798322]
• 5: S. Chiba. Open C++ programmer's guide. Technical Report TR93-93-3, Dept. of information science, University of Tokyo, 1993.
• 6: Shigeru Chiba, A metaobject protocol for C++, Proceedings of the tenth annual conference on Object-oriented programming systems, languages, and applications, p.285-299, October 15-19, 1995, Austin, Texas, United States
• 7: Andy Chou , Benjamin Chelf , Dawson Engler , Mark Heinrich, Using meta-level compilation to check FLASH protocol code, Proceedings of the ninth international conference on Architectural support for programming languages and operating systems, p.59-70, November 2000, Cambridge, Massachusetts, United States
• 8: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 9: R. E Crew. ASTLOG: A language for examining abstract syntax trees. In Proc. of the First Conf. on Domain Specific Languages, pages 229-242, Oct. 1997.
• 10: D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proc. of the 4th Symp. on Operating Systems Design and Implementation (OSDI 2000), pages 23- 25, Sept. 2000.
• 11: Ásgeir Th. Eiríksson , Kenneth L. McMillan, Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study, Proceedings of the 7th International Conference on Computer Aided Verification, p.367-380, July 03-05, 1995
• 12: Jeanne Ferrante , Karl J. Ottenstein , Joe D. Warren, The program dependence graph and its use in optimization, ACM Transactions on Programming Languages and Systems (TOPLAS), v.9 n.3, p.319-349, July 1987 [doi>10.1145/24039.24041]
• 13: Mark Andrew Heinrich , John L. Hennessy, The performance and scalability of distributed shared-memory cache coherence protocols, 1999
• 14: Gerard J. Holzmann , Margaret H. Smith, Software Model Checking, Proceedings of the IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), p.481-497, October 05-08, 1999
• 15: J. Kuskin , D. Ofelt , M. Heinrich , J. Heinlein , R. Simoni , K. Gharachorloo , J. Chapin , D. Nakahira , J. Baxter , M. Horowitz , A. Gupta , M. Rosenblum , J. Hennessy, The Stanford FLASH multiprocessor, Proceedings of the 21ST annual international symposium on Computer architecture, p.302-313, April 18-21, 1994, Chicago, Illinois, United States
• 16: T. Lord. Application specific static code checking for C programs: Ctool. In -twaddle: A Digital Zine (version 1.0), 1997.
• 17: K. McMillan and J. Schwalbe. Formal verification of the gigamax cache consistency protocol. In Proc. of the Intl. Syrup. on Shared Memory Multiprocessing ( ISSMM91), pages 242-251. Tokyo, Japan Inf. Process. Soc., 1991.
• 18: G. Nelson. Techniques f or program verification. Available as Xerox PARC Research Report CSL-81-10, June, 1981, Stanford University, 1981.
• 19: Seungjoon Park , David L. Dill, Verification of FLASH cache coherence protocol by aggregation of distributed transactions, Proceedings of the eighth annual ACM symposium on Parallel algorithms and architectures, p.288-296, June 24-26, 1996, Padua, Italy [doi>10.1145/237502.237573]
• 20: Amitabh Srivastava , Alan Eustace, ATOM: a system for building customized program analysis tools, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.196-205, June 20-24, 1994, Orlando, Florida, United States
• 21: Ulrich Stern , David L. Dill, Automatic verification of the SCI cache coherence protocol, Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, p.21-34, October 02-04, 1995
• 22: E Tip. A survey of program slicing techniques. Journal of Programming Languages, 3(3): 121-189, September 1995.
• 23: M. Weiser. Program slicing. IEEE Transactions on Software Engineering, 10(4):352-357, July 1984.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.3 MEMORY STRUCTURES
      B.3.2 Design Styles
          Subjects: Shared memory

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS

  I. Computing Methodologies
  I.6 SIMULATION AND MODELING

General Terms:
Design, Measurement, Performance, Reliability, Standardization, Theory