Linear types for aliased resources

Linear types for aliased resources. Chris Hawblitzel.

Type systems that track aliasing can verify state-dependent program properties. For example, such systems can verify that a program does not access a resource after deallocating the resource. The simplest way to track aliasing is to use linear types, which on the surface appear to ban the aliasing of linear resources entirely. Since banning aliasing is considered too draconian for many practical programs, researchers have proposed type systems that allow limited forms of aliasing, without losing total control over state-dependent properties. This paper describes how to encode one such system, the capability calculus, using a type system based on plain linear types with no special support for aliasing. Given well-typed capability calculus source programs, the encodings produce well-typed target programs based on linear types. These encodings demonstrate that, contrary to common expectations, linear type systems can express aliasing of linear resources.

The prose is slightly confusing, but the code examples help.

Sections 1 & 2 should be enough for those who only want to understand the problem with aliasing, and get a glimpse of what linear types are.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Personally I do not see a problem with aliasing.

Personally I do not see a problem with aliasing. Maybe I am too optimistic, but I think if a block of code is viewed as a black box with annotations on its input and output, then the problem of checking aliases becomes a problem of reviewing annotations at the start and end of block.

When I say 'annotation', I mean information about: a) the validity of the state of the input/output variables, b) the relationship of the input and output variables.

Let's see an example. The following signature of a method in Java-like code is annotated on its input and output:

Foo something(Foo foo -> {out, null});

In the above, the input variable foo is annotated as: a) possibly being returned and b) possibly null. Therefore, the following piece of code must be rejected by the compiler:

Foo foo = new Foo();
foo = something(foo);
foo.bar();

whereas the following should be accepted:

Foo foo = new Foo();
foo = something(foo);
if (foo != null) foo.bar();

A compiler could easily extract the proper annotations and store them in class/symbol files.

Let's not forget that C++'s const keyword is a similar annotation.

Aliasing considered harmful

I hate to be trite, but really, aliasing is the bane of imperative programming. There are a tremendous number of optimizations that simply aren't possible because of aliasing, and a good deal of static checks too. Perhaps you missed the significance of the given example: determining when a resource is being used properly. If two different pieces of code hold a reference to a file, and one of them closes it, the other doesn't know that the file is no longer valid to access without performing a check every time first. On the other hand, if it were statically impossible to access a file after it was closed, then a whole range of runtime checks and problems could simply be eliminated. I think that's *huge*.

Unfortunately, I think linear types look too bulky to become popular in practice, but this paper is a stepping stone towards a production-ready mechanism of encoding stateful information in types. In C++, the idiomatic way to handle this resource usage is to use something like a shared pointer with custom deleter, where the last pointer to the resource cleans up the resource (closes the file). The problem with this technique is that it requires all the space and time overhead of the shared pointer (which, fortunately, is not particularly exorbitant, but which would still be nice to eliminate).

The other thing you might be missing is the implication for storage management. Aliasing is the sole reason that memory management is hard. If there were never more than one reference to a given storage area, you would only need to track the lifetime of that one reference to determine when the storage can be reclaimed. It is the fact that multiple aliases with different lifetimes can access the storage that we must resort to techniques like reference counting and garbage collection. Reference counting is an explicit demonstration that aliasing is a computationally pervasive cost. And if you don't think that reference counting is popular, just look at COM.

Now, what if linear types gave us a way to *statically determine when storage can be reclaimed*?? Wow! Then you have another mechanism like region inferencing for performing compile-time memory management, thereby avoiding the cost in rc *or* gc! I hope that the magnitude of this possibility is not lost on you. GC today is "good" to "pretty good", but A) it still has a cost, no matter how you do it, and B) almost all GC is *conservative*. That is, there will be some storage regions that are semantically dead but held alive by a reference. If we could statically determine that more regions are semantically dead because those references are no longer used, then we would have even better storage reclamation.

To get back to the title of my post, the reason aliasing is so popular in many languages, despite the difficulties it can bring, is because it's also extremely useful. So aliasing itself isn't going to go away any time soon. The FP solution to aliasing is to make it a non-issue by preserving referential transparency. However, that has an associated cost as well.

Optimisations may interfere

Now, what if linear types gave us a way to *statically determine when storage can be reclaimed*??

The Clean compiler has such an optimisation (using uniqueness types which are related to linear types).

Now, as is often the case, this optimisation may interfere with other optimisations.
For example the technique described in
Haskell on a Shared-Memory Multiprocessor (Tim Harris, Simon Marlow, Simon Peyton Jones) is not immediately applicable because memory space for immutable objects may now be overwritten by other objects.

It was my understanding that

It was my understanding that uniqueness types and linear types was the same thing. Could you please expand on the diffrence, or give some pointers?

Uniqueness vs. linear typing

See the intro of Erik Barendsen and Sjaak Smetsers
Uniqueness typing for functional languages with graph rewriting semantics,

Perhaps you did not understand my post.

If you follow my post above more closely, you will see that there is a solution which allows aliases to exist, but also preserves the program's correctness, including state of storage.

Non-nullable pointers and linear types are special cases of the solution of the problem of state correctness, to which I think a solution exists.

Perhaps you did not understand mine

Your "solution" is to enforce the runtime checks that already exist and must be written manually to deal with aliasing issues. My "solution" is to eliminate the need for checks at all. The difference is that annotations can only enforce local invariants and preserve local information. What annotation are you going to specify that says: "This file can only be opened if it is closed, and closed if it is open"? Consider the case of a database engine where several different query objects need access to a file and have different lifetimes.

On the other hand, types which allow you to perform inference over a whole program can, in some instances, allow you to eliminate entirely the runtime checks which appear in your annotated code. That is less code to write/generate, less code to execute, and less code to maintain. Where I come from, that is an unequivocal Good Thing(TM).

Working on it...

What annotation are you going to specify that says: "This file can only be opened if it is closed, and closed if it is open"?

Currently working on it and I have good reasons to believe that it's possible, with a good programming language.

A key to this would be, for instance, to have a different type for an opened file and a closed file.


file_open: closed_file -> open_file
file_open_rw: closed_file -> open_file_rw
open_rw_as_open: open_file_rw -> open_file
file_close: open_file -> closed_file

Etc.

On this topic, see also Microsoft Research's Vault or Naoki Kobayashi's TyPiCal & Resource Usage Analysis.

Phantom types

Is not hard to this with with phantom types, I posted one (ugly) way to do it on fa.caml last February. The posted the 'close' function does type if you eta-expand it). Its not really satisfactory though, because you have to jump through hoops to localize your effects.

Phantom types ?

Do you have some documentation about this ?

Phantom Types on the Haskell wiki

From Phantom Types:

We create a Parameterized type in which the parameter does not appear on the right hand side.

Thanks

Thanks. Lucky for me I'm working on something more generic, otherwise I'd have been busted.

Aha, somebody beat me to it.

But I am happy I am not alone in this pursuit.

Maybe I did not explain my solution enough.

You said that:

"Your "solution" is to enforce the runtime checks that already exist and must be written manually to deal with aliasing issues

Not at all!

first of all, all the checks I am proposing are not done at run-time, but at compile-time.

Secondly, I do not propose to write them manually, but to have the compiler infer them from the code. The programmer would only have to write the logical requirements.

My "solution" is to eliminate the need for checks at all.

But your solution works in a very limited scope. My solution is general, and accounts for all logical problems. In fact, my solution is the "missing link" of programming: the declaration of requirements along with the implementation.

What annotation are you going to specify that says: "This file can only be opened if it is closed, and closed if it is open"?

Hey, it's very easy. Example in C-like syntax:

FILE CreateFile() -> {closed} {
    //bla bla create file object
    return file;
}
FILE OpenFile(FILE file -> {closed}) -> {open} {
    //bla bla open file
    return file;
}
FILE CloseFile(FILE file -> {open}) -> {closed} {
    //bla bla close file
    return file;
}
void ReadFile(FILE file -> {open}, byte[] buffer) {
    //bla bla read file
}

It's very easy to see from the above that:

  • when a file is created, its state is closed.
  • when a file is opened, its state is open.
  • before a file is opened, it must be closed.
  • before a file is closed, it must be open.
  • before a file is read, it must be open.

The above can be checked mechanically by a compiler. If only APIs came together with their requirements, programs would be of much higher quality.

That is less code to write/generate, less code to execute, and less code to maintain. Where I come from, that is an unequivocal Good Thing(TM)

I couldn't agree more. That's one of the reasons I post here.

Design by Contract?

This sounds (to me, anyway) a lot like Design by Contract implemented as static analysis, which is what SPARK-Ada does. Having said that, I've never actually done any SPARK programming, so perhaps I'm off base here.

Not quite as simple as that

I thought through this possibility myself before spotting the problem. Without linearity, consider this code:

void write(FILE f)
{
    WriteFile(f, "Hello, world.");
}

void write_n_close(FILE f)
{
    WriteFile(f, "Goodbye, world!");
    CloseFile(f);
}

FILE file = OpenFile("foo.txt");
if (getchar() == 'x') write(file);
else write_n_close(file);
write_n_close(file);

Now, consider that you can't statically determine whether the second invocation of write_n_close() will fail or not. The conservative thing to do would be to forbid it, but that would also make most code unwritable. This is why I said that you must introduce runtime checks. There's a few problems. One is copying, naturally. The other is dataflow analysis. Trying to find all possible paths through the code statically to make sure the invariants are preserved is going to be exponentially hard (or worse) in many cases.

That's why the linear types were introduced. By controlling copying, you can limit leakage of control. That's really the only way to do this kind of thing and avoid the runtime checks.

As I understand it the whole

As I understand it the whole point is that write and write_n_close has diffrent types, and if you want to enforce static checks on them you generally can't permit diffrent types in diffrent branches of a conditional.

Bad example

I didn't spend much time trying to make a robust example, so here's a much better attempt:

FILE file1 = OpenFile("foo.txt");
FILE file2 = file1;  // problem
CloseFile(file1);
ReadFile(file2, buffer);  // Boom!

Process variables, not names.

In order to solve the aliasing problem, all you have to do is to process variables and not names. Names can be attached to variables during the analysis in order to find out about which variable we are interested in any given point.

To put it differently, variable identifiers are only meaningful as names. If a variable has more than one name, then it is clear that it is the variable that we should be interested in and not the names that are attached to it.

The example you posted can be re-written in the following way which clearly demonstrates the solution:

FILE file1 = OpenFile("foo.txt"); //var1[file1]:{Open}
FILE file2 = file1;               //var1[file1, file2]:{Open}
CloseFile(file1);                 //var1[file1, file2]:{Close}
ReadFile(file2, buffer);          //var1[file1, file2]:{Close}; error.

The above means that openFile creates 'var1', and within the square brackets we can find the possible names of 'var1'. You can see that the problem of aliasing goes away when we process the actual variables and not assume that one name == one variable.

More conventionally (at

More conventionally (at least around here), one would talk about variables being bound to references to mutable storage cells that contain values. Which means all variables are bound to immutable values.

Now, consider that you can't

Now, consider that you can't statically determine whether the second invocation of write_n_close() will fail or not. The conservative thing to do would be to forbid it, but that would also make most code unwritable.

Not really. The correct thing would be to forbid it, because a possible path might lead to closing a closed file.

Trying to find all possible paths through the code statically to make sure the invariants are preserved is going to be exponentially hard (or worse) in many cases.

Actually you do not have to check all the possible paths. You only have to check the edges of blocks using sets of values. For example:

void mighty_function_which_may_close_the_file(FILE f)
{
    ...8,000 lines of very complex code, which in some place
    CloseFile is invoked.
}

FILE file = OpenFile("foo.txt");
if (getchar() == 'x') write(file); else mighty_function_which_may_close_the_file(file);
CloseFile(file);

In the above example, we do not care about following all the paths in the function "mighty_function_which_may_close_the_file"...all we care about is that it is possible for the file to close. Once we compile this function, we keep the information that the passed file may be closed after the function returns.

To explain more rigorously:

the input set of the function 'mighty_function_which_may_close_the_file' is:

{Open}.

The output set is:

{Open, Close}.

The input set of the function 'closeFile' is:

{Open}.

The sequence

mighty_function_which_may_close_the_file(file) => closeFile(file)

creates the following set relationships (output of a subroutine becomes an input of another subroutine):

{Open} => {Open, Close} => {Open}

Since {Open, Close} is a superset of {Open}, we can safely declare an error: the input set of CloseFile(file) may be {Open, Close}, but only {Open} is allowed.

The set information can be kept along the function and checked where the function is used.

And what we actually get is

And what we actually get is a phantom type. Or perhaps not, because we probably want to be able to branch on the actual state if we don't know it statically (oh look, GADT!). The sets are perhaps best handled as (disjoint) unions with subtyping.

Referential Transparency

What do you mean when you write "FP makes aliasing a non-issue"? That the storage-management benefits are irrelevant?
I'm actually interested in linear types because of FP, since they seem to be the only efficient & truly-FP solution for things like aggregate update.

On another note, aren't "referential transparency" and "pure"-FP somewhat idealized, since function calls can easily change the layout of memory used by the app? That is, the return value may contain newly-allocated memory.. (and then there is the stack, the PC, &cetera). I'm sure someone has pointed this out; I just haven't seen it.

So in an unusual sense, the reuse of storage via linear types could actually make functions more pure, if said functions just transform memory (vs. alloc/free it).

On another note, aren't

On another note, aren't "referential transparency" and "pure"-FP somewhat idealized, since function calls can easily change the layout of memory used by the app? That is, the return value may contain newly-allocated memory.. (and then there is the stack, the PC, &cetera). I'm sure someone has pointed this out; I just haven't seen it.

They're not idealized because the elements you mention are not part of the abstract machine used to specify the semantics.

Annotations

I believe this article (Broadway: A Compiler for Exploiting the Domain-Specific Semantics of Software Libraries) uses annotations for compiler optimization and this one (Error Checking with Client-Driven Pointer Analysis) uses it for pointer analysis. Both are generally within the domain of libraries in C.

Not that different

Personally I do not see a problem with aliasing. Maybe I am too optimistic, but I think if a block of code is viewed as a black box with annotations on its input and output, then the problem of checking aliases becomes a problem of reviewing annotations at the start and end of block.

In a sense, linear types are annotations that tell the compiler "you can't alias this value". They just happen to have extensive research done about them.

Yeap. But why such a restriction,

... where a more general solution exists?

Why sed?

Why have regular expressions when a more general solution exists?

You are too optimistic :(

If you have mutable data, then that data forms a new channel of communication between different parts of the program. You can use this power for good, when you use aliasing to design algorithms that communicate through shared memory to save time and space, but more commonly it just leads to bugs.

The reason that the obvious kind of annotations don't work is because you need to specify no-aliasing conditions in your preconditions and postconditions. Suppose your function has six different variables all of type Foo (call them x,y,z,u,v,w). Now, if two of those variables point to the same Foo object, then an update on one must update the other one too. If they hold different Foo objects, then an update to one should not change the other one.

Why is this hard? If you've got distinct objects (and you usually do), then the number of no-aliasing clauses in your specification will rise quadratically with the number of variables in the routine. For example, to specify that the variables in the previous example don't alias, you'd need to write:

x != y & x != z & x != u & x != v & x != w &
y != z & y != u & y != v & y != w &
z != u & z != v & z != w &
u != v & u != w &
v != w

Things get even worse with arrays, because you have to give a no-aliasing condition for each element in an array. This is basically why Hoare logic never lived up to the high hopes people had for it back in the 70s; you couldn't scale it up to real programs because every spec had a ton of unenlightening no-aliasing conditions for ever ounce of real meaning.

Other papers linear types for explicit memory mgmt

This paper seems to be about a technical result regarding the expressiveness of F_omega with linear types. Somewhat interesting, but not a great place to start learning about linear types for explicit memory management.

Some other good papers on this include Morrisett and Ahmed's on L^3, A Linear Language with Locations and Zhu and Xi's on Safe Programming with Pointers through Stateful Views. Also, if anyone wants to play around with it, this feature is implemented in research the language ATS where the linear capabilities are called 'views'.