Access analysis-based tight localization of abstract memories

Hakjoo Oh, Lucas Brutschy, Kwangkeun Yi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Citations (Scopus)

Abstract

On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called "abstract garbage collection" or "framing". In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable. Our technique first estimates, by an efficient pre-analysis, the set of locations that will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure's body and reduces the average analysis time and memory by 92.1% and 71.2%, respectively, without sacrificing the analysis precision. Localizing more frequently such as at loop bodies and basic blocks as well as procedure bodies, the generalized localization additionally reduces analysis time by an average of 31.8%.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings
Pages356-370
Number of pages15
DOIs
Publication statusPublished - 2011 Feb 1
Externally publishedYes
Event12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011 - Austin, TX, United States
Duration: 2011 Jan 232011 Jan 25

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6538 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011
CountryUnited States
CityAustin, TX
Period11/1/2311/1/25

Fingerprint

Data storage equipment
Block codes
Block Codes
Garbage Collection
Abstract Interpretation
Reachability
Subset
Estimate
Experiments
Experiment

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Oh, H., Brutschy, L., & Yi, K. (2011). Access analysis-based tight localization of abstract memories. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings (pp. 356-370). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6538 LNCS). https://doi.org/10.1007/978-3-642-18275-4_25

Access analysis-based tight localization of abstract memories. / Oh, Hakjoo; Brutschy, Lucas; Yi, Kwangkeun.

Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. 2011. p. 356-370 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6538 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Oh, H, Brutschy, L & Yi, K 2011, Access analysis-based tight localization of abstract memories. in Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6538 LNCS, pp. 356-370, 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2011, Austin, TX, United States, 11/1/23. https://doi.org/10.1007/978-3-642-18275-4_25
Oh H, Brutschy L, Yi K. Access analysis-based tight localization of abstract memories. In Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. 2011. p. 356-370. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-18275-4_25
Oh, Hakjoo ; Brutschy, Lucas ; Yi, Kwangkeun. / Access analysis-based tight localization of abstract memories. Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings. 2011. pp. 356-370 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{985617f7a23540398a08d57f9e6972fc,
title = "Access analysis-based tight localization of abstract memories",
abstract = "On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called {"}abstract garbage collection{"} or {"}framing{"}. In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable. Our technique first estimates, by an efficient pre-analysis, the set of locations that will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure's body and reduces the average analysis time and memory by 92.1{\%} and 71.2{\%}, respectively, without sacrificing the analysis precision. Localizing more frequently such as at loop bodies and basic blocks as well as procedure bodies, the generalized localization additionally reduces analysis time by an average of 31.8{\%}.",
author = "Hakjoo Oh and Lucas Brutschy and Kwangkeun Yi",
year = "2011",
month = "2",
day = "1",
doi = "10.1007/978-3-642-18275-4_25",
language = "English",
isbn = "9783642182747",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "356--370",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings",

}

TY - GEN

T1 - Access analysis-based tight localization of abstract memories

AU - Oh, Hakjoo

AU - Brutschy, Lucas

AU - Yi, Kwangkeun

PY - 2011/2/1

Y1 - 2011/2/1

N2 - On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called "abstract garbage collection" or "framing". In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable. Our technique first estimates, by an efficient pre-analysis, the set of locations that will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure's body and reduces the average analysis time and memory by 92.1% and 71.2%, respectively, without sacrificing the analysis precision. Localizing more frequently such as at loop bodies and basic blocks as well as procedure bodies, the generalized localization additionally reduces analysis time by an average of 31.8%.

AB - On-the-fly localization of abstract memory states is vital for economical abstract interpretation of imperative programs. Such localization is sometimes called "abstract garbage collection" or "framing". In this article we present a new memory localization technique that is more effective than the conventional reachability-based approach. Our technique is based on a key observation that collecting the reachable memory parts is too conservative and the accessed parts are usually tiny subsets of the reachable. Our technique first estimates, by an efficient pre-analysis, the set of locations that will be accessed during the analysis of each code block. Then the main analysis uses the access-set results to trim the memory entries before analyzing code blocks. In experiments with an industrial-strength global C static analyzer, the technique is applied right before analyzing each procedure's body and reduces the average analysis time and memory by 92.1% and 71.2%, respectively, without sacrificing the analysis precision. Localizing more frequently such as at loop bodies and basic blocks as well as procedure bodies, the generalized localization additionally reduces analysis time by an average of 31.8%.

UR - http://www.scopus.com/inward/record.url?scp=79251582841&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79251582841&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-18275-4_25

DO - 10.1007/978-3-642-18275-4_25

M3 - Conference contribution

SN - 9783642182747

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 356

EP - 370

BT - Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Proceedings

ER -