[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
article
Free access

Using meta-level compilation to check FLASH protocol code

Published: 01 November 2000 Publication History

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]
R. S. Boyer and Y. Yu. Automated proofs of object code for a widely used microprocessor. Journal of the ACM, 1(43):166-192, January 1996.]]
[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]
S. Chiba. A metaobject protocol for C-t-+. In OOP- SLA 1995 Conference Proceedings Object.oriented programming systems, languages, and applications, pages 285-299, October 1995.]]
[5]
A. Chou and D. Engier. Metal: a language and system for building lightweight, system-specific software checkers, analyzers and optimizers. 2000.]]
[6]
J.C. Corbett, M.B. Dwyer, J. Hatcliff, S. Laubach, C.S. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from java source code. In ICSE ~000, 2000.]]
[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]
D.R. Engler. Interface compilation: Steps toward compiling program interfaces as languages. IEEE Transactions on Software Engineering, 25(3):387- 400, May/June 1999.]]
[12]
R. W. Floyd. Assigning meanings to programs, pages 19-32. J.T. Schwartz, Ed. American Mathematical Society, 1967.]]
[13]
C. W. Fraser and D. R. Hanson. A retargetable C compiler: design and implementation. Benjamin/Cummings Publishing Co., Redwood City, CA, 1995.]]
[14]
M. Heinrich. The Performance and Scalability of Distributed Shared Memory Cache Coherence Protocols. PhD thesis, Stanford .University, October 1998.]]
[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]
M. Heinrich, R. Soundararajan, J. Hennessy, and A. Gupta. A quantitatitve analysis of the performance and scalability of distributed shared memory cache coherence protocols. IEEE Transactions on Computers, 48(2):205-217, February 1999. Special Issue on Cache Memory and Related Problems.]]
[17]
G. Holzmann and M. Smith. Software model checking: Extracting verification models from source code. In Invited Paper. Proc. PSTV/FORTE99 Publ. Kluwer, 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, and J. Hennessy. The Stanford FLASH multiprocessor. In Proceedings of the 21st International Symposium on Computer Architecture, April 1994.]]
[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]
T.C. Mowry, A.K. Demke, and O. Krieger. Automatic compiler-inserted I/O prefetching for outof-core applications. In Proceedings of the Second Symposium on Operating Systems Design and Implementation, 1996.]]
[24]
G. Nelson. Techniques for program verification. Available as Xerox PARC Research Report CSL- 81-10, June, 1981, Stanford University, 1981.]]
[25]
S. Park and D.L. Dill. Verification of FLASH cache coherence protocol by aggregation of distributed transactions. In Proceedings of the 8th A CM Symposium on 'Parallel Algorithsm and Architectures, pages 288-296, June 1996.]]
[26]
S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, and T.E. Anderson. Eraser: A dynamic data race detector for multithreaded programs. A CM Transactions on Computer Systems, 15(4):391-411, 1997.]]
[27]
R. Soundararajan, M. Heinrich, B. Verghese, and et al. Flexible use of memory for replication/migration in cache-coherent dsm multiprocessots. In Proceedings of the P5th International Symposium on Computer Architecture, June 1998.]]
[28]
A. Srivastava and A. Eustace. ATOM - a system for building customized program analysis tools. In Proceedings of the SIGPLAN '94 Conference on Programming Language Design and Implementation, 1994.]]
[29]
U. Stern and D.L. Dill. Automatic verification of the SCI cache coherence protocol. In Correct Hardware Design and Verification Methods: IFIP WGIO.5 Advanced Research Working Conference Proceedings, 1995.]]

Cited By

View all
  • (2012)Understanding and detecting real-world performance bugsACM SIGPLAN Notices10.1145/2345156.225407547:6(77-88)Online publication date: 11-Jun-2012
  • (2002)C Wolf - A Toolset for Extracting Models from C ProgramsProceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems10.5555/646220.682194(260-275)Online publication date: 11-Nov-2002
  • (2002)C Wolf - A Toolset for Extracting Models from C ProgramsFormal Techniques for Networked and Distributed Sytems — FORTE 200210.1007/3-540-36135-9_17(260-275)Online publication date: 5-Nov-2002

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 35, Issue 11
Nov. 2000
269 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/356989
Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2000
Published in SIGPLAN Volume 35, Issue 11

Check for updates

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)32
  • Downloads (Last 6 weeks)4
Reflects downloads up to 01 Jan 2025

Other Metrics

Citations

Cited By

View all
  • (2012)Understanding and detecting real-world performance bugsACM SIGPLAN Notices10.1145/2345156.225407547:6(77-88)Online publication date: 11-Jun-2012
  • (2002)C Wolf - A Toolset for Extracting Models from C ProgramsProceedings of the 22nd IFIP WG 6.1 International Conference Houston on Formal Techniques for Networked and Distributed Systems10.5555/646220.682194(260-275)Online publication date: 11-Nov-2002
  • (2002)C Wolf - A Toolset for Extracting Models from C ProgramsFormal Techniques for Networked and Distributed Sytems — FORTE 200210.1007/3-540-36135-9_17(260-275)Online publication date: 5-Nov-2002

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media