Heap-Bounded Assembly Language

David Aspinall, Adriana Compagnoni

Research output: Contribution to journalArticlepeer-review

Abstract

We present a first-order linearly typed assembly language, HBAL, that allows the safe reuse of heap space for elements of different types. Linear typing ensures the single pointer property, disallowing aliasing but allowing safe, in-place-update compilation of programming languages. We prove that HBAL is sound for a low-level untyped model of the machine, using a satisfiability relation that captures when a location correctly models a value of some type. This interpretation is closer to the machine than previous abstract machines used for typed assembly language models, and we separate typing of the store from an untyped operational semantics of programs, as would be required for proof-carrying code. Our ultimate aim is to design a family of assembly languages that have high-level typing features for expressing resource-bound constraints. We want to link the assembly-level with high-level languages expressing similar constraints, to provide end-to-end guarantees and a viable framework for proof-carrying code. HBAL is a first exemplifying step in this direction. It is designed as a target low-level language for Hofmann's LFPL language. Programs written in LFPL run in a bounded amount of heap space, and this property carries over when they are compiled to HBAL: the resulting program does not allocate store or assume an external garbage collector. Following LFPL, we include a special diamond resource type that stands for a unit of heap space of uncommitted type.
Original languageEnglish
Pages (from-to)261-302
Number of pages42
JournalJournal of Automated Reasoning
Volume31
Issue number3-4
DOIs
Publication statusPublished - 2003

Keywords

  • typed assembly language
  • proof-carrying code

Fingerprint Dive into the research topics of 'Heap-Bounded Assembly Language'. Together they form a unique fingerprint.

Cite this