NDLI: Using meta-level compilation to check FLASH protocol code (OPSR, Vol. 34, Issue. 5)

Content Provider	ACM Digital Library
Author	Engler, Dawson Chou, Andy Chelf, Benjamin Heinrich, Mark
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, meta-level 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.
Starting Page	59
Ending Page	70
Page Count	12
File Format	PDF
ISSN	01635980
DOI	10.1145/384264.379002
Journal	ACM SIGOPS Operating Systems Review (OPSR)
Volume Number	34
Issue Number	5
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1975-04-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Content Type	Text
Resource Type	Article
Subject	Computer Networks and Communications Hardware and Architecture Information Systems

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Using meta-level compilation to check FLASH protocol code (CARN, Vol. 28, Issue. 5)

Effective null pointer check elimination utilizing hardware trap (OPSR, Vol. 34, Issue. 5)

FLASH vs. (Simulated) FLASH:closing the simulation loop (OPSR, Vol. 34, Issue. 5)

Communication scheduling (OPSR, Vol. 34, Issue. 5)

Power aware page allocation (OPSR, Vol. 34, Issue. 5)

Architecture and design of AlphaServer GS320 (OPSR, Vol. 34, Issue. 5)

System architecture directions for networked sensors (OPSR, Vol. 34, Issue. 5)

Designing computer systems with MEMS-based storage (OPSR, Vol. 34, Issue. 5)

Thread-level parallelism and interactive performance of desktop applications (OPSR, Vol. 34, Issue. 5)

Using meta-level compilation to check FLASH protocol code (OPSR, Vol. 34, Issue. 5)

Similar Documents

Using meta-level compilation to check FLASH protocol code (CARN, Vol. 28, Issue. 5)

Effective null pointer check elimination utilizing hardware trap (OPSR, Vol. 34, Issue. 5)

FLASH vs. (Simulated) FLASH:closing the simulation loop (OPSR, Vol. 34, Issue. 5)

Communication scheduling (OPSR, Vol. 34, Issue. 5)

Power aware page allocation (OPSR, Vol. 34, Issue. 5)

Architecture and design of AlphaServer GS320 (OPSR, Vol. 34, Issue. 5)

System architecture directions for networked sensors (OPSR, Vol. 34, Issue. 5)

Designing computer systems with MEMS-based storage (OPSR, Vol. 34, Issue. 5)

Thread-level parallelism and interactive performance of desktop applications (OPSR, Vol. 34, Issue. 5)

Using meta-level compilation to check FLASH protocol code (OPSR, Vol. 34, Issue. 5)