Heap-bounded assembly language

被引:16
作者
Aspinall, D
Compagnoni, A
机构
[1] Univ Edinburgh, Sch Informat, LFCS, Edinburgh EH9 3JZ, Midlothian, Scotland
[2] Stevens Inst Technol, Dept Comp Sci, Hoboken, NJ 07030 USA
关键词
typed assembly language; proof-carrying code;
D O I
10.1023/B:JARS.0000021014.79255.33
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:261 / 302
页数:42
相关论文
共 36 条
[1]  
[Anonymous], 1990, IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel
[2]  
Appel AndrewW., 2000, P 27 ACM SIGPLAN SIG, P243
[3]  
ASPINALL D, 2002, P ESOP 2002 EUR S PR
[4]  
BAKER HG, 1992, SIGPLAN NOTICES, V27, P89, DOI 10.1145/142137.142162
[5]  
Banerjee A., 1999, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), P88, DOI 10.1109/LICS.1999.782594
[6]  
CRARY K, 1999, P INT C AUT LANG PRO, P40
[7]  
Crary K., 2000, P 27 ACM S PRINC PRO, P184
[8]   LINEAR LOGIC [J].
GIRARD, JY .
THEORETICAL COMPUTER SCIENCE, 1987, 50 (01) :1-102
[9]  
HARPER R, 1995, P 22 ACM S PRINC PRO, P130
[10]  
Hofman M., 2000, Nordic Journal of Computing, V7, P258