Interim is a statically-typed, low-level dialect of Lisp featuring compile-time, GC-free memory management.
Interim is a technology demonstrator for compile-time memory management using regions. As of 2018, the only major language with compile-time memory management is Rust, which is notoriously tough to learn. Interim was built to prove that sound, GC-free, compile-time memory management can be both simple to implement and easy to learn and use.
Memory safety is achieved by preventing three classes of errors:
NULL
pointers- Double
free()
- Use after
free()
(dangling pointers)
Preventing NULL
pointers is easy: we use an option type (called Maybe
in
Haskell). In the case of Interim, we have a special pointer type called
nullable
which represents a pointer which is potentially NULL
. The case
construct can be used to extract a never-NULL
pointer in a safe way.
Preventing double free()
and use after free()
errors is harder, and this is
where regions come in.
Consider this code:
(letregion rho
(let ((p (allocate rho 10)))
(letregion rho'
(let ((p' (allocate rho' 12)))
nil))))
What we're doing here is:
-
Defining a region
rho
. Regions are both lexical objects and run-time values. -
Defining a variable
p
, whose initial value is the result of allocating the number 10 in the regionrho
.An
allocate
call takes a value of typeT
and a region indentifier, allocates enough memory in the region to hold that value, and returns a pointer to it. The result pointer has the type(nullable T R)
, whereT
is the type of the value we're allocating andR
is the region identifier. -
Defining a new region
rho'
. -
Defining a new variable
p'
, whose initial value is(allocate rho' 12)
, that is, the result of allocating the value12
in the regionrho'
. -
Finally, return
nil
.
Now notice what happens if we try to store p'
in p
:
(letregion rho
(let ((p (allocate rho 10)))
(letregion rho'
(let ((p' (allocate rho' 12)))
(<- p p')))))
The compiler will fail with
Cannot assign to variable 'p': the type of the variable is (nullable i32 rho),
while the type of the expression is (nullable i32 rho')
This is the key to preventing dangling pointer errors: pointers are tagged with the region they belong to. A pointer cannot escape its lifetime, to a higher-up region or to a global variable, because the types won't match.
Double free()
errors are prevented through a straightforward feature of
regions: there is no way to do a manual free()
, and everything in a region is
freed automatically when exiting the region's body.
For more examples, look in the examples/
directory.
(defun main () i32
(println "Hello, world!")
0)
(defun fib ((n i32)) i32
(if (< n 2)
n
(+ (fib (- n 1))
(fib (- n 2)))))
(defun main () i32
(print "fib(30) = ")
(println (fib 30))
0)
Output:
fib(30) = 832040
(defun main () i32
(letregion rho
(let ((p (allocate rho 10)))
(case p
((not-null p')
(print "Allocated successfully! Value: ")
(println (load p'))
0)
(null
(println "Out of memory!")
-1)))))
Output:
Allocated successfully! Value: 10
You need MLton, git and make to build Interim. On Ubuntu:
$ sudo apt-get install mlton git make
Then:
$ make interim
After building, try
$ make examples
The only dependency is Parsimony, a parser combinator library.
Being a technology demonstrator, Interim lacks many features of real languages: modules, macros, higher-order functions, and higher-order types are not implemented since the focus is on region-based memory management.
As the name implies, Interim is a stepping stone or proof of concept for a larger, more sophisticated language.
-
Grossman, Dan, Greg Morrisett, Trevor Jim, Michael Hicks, Yanling Wang, and James Cheney. "Region-based memory management in Cyclone." ACM Sigplan Notices 37, no. 5 (2002): 282-293.
-
Swamy, Nikhil, Michael Hicks, Greg Morrisett, Dan Grossman, and Trevor Jim. "Safe manual memory management in Cyclone." Science of Computer Programming 62, no. 2 (2006): 122-144.
-
Gay, David, and Alex Aiken. Memory management with explicit regions. Vol. 33, no. 5. ACM, 1998.
Copyright 2018 Fernando Borretti.
Licensed under the GPLv3 license. See the COPYING file for details.