ezyang’s blog

the arc of software bends towards understanding

Cost semantics for STG in modern GHC

One of the problems with academic publishing is that it’s hard to keep old papers up-to-date. This is the certainly case for this 1995 Sansom paper on profiling non-strict, higher-order functional languages. While the basic ideas of the paper still hold, the actual implementation of cost centers in GHC has changed quite a bit, perhaps the most dramatic change being the introduction of cost center stacks. So while the old paper is good for giving you the basic idea of how profiling in GHC works, if you really want to know the details, the paper offers little guidance.

So what do you do when your cost semantics are out-of-date? Why, update them of course! I present an updated cost-semantics for STG in modern GHC (PDF) (GitHub). Eventually these will go in the GHC repository proper, alongside core-spec which is a similar document for Core. However, I haven't done any proofs with these semantics yet, so they are probably a little buggy.

Despite the lack of proofs, the formalization has been helpful already: I’ve already spotted one bug in the current implementation (remarked upon in the document). I’ve also identified a potential refactoring based on the way the rules are currently setup. Please let me know about any other bugs you find!

7 Responses to “Cost semantics for STG in modern GHC”

  1. Luca Bruno says:
    September 8, 2013 at 7:29 pm

    I was lately reading about STG and turned out that some of the papers are out of date. This is certainly not that problematic, ghc code is clean and papers very helpful, still updating them is a nice thing do.
    I’m trying to get involved in ghc/ghcjs and that helps me a lot, thanks.

  2. Luca Bruno says:
    September 8, 2013 at 7:33 pm

    Also, what’s the syntax at page 4? It’s something logic but it’s very complex to read.

  3. Edward Z. Yang says:
    September 8, 2013 at 10:05 pm

    Luca: Great! Hope they are of use.

    Re the syntax on page 4, those are the cost semantics. They are big(-ish) step operational semantics with some extra bits (namely the costs of operations). So if you’ve never looked at a big-step operational semantics before, it might be a little difficult to understand, since this particular one is a little hairy. If you have any specific questions I can probably answer them, but a full answer would probably take another blog post…

  4. Luca Bruno says:
    September 9, 2013 at 3:42 am

    Ok thanks, couldn’t find a name for that syntax :-) It would be helpful to tell that in the paper. Now reading what it operational semantics is, do you have any suggested paper about big-step operational semantics at hand?

  5. Edward Z. Yang says:
    September 9, 2013 at 4:32 am

    I’m not really sure how I picked it up (I guess by osmosis). Essentially, it says “this expression in this environments evaluates to this other expression in some new environment” + some side conditions (i.e. there is something particular in the heap, or some other evaluation goes. If you stare at it a while it should make some sense.

  6. Luca Bruno says:
    September 9, 2013 at 4:49 am

    The problem is with the symbols, have to find some paper describing them :-)

  7. Edward Z. Yang says:
    September 9, 2013 at 5:06 am

    Well, they vary from presentation to presentation, so you’re unlikely to find one which exactly matches the presentation here :)

    But point taken, I will add some more explanatory text for the notational conventions here.

Leave a Comment