Lindsey Kuper

Over the last year or two, I’ve been using PLT Redex more and more often as a tool for my research. Redex is a domain-specific programming language and suite of tools for expressing and experimenting with semantic models of programming languages.

Taking your semantics for a shakedown cruise

What do I mean by “expressing and experimenting with semantic models of programming languages”? One way to think of Redex is as a programming language for writing programming languages. When you write up a model of a language L in Redex, you end up with something that is in fact an implementation of L, although one that probably runs too slowly to be practical. So it might be more accurate to think of Redex as a language for writing reference implementations of programming languages, together with a suite of tools for doing lots of things that you might want to do with such a reference implementation, like randomized testing, typesetting, and visualization.1

But, ugh! That phrase “reference implementation” raises the specter of mind-numbing technical standards documents and the like. It doesn’t convey the fun of Redex at all. Instead, I like to think of Redex as a quick way of giving potential new language features a try.

For instance, I want LVars to be a mechanism for deterministic parallelism: programs that use LVars to communicate between parallel tasks should always evaluate to the same value, regardless of the order in which LVar operations occur. To that end, it’s useful to model a tiny language in which LVars are the only interesting feature. If I know that no other feature of my tiny language introduces nondeterminism, then if any nondeterminism does arise in programs I’ve written using the model, I’ll know that something is wrong with my design for LVars.

Redex isn’t a theorem-proving tool, so I can’t use it to prove that a language is deterministic.2 I can, however, use Redex to attempt to falsify properties of a language. For instance, Redex can evaluate a program in every possible order and compare the results with an expected result. If I ever get something different, then I’ll know that my language is not deterministic. In this sense, Redex is a way to take a language semantics for a shakedown cruise before you try to prove anything about it, because getting halfway through a long proof only to find that the property you’re attempting to prove is false is about as much fun as finding out that your boat’s not seaworthy when you’re halfway across the ocean.

Parameterizing a language definition by a lattice

Some whiteboard sketches from December 2011. These lattices are one of the ideas that survived!
Some whiteboard sketches from December 2011. These lattices are one of the ideas that survived!

My tiny LVar language, lambdaLVar, is more or less a garden-variety untyped lambda calculus, extended with a memory store and with put and get operations that respectively write to and read from store locations. lambdaLVar expressions can reduce in parallel, and having a store of shared mutable memory would ordinarily let nondeterminism in. Instead of ordinary mutable memory cells, though, the store contains LVars, which is short for “lattice variables”. An LVar’s value can only increase over time, where the meaning of “increase” is given by a partially ordered set, or lattice, that the user of the language specifies. Therefore lambdaLVar is really a family of languages: instantiate it with one lattice and you get one deterministic parallel language; with a different lattice, and you get another.

On paper, the definition of lambdaLVar is parameterized by that user-specified lattice. For a long time, I wanted the Redex definition of lambdaLVar to be parameterized in the same way, but I couldn’t figure out how to accomplish it in Redex. Finally, after checking with the Racket users mailing list, I learned that what I want to do isn’t possible in Redex as it stands today, although it should be possible in a future version.

But wait! Redex is embedded in Racket, a language with a powerful macro system that allows you to write programs that generate programs.3 So, even though I couldn’t parameterize the definition of lambdaLVar by a lattice using Redex alone, I could write a Racket macro taking a lattice as an argument, then use it to generate instantiations of lambdaLVar at macro expansion time.

I defined a Racket macro, define-lambdaLVar-language, that takes a language name, a least upper bound operation, and a set of lattice values, and generates a Redex language definition. For instance, to generate a Redex language model called lambdaLVar-nat where the user-specified lattice is the natural numbers with max as the least upper bound, I can call define-lambdaLVar-language like this:

(define-lambdaLVar-language lambdaLVar-nat max natural)

Here, max is an operation that’s built in to Racket. natural doesn’t mean anything in Racket, but to Redex it means “the set of natural numbers”. The above program is a Racket program, not a Redex program, but because define-lambdaLVar-language is a macro, it’s perfectly okay to pass in arguments like natural; they won’t be interpreted until after the macro has expanded.

I’m no macrologist, but writing the define-lambdaLVar-language macro itself was easy.4 I already had a Redex model of lambdaLVar, but specialized to use natural as the set of lattice elements, and calling out to a user-specified least upper bound operation called lub-op. So the macro just ended up being a very thin wrapper around the code I already had, with some trivial changes.

(define-syntax-rule (define-lambdaLVar-language name lub-op lattice-values ...)
  (begin
    ;; Entire original Redex model goes here, with `natural` replaced with
    ;; `lattice-values ...`, and instances of `...` replaced with `(... ...)`
))

You can see what it ended up looking like on GitHub. lambdaLVar.rkt defines the define-lambdaLVar-language macro. The nat directory has a test suite of programs for lambdaLVar-nat; natpair and natpair-ivars are two more example instantiations. As you might expect, for some lattices, the least upper bound operation is dead simple; for others, it’s a little more sophisticated. Try writing one yourself, and instantiate your own deterministic parallel language today!

Thanks to the folks on the Racket users list for their help, and to Matt Might, who originally suggested that I would need to write Redex-generating macros in a conversation at ICFP last September. I wanted so badly for there to be some way to do everything within Redex that I ignored his advice for another six months!

  1. For a snappy introduction to Redex, I recommend Robby Findler’s POPL 2012 talk, “Run Your Research”. ↩

  2. I ended up doing that by hand, more’s the pity. ↩

  3. In fact, Redex itself is implemented using Racket macros, although you don’t need to know how that works to use Redex. ↩

  4. Vincent St-Amour recommended Greg Hendershott’s “Fear of Macros” as a guide for beginners. ↩

Comments