A resource semantics and abstract machine for Safe: A functional language with regions and explicit deallocation

In this paper we summarise Safe, a first-order functional language for programming small devices and embedded systems with strict memory requirements, which has been introduced elsewhere. It has some unusual memory management features such as heap regions and explicit cell deallocation. It is target...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2014-04, Vol.235, p.3-35
Main Authors: Montenegro, Manuel, Peña, Ricardo, Segura, Clara
Format: Article
Language:English
Subjects:
Abstract machines
Certifying compilers
Code generation
Functional languages
Memory management
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:In this paper we summarise Safe, a first-order functional language for programming small devices and embedded systems with strict memory requirements, which has been introduced elsewhere. It has some unusual memory management features such as heap regions and explicit cell deallocation. It is targeted at a Proof Carrying Code environment, and consistently with this aim the Safe compiler provides machine checkable certificates about important safety properties such as the absence of dangling pointers and bounded memory consumption. The kernel of the paper is devoted to developing part of the Safe compiler's back-end, by deriving an appropriate abstract machine from the language semantics, by providing the code generation functions, and by formally proving that the translation is sound, both in the semantic and in the memory consumption senses.
ISSN:0890-5401
1090-2651
DOI:10.1016/j.ic.2014.01.003