Recognition of logically related regions based heap abstraction

DOI10.1016/J.JOEMS.2011.12.011MaRDI QIDQ1942939zbMATH OpenOpenAlexFDO

Authors Mohamed A. El-Zawawy

Publication date 14 March 2013

Published in Journal of the Egyptian Mathematical Society (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://arxiv.org/abs/1212.5094

zbMATH Keywords

data structuresheap abstractionobject co-locationpool allocationregion-based garbage collectionstatic deallocation

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Graph theory (including graph drawing) in computer science (68R10) Nonnumerical algorithms (68W05)

Abstract: This paper presents a novel set of algorithms for heap abstraction, identifying logically related regions of the heap. The targeted regions include objects that are part of the same component structure (recursive data structure). The result of the technique outlined in this paper has the form of a compact normal form (an abstract model) that boosts the efficiency of the static analysis via speeding its convergence. The result of heap abstraction, together with some properties of data structures, can be used to enable program optimizations like static deallocation, pool allocation, region-based garbage collection, and object co-location. More precisely, this paper proposes algorithms for abstracting heap components with the layout of a singly linked list, a binary tree, a cycle, and a directed acyclic graph. The termination and correctness of these algorithms are studied in the paper. Towards presenting the algorithms the paper also presents concrete and abstract models for heap representations.

Recommendations

• Automatic numeric abstractions for heap-manipulating programs
• scientific article; zbMATH DE number 2090862
• Static Analysis
• Recency-Abstraction for Heap-Allocated Storage
• Verification, Model Checking, and Abstract Interpretation

Cites work

• An axiomatic basis for computer programming
• From flow logic to static type systems for coordination languages
• scientific article; zbMATH DE number 1948399 (Why is no real title available?)
• scientific article; zbMATH DE number 1953280 (Why is no real title available?)
• Program and proof optimizations with type systems
• Semi-sparse flow-sensitive pointer analysis
• Simple relational correctness proofs for static analyses and program transformations
• Type systems equivalent to data-flow analyses for imperative languages

Cited in

(2)

• scientific article; zbMATH DE number 2090862 (Why is no real title available?)
• Liberate abstract garbage collection from the stack by decomposing the heap

This page was built for publication: Recognition of logically related regions based heap abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1942939)