Certifying compilation for a language with stack allocation

This paper describes an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is...

Full description

Saved in:
Bibliographic Details
Main Authors: Jia, L., Spalding, F., Walker, D., Glew, N.
Format: Conference Proceeding
Language:English
Subjects:
Assembly systems
Automatic logic units
Computer science
Data structures
High level languages
Memory management
Safety
Shape
System testing
Utility programs
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This paper describes an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is a tree of "stack tags" that tracks the evolution of the stack over time. To demonstrate the expressiveness of the type system, we define Micro-CLI, a simple imperative language that captures the essence of stack allocation in the common language infrastructure. We show how to compile well-typed Micro-CLI into well-typed assembly.
ISSN:1043-6871
2575-5528
DOI:10.1109/LICS.2005.9