Using meta-level compilation to check FLASH protocol code

ABSTRACT

Building systems such as OS kernels and embedded software is difficult. An important source of this difficulty is the numerous rules they must obey: interrupts cannot be disabled for "too long," global variables must be protected by locks, user pointers passed to OS code must be checked for safety before use, etc. A single violation can crash the system, yet typically these invariants are unchecked, existing only on paper or in the implementor's mind.This paper is a case study in how system implementors can use a new programming methodology, metalevel compilation (MC), to easily check such invariants. It focuses on using MC to check for errors in the code used to manage cache coherence on the FLASH shared memory multiprocessor. The only real practical method known for verifying such code is testing and simulation. We show that simple, system-specific checkers can dramatically improve this situation by statically pinpointing errors in the program source. These checkers can be written by implementors themselves and, by exploiting the system-specific information this allows, can detect errors unreachable with other methods. The checkers in this paper found 34 bugs in FLASH code despite the care used in building it and the years of testing it has undergone. Many of these errors fall in the worst category of systems bugs: those that show up sporadically only after days of continuous use. The case study is interesting because it shows that the MC approach finds serious errors in well-tested, non-toy systems code. Further, the code to find such bugs is usually 10-100 lines long, written in a few hours, and exactly locates errors that, if discovered during testing, would require several days of investigation by an experienced implementor.The paper presents 8 checkers we wrote, their application to five different protocol implementations, and a discussion of the errors that we found.

REFERENCES

• 1: M. Bishop and M. Dilger. Checking for race conditions in file accesses. Computing systems, pages 131-152, Spring 1996.
• 2: Robert S. Boyer , Yuan Yu, Automated proofs of object code for a widely used microprocessor, Journal of the ACM (JACM), v.43 n.1, p.166-192, Jan. 1996 [doi>10.1145/227595.227603]
• 3: S. Chandra, M. Dahlia, B. Richards, R. Wang, T. Anderson, and J. Larus. Experience with a language for writing coherence protocols. In Proceedings of the First Conference on Domain Specific Languages, pages 51-65, October 1997.
• 4: 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
• 5: A. Chou and D. Engier. Metal: a language and system for building lightweight, system-specific software checkers, analyzers and optimizers. 2000.
• 6: 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]
• 7: R. F. Crew. ASTLOG: A language for examining abstract syntax trees. In Proceedings of the First Conference on Domain Specific Languages, pages 229-242, October 1997.
• 8: D.L. Detlefs, R.M. Leino, G. Nelson, and J.B. Saxe. Extended static checking. TR SRC-159, COMPAQ SRC, December 1998.
• 9: D. Engler, B. Chelf, A.C. Chou, and S. Hallem. A simple, effective method for checking and optimizing systems using system-specific, programmerwritten compiler extensions. To Appear in Operating Systems Design and Implementation (OSDI) 2000, April 2000.
• 10: D.R. Engler. Incorporating application semantics and control into compilation. In Proceedings of the First Conference on Domain Specij~c Languages, October 1997.
• 11: Dawson R. Engler, Interface Compilation: Steps Toward Compiling Program Interfaces as Languages, IEEE Transactions on Software Engineering, v.25 n.3, p.387-400, May 1999 [doi>10.1109/32.798327]
• 12: R. W. Floyd. Assigning meanings to programs, pages 19-32. J.T. Schwartz, Ed. American Mathematical Society, 1967.
• 13: Christopher W. Fraser , David R. Hanson, A Retargetable C Compiler: Design and Implementation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1995
• 14: Mark Andrew Heinrich , John L. Hennessy, The performance and scalability of distributed shared-memory cache coherence protocols, 1999
• 15: M. Heinrich, D. Ofelt, M. Horowitz, and J. Hennessy. Hardware/software codesign of the stanford flash multiprocessor. Proceedings of the IEEE Special Issue on Hardware/Software Co-design, 85(3), March 1997.
• 16: Mark Heinrich , Vijayaraghavan Soundararajan , John Hennessy , Anoop Gupta, A Quantitative Analysis of the Performance and Scalability of Distributed Shared Memory Cache Coherence Protocols, IEEE Transactions on Computers, v.48 n.2, p.205-217, February 1999 [doi>10.1109/12.752662]
• 17: 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
• 18: Intrinsa. A technical introduction to prefix/enterprise. Technical report, Intrinsa Corporation, 1998.
• 19: A. Kolawa and A. Hicken. Insure++: A tool to support total quality software. http://ww~, parasoft, tom/insure/papers/ tech.htm.
• 20: 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
• 21: T. Lord. Application specific static code checking for C programs: Ctool. In ~twaddle: A Digital Zine (version 1.0), 1997.
• 22: K.L. McMillan and J. Schwalbe. Formal verification of the gigamax cache consistency protocol. In Proceedings of the International Symposium on Shared Memory Multiprocessing, pages 242-51. Tokyo, Japan Inf. Process. Soc., 1991.
• 23: Todd C. Mowry , Angela K. Demke , Orran Krieger, Automatic compiler-inserted I/O prefetching for out-of-core applications, Proceedings of the second USENIX symposium on Operating systems design and implementation, p.3-17, October 29-November 01, 1996, Seattle, Washington, United States
• 24: G. Nelson. Techniques for program verification. Available as Xerox PARC Research Report CSL- 81-10, June, 1981, Stanford University, 1981.
• 25: 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]
• 26: Stefan Savage , Michael Burrows , Greg Nelson , Patrick Sobalvarro , Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, ACM Transactions on Computer Systems (TOCS), v.15 n.4, p.391-411, Nov. 1997 [doi>10.1145/265924.265927]
• 27: Vijayaraghavan Soundararajan , Mark Heinrich , Ben Verghese , Kourosh Gharachorloo , Anoop Gupta , John Hennessy, Flexible use of memory for replication/migration in cache-coherent DSM multiprocessors, Proceedings of the 25th annual international symposium on Computer architecture, p.342-355, June 27-July 02, 1998, Barcelona, Spain
• 28: 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
• 29: 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

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS
      K.6.1 Project and People Management
          Subjects: Systems analysis and design