NDLI: Enforcing resource bounds via static verification of dynamic checks

Content Provider	ACM Digital Library
Author	Espinosa, David Lee, Peter Islam, Nayeem Necula, George C. Chander, Ajay
Copyright Year	2007
Abstract	We show how to limit a program's resource usage in an efficient way, using a novel combination of dynamic checks and static analysis. Usually, dynamic checking is inefficient due to the overhead of checks, while static analysis is difficult and rejects many safe programs. We propose a hybrid approach that solves these problems. We split each resource-consuming operation into two parts. The first is a dynamic check, called reserve. The second is the actual operation, called consume, which does not perform any dynamic checks. The programmer is then free to hoist and combine reserve operations. Combining reserve operations reduces their overhead, while hoisting reserve operations ensures that the program does not run out of resources at an inconvenient time. A static verifier ensures that the program reserves resources before it consumes them. This verification is both easier and more flexible than an a priori static verification of resource usage. We present a sound and efficient static verifier based on Hoare logic and linear inequalities. As an example, we present a version of tar written in Java.
File Format	PDF
ISSN	01640925
e-ISSN	15584593
DOI	10.1145/1275497.1275503
Volume Number	29
Issue Number	5
Journal	ACM Transactions on Programming Languages and Systems (TOPLAS)
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2007-08-02
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Resource bounds Dynamic Static
Content Type	Text
Resource Type	Article
Subject	Software

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

Enforcing Resource Bounds via Static Verification of Dynamic Checks (2005)

Enforcing resource bounds via static verification of dynamic checks (2005)

Enforcing resource bounds via static verification of dynamic checks.

Compositional certified resource bounds

Java bytecode verification via static single assignment form

SUDS:an infrastructure for dynamic software bug detection using static analysis

Enforcing object protocols by combining static and runtime analysis

PolyCheck: dynamic verification of iteration space transformations on affine programs

ABCD:eliminating array bounds checks on demand

Enforcing resource bounds via static verification of dynamic checks

Similar Documents

Enforcing Resource Bounds via Static Verification of Dynamic Checks (2005)

Enforcing resource bounds via static verification of dynamic checks (2005)

Enforcing resource bounds via static verification of dynamic checks.

Compositional certified resource bounds

Java bytecode verification via static single assignment form

SUDS:an infrastructure for dynamic software bug detection using static analysis

Enforcing object protocols by combining static and runtime analysis

PolyCheck: dynamic verification of iteration space transformations on affine programs

ABCD:eliminating array bounds checks on demand

Enforcing resource bounds via static verification of dynamic checks