quchen / stgi

A user-centric visual STG implementation to help understand GHC/Haskell's execution model.
Other
527 stars 26 forks source link

STGi - STG interpreter

STGi is a visual STG implementation to help understand Haskell's execution model.

It does this by guiding through the running of a program, showing stack and heap, and giving explanations of the applied transition rules. Here is what an intermediate state looks like:

Release Hackage BSD3

Table of contents

Quickstart guide

If you want to have a quick look at the STG, here is what you need to get going. The program should build with both stack and cabal.

The app/Main.hs file is written so you can easily switch out the prog value for other Programs that contain a main definition. The Stg.ExamplePrograms module provides a number of examples that might be worth having a look, and are a good starting point for modifications or adding your own programs. It's probably easier to read in Haddock format, so go ahead and run

stack haddock --open stgi

and have a look at the example programs.

When you're happy with your app/Main.hs, run

stack build --exec "stgi-exe --colour=true" | less -R

to get coloured output in less. Type /==== to search for ====, which finds the top of every new step; use n (next step) or N (previous step) to navigate through the execution.

About the machine

The spineless tagless graph reduction machine, STG for short, is an automaton used to map non-strict functional languages onto stock hardware. It was developed for, and is heavily used in, the Haskell compiler GHC.

This project implements an interpreter for the STG as it is described in the 1992 paper on the subject, with the main focus on being nice to a human user. Things that might be important for an actual compiler backend, such as performance or static analysis, are not considered in general, only if it helps the understanding of the STG.

The idea behind the machine is to represent the program in its abstract syntax tree form. However, due to references to other parts of the syntax tree, a program is a graph, not a tree. By evaluating this graph using a small set of rules, it can be systematically reduced to a final value, which will be the result of the program.

The STG is

Useful applications

STGi was started to teach myself about the STG. Not long into the project, I decided to extend it to save others the many detours I had to take to implement it. In that sense, it can be a useful tool if you're interested in the lower-level properties of a Haskell implementation. I did my best to keep the code readable, and added some decent Haddock/comment coverage. Speaking of Haddock: it's an excellent tool to start looking around the project before digging into the source!

The other benefit is for teaching others: instead (or in addition to!) of explaining certain common Haskell issues on a whiteboard with boxes and arrows, you can share an interactive view of common programs with others. The example programs feature some interesting cases.

  1. Does this leak memory? On the stack or the heap?
  2. I heard GHC doesn't have a call stack?!
  3. Why is this value not garbage collected?
  4. Why are lists sometimes not very performant?
  5. How many steps does this small, innocent function take to produce a result?

Language introduction

The STG language can be seen as a mostly simplified version of Haskell with a couple of lower level additions. The largest difference is probably that STG is an untyped language.

The syntax will be discussed below. For now, as an appetizer, the familiar Haskell code

foldl' _ acc [] = acc
foldl' f acc (y:ys) = case f acc y of
    !acc' -> foldl' f acc' ys

sum = foldl' add 0

could be translated to

foldl' = \f acc xs -> case xs of
    Nil -> acc;
    Cons y ys -> case f acc y of
        acc' -> foldl' f acc' ys;
    badList -> Error_foldl' badList;

sum = \ -> foldl' add zero;

zero = \ -> Int# 0#

Top-level

An STG program consists of a set of bindings, each of the form

name = \(<free vars>) <bound vars> -> <expression body>

The right-hand side is called a lambda form, and is closely related to the usual lambda from Haskell.

The main value, termination

In the default configuration, program execution starts by moving the definitions given in the source code onto the heap, and then evaluating the main value. It will continue to run until there is no rule applicable to the current state. Due to the lazy IO implementation, you can load indefinitely running programs in your pager application and step as long forward as you want.

Expressions

Expressions can, in general, be one of a couple of alternatives.

For example, Haskell's maybe function could be implemented in STG like this:

maybe = \nothing just x -> case x of
    Just j   -> just j;
    Nothing  -> nothing;
    badMaybe -> Error_badMaybe badMaybe

Some lambda expressions can only contain certain sub-elements; these special cases are detailed in the sections below. To foreshadow these issues:

Updates

A lambda form can optionally use a double arrow =>, instead of a normal arrow ->. This tells the machine to update the lambda form's value in memory once it has been calculated, so the computation does not have to be repeated should the value be required again. This is the mechanism that is key to the lazy evaluation model the STG implements. For example, evaluating main in

add2 = … -- <add two boxed ints>
one = \ -> Int# 1#;
two = \ -> Int# 2#;
main = \ => add2 one two

would, once the computation returns, overwrite main (modulo technical details) with

main = \ -> Int# 3#

A couple of things to keep in mind:

Pitfalls

Code example

The 1992 paper gives two implementations of the map function in section 4.1. The first one is the STG version of

map f [] = []
map f (y:ys) = f y : map f ys

which, in this STG implementation, would be written

map = \f xs -> case xs of
    Nil -> Nil;
    Cons y ys -> let fy = \(f y) => f y;
                     mfy = \(f ys) => map f ys
                 in Cons fy mfy;
    badList -> Error_map badList

For comparison, the paper's version is

map = {} \n {f,xs} -> case xs of
    Nil {} -> Nil {}
    Cons {y,ys} -> let fy = {f,y} \u {} -> f {y}
                       mfy = {f,ys} \u {} -> map {f,ys}
                   in Cons {fy,mfy}
    badList -> Error_map {badList}

You can find lots of further examples of standard Haskell functions implemented by hand in STG in the Prelude modules. Combined with the above explanations, this is all you should need to get started.

Marshalling values

The Stg.Marshal module provides functions to inject Haskell values into the STG (toStg), and extract them from a machine state again (fromStg). These functions are tremendously useful in practice, make use of them! After chasing a list value on the heap manually you'll know the value of fromStg, and in order to get data structures into the STG you have to write a lot of code, and be careful doing it at that. Keep in mind that fromStg requires the value to be in normal form, or extraction will fail.

Runtime behaviour

The following steps are an overview of the evaluation rules. Running the STG in verbose mode (-v2) will provide a more detailed description of what happened each particular step.

Code segment

The code segment is the current instruction the machine evaluates.

Stack

The stack has three different kinds of frames.

Heap

The heap is a mapping from memory addresses to heap objects, which can be closures or black holes (see below). Heap entries are allocated by let(rec), and deallocated by garbage collection.

As a visual guide to the user, closures are annotated with Fun (takes arguments), Con (data constructors), and Thunk (suspended computations).

Black holes

The heap does not only contain closures, but also black holes. Black holes are annotated with the step in which they were created; this annotation is purely for display purposes, and not used by the machine.

At runtime, when an updatable closure is entered (evaluated), it is overwritten by a black hole. Black holes do not only provide better overview over what thunk is currently evaluated, but have two useful technical benefits:

  1. Memory mentioned only in the closure is now ready to be collected, avoiding certain space leaks. The 1992 paper gives the following example in section 9.3.3:

    list = \(x) => <long list>
    l = \(list) => last list

    When entering l without black holes, the entire list is kept in memory until last is done. On the other hand, overwriting l with a black hole upon entering deletes the last pointer from it, and last can run, and be garbage collected, incrementally.

  2. Entering a black hole means a thunk depends on itself, allowing the interpreter to catch some non-terminating computations with a useful error

Garbage collection

Currently, two garbage collection algorithms are implemented:

Unhelpful error message?

The goal of this project is being useful to human readers. If you find an error message that is unhelpful or even misleading, please open an issue with a minimal example on how to reproduce it!

Differences from the 1992 paper

Grammar

Evaluation

GHC's current STG

The implementation here uses the push/enter evaluation model of the STG, which is fairly elegant, and was initially thought to also be top in terms of performance. As it turned out, the latter is not the case, and another evaluation model called eval/apply, which treats (only) function application a bit different, is faster in practice.

This notable revision is documented in the 2004 paper How to make a fast curry. I don't have plans to support this evaluation model right now, but it's on my list of long-term goals (alongside the current push/enter).