So there’s a blog post that advises every method should, when possible, return self. I’d like to suggest you do the opposite: wherever possible, return something other than self.

Mutation is hard

Mutation makes code harder to reason about. Mutable objects make equality comparisons tricky: if you use a mutable object as the key in a hashmap, for instance, then change one of its fields, what happens? Can you access the value by the new string value? By the old one? What about a set? An array? For a fun time, try these in various languages. Try it with mutable primitives, like Strings, if the language makes a distinction. Enjoy the results.

If you call a function with a mutable object as an argument, you have very few guarantees about the new object’s value. It’s up to you to enforce invariants like “certain fields must be read together”.

If you have two threads interacting with mutable objects concurrently, things get weird fast.

Now, nobody’s arguing that mutability is always bad. There are really good reasons to mutate: your program ultimately must change state; must perform IO, to be meaningful. Mutation is usually faster, reduces GC pressure, and can be safe! It just comes with costs! The more of your program deals with pure values, the easier it is to reason about. If you compare two objects now, you know they’ll compare the same later. You can pass arguments to functions without ever having to worry that they’ll be changed out from underneath you. It gets easier to reason about thread safety.

Moreover, you don’t need a fancy type system like Haskell to experience these benefits: even in the unityped default-mutable wonderland of Ruby, having a culture that makes mutation explicit (for instance, gsub vs gsub!), a culture where not clobbering state is the default, can make our jobs a little easier. Remember, we don’t have to categorically prevent bugs; just make them less likely. Every bit helps.

Returning nil, void, or self strongly suggests impurity

Any time you see a method like

public void foo(String X) { ... } function(a, b) { ... return undefined; } def foo(args) ... self end

you should read: “This function probably mutates state!” In an object oriented language, it might mutate the receiver (self or this). It might mutate any of its arguments. It might mutate variables in lexical scope. It might mutate the computing environment, by setting a global variable, or writing to the filesystem, or sending a network packet.

The hand-wavy argument for this is that there is exactly one meaningful pure function for each of these three return types: the constant void function, the constant nil function, and the identity function(s). If you see this signature used over and over, it’s a hint you’re staring at a big ball of mutable state.

Proof

We aim to show there is only one pure function returning void, one pure function returning nil, etc. In general, we wish to show for any value r you might care to return, there exists exactly one pure function which always returns r.

I’m going to try to write this for folks without a proofs background, but I will use some notation:

• Capital letters, e.g. X, denote sets
• f(x) is function application
• a iff b means “a if, and only if, b”
• | means “such that”
• ∀ x means “for all x”
• ∃ x means “there exists an x”
• x ∈ X means “x is an element of the set X”
• (x, y) is an ordered pair, like a tuple
• X x Y is the Cartesian product: all ordered pairs of (x, y) taken from X and Y respectively.

Definitions

I’m going to depart slightly from the usual set-theoretic definitions to simplify the proof and reduce confusion with common CS terms. We’re interested in functions which might:

• Take a receiver (e.g. this, self)
• Take arguments
• Return values
• Throw exceptions
• Depend on an environment
• Mutate their environment

Let’s simplify.

• A receiver is simply the first argument to a function.
• Zero or multiple arguments can be represented as an ordered tuple: (), (arg1), (arg1, arg2, arg3, …).
• Returning multiple return values (as in go) can be modeled by returning tuples.
• Exceptions can be modeled as a special set of return values, e.g. (“exception”, “something bad!”)
• In addition to mapping an argument to a return value, the function will map an initial environment e to a (possibly identical) final environment e'. The environment encapsulates IO, global variables, dynamic scope, mutable state, etc.

Now we adapt the usual set-theoretic graph definition of a function to our model:

Definition 1. A function f in an environment set E, from an input set X (the “domain”), to a set of return values Y (the “codomain”), written f: E, X -> Y, is the set of ordered tuples (e, e', x, y) where e and e' ∈ E, x ∈ X, and y ∈ Y, with two constraints:

1. Completeness. ∀ x ∈ X, e ∈ E: ∃ (e, e', x, y) ∈ f.
2. Determinism. ∀ (e, e', x, y) ∈ f: e' = e' and y = y if e = e and x = x

Completeness simply means that the function must return a value for all environments and x’s. Determinism just means that the environment and input x uniquely determine the new environment and return value. Nondeterministic functions are modeled by state in the environment.

We write function application in this model as f(e, x) = (e', y). Read: “Calling f on x in environment e returns y and changes the environment to e'.”

Definition 2. A function is pure iff ∀ (e, e', x, y) ∈ f, e = e'; e.g, its initial and final environments are identical.

There can be only one

We wish to show that for any value r, there is only one pure function which always returns r. Assume there exist two distinct pure functions f and g, over the same domain X, returning r. Remember, these functions are pure, so their initial and final environments are the same:

• ∀ e ∈ E, x ∈ X: f(e, x) -> (e, r)
• ∀ e ∈ E, x ∈ X: g(e, x) -> (e, r)

But by definition 1, f and g are simply:

• f = {(e, e, x, r) | e ∈ E, x ∈ X}
• g = {(e, e, x, r) | e ∈ E, x ∈ X}

… which are identical sets. We obtain a contradiction: f and g cannot be distinct; therefore, in any environment E and over any input set X, there exists only a single function returning r. ∎

You can make the exact same argument for functions that return their first (or nth) argument: they’re just variations on the identity function, one version for each arity:

• (e, e, (x), x)
• (e, e, (x, a), x)
• (e, e, (x, a, b), x)
• (e, e, (x, a, b, …), x)

Redundancy of functions over different domains

Given two pure single-valued functions over different domains f: E, X1 -> {r} and g: E, X2 -> {r}, let h be the set of all tuples in either f or g: h = f ∪ g.

Since f is pure, ∀ (e, e', x, y) ∈ f, e = e'; and the same for g. Therefore, ∀ (e, e', x, y) ∈ h, e = e' as well: h does not mutate its environment.

Since f has a mapping for all combinations of environments in E and inputs in X1, so does h. And the same goes for g: h has mappings for all combinations of environments in E and inputs in X2. h is therefore complete over E and X1 ∪ X2.

Since f and g always return r, ∀ (e, e', x, y) ∈ h, y = r too. Because h can never have multiple values for y (and because it does not mutate its environment), it is deterministic per definition 1.

Therefore, h is a pure function in E over X1 ∪ X2–and is therefore a pure function over either X1 or X2 alone. You can safely replace any instance of f or g with h: there isn’t really a point to having more than one pure function returning void, nil, etc. in your program, unless you’re doing it for static type safety.

Don’t believe me? Here’s a single Clojure function that can replace any pure function returning its first argument. Works on integers, strings, other functions… whatever types you like.

user=> (def selfie (fn [self & args] self))) #'user/selfie user=> (selfie 3) 3 user=> (selfie "channing" "tatum") "channing"

Returning self suggests impurity

You can write the same function more than one way. Here are two pure functions in Ruby that both return self:

def meow self end def stretch nil ENV["USER"] + " in spaaace" 5.3 / 3 self end

meow is just identity–but so is stretch, and, by our proof above, so is every other pure function returning self. The only difference is that stretch has useless dead code, which any compiler, linter, or human worth their salt will strip out. Writing code like this is probably silly. You can construct weird cases (interfaces, etc) where you want a whole bunch of identity functions, or (constantly nil), etc, but I think those are pretty rare.

What about calling a function then returning self?

def foo enjoy("http://shirtless-channing-tatum.biz") self end

There are only two cases. If enjoy is pure, so is foo, and we can replace the function by

def foo self end

If enjoy is impure (and let’s face it: shirtless Channing Tatum induces side effects in most callers), then foo is also impure, and we’re back to square one: mutation.

Final thoughts

When you see functions that return void, nil, or self, ask “what is this mutating?” If you have a pure function (say, returning the number of explosions in a film) and follow the advice of returning self as much as possible, you are turning a pure function into an impure one. You have to add state and mutability to the system. You should strive to do the opposite: reduce mutation wherever possible.

I assure you, return values are OK.

Writing software can be an exercise in frustration. Useless error messages, difficult-to-reproduce bugs, missing stacktrace information, obscure functions without documentation, and unmaintained libraries all stand in our way. As software engineers, our most useful skill isn’t so much knowing how to solve a problem as knowing how to explore a problem that we haven’t seen before. Experience is important, but even experienced engineers face unfamiliar bugs every day. When a problem doesn’t bear a resemblance to anything we’ve seen before, we fall back on general cognitive strategies to explore–and ultimately solve–the problem.

There’s an excellent book by the mathematician George Polya: How to Solve It, which tries to catalogue how successful mathematicians approach unfamiliar problems. When I catch myself banging my head against a problem for more than a few minutes, I try to back up and consider his principles. Sometimes, just taking the time to slow down and reflect can get me out of a rut.

1. Understand the problem.
2. Devise a plan.
3. Carry out the plan
4. Look back

Seems easy enough, right? Let’s go a little deeper.

Understanding the problem

Well obviously there’s a problem, right? The program failed to compile, or a test spat out bizarre numbers, or you hit an unexpected exception. But try to dig a little deeper than that. Just having a careful description of the problem can make the solution obvious.

Our audit program detected that users can double-withdraw cash from their accounts.

What does your program do? Chances are your program is large and complex, so try to isolate the problem as much as possible. Find preconditions where the error holds.

The problem occurs after multiple transfers between accounts.

Identify specific lines of code from the stacktrace that are involved, specific data that’s being passed around. Can you find a particular function that’s misbehaving?

The balance transfer function sometimes doesn’t increase or decrease the account values correctly.

What are that function’s inputs and outputs? Are the inputs what you expected? What did you expect the result to be, given those arguments? It’s not enough to know “it doesn’t work”–you need to know exactly what should have happened. Try to find conditions where the function works correctly, so you can map out the boundaries of the problem.

Trying to transfer $100 from A to B works as expected, as does a transfer of $50 from B to A. Running a million random transfers between accounts, sequentially, results in correct balances. The problem only seems to happen in production.

If your function–or functions it calls–uses mutable state, like an agent, atom, or ref, the value of those references matters too. This is why you should avoid mutable state wherever possible: each mutable variable introduces another dimension of possible behaviors for your program. Print out those values when they’re read, and after they’re written, to get a description of what the function is actually doing. I am a huge believer in sprinkling (prn x) throughout one’s code to print how state evolves when the program runs.

Each balance is stored in a separate atom. When two transfers happen at the same time involving the same accounts, the new value of one or both atoms may not reflect the transfer correctly.

Look for invariants: properties that should always be true of a program. Devise a test to look for where those invariants are broken. Consider each individual step of the program: does it preserve all the invariants you need? If it doesn’t, what ensures those invariants are restored correctly?

The total amount of money in the system should be constant–but sometimes changes!

Draw diagrams, and invent a notation to talk about the problem. If you’re accessing fields in a vector, try drawing the vector as a set of boxes, and drawing the fields it accesses, step by step on paper. If you’re manipulating a tree, draw one! Figure out a way to write down the state of the system: in letters, numbers, arrows, graphs, whatever you can dream up.

Transferring $5 from A to B in transaction 1, and $5 from B to A in transaction 2: Transaction | A | B -------------+-----+----- txn1 read | 10 | 10 ; Transaction 1 sees 10, 10 txn1 write A | 5 | 10 ; A and B now out-of-sync txn2 read | 5 | 10 ; Transaction 2 sees 5, 10 txn1 write B | 5 | 15 ; Transaction 1 completes txn2 write A | 10 | 15 ; Transaction 2 writes based on out-of-sync read txn2 write B | 5 | 5 ; Should have been 10, 10!

This doesn’t solve the problem, but helps us explore the problem in depth. Sometimes this makes the solution obvious–other times, we’re just left with a pile of disjoint facts. Even if things look jumbled-up and confusing, don’t despair! Exploring gives the brain the pieces; it’ll link them together over time.

Armed with a detailed description of the problem, we’re much better equipped to solve it.

Devise a plan

Our brains are excellent pattern-matchers, but not that great at tracking abstract logical operations. Try changing your viewpoint: rotating the problem into a representation that’s a little more tractable for your mind. Is there a similar problem you’ve seen in the past? Is this a well-known problem?

Make sure you know how to check the solution. With the problem isolated to a single function, we can write a test case that verifies the account balances are correct. Then we can experiment freely, and have some confidence that we’ve actually found a solution.

Can you solve a related problem? If only concurrent transfers trigger the problem, could we solve the issue by ensuring transactions never take place concurrently–e.g. by wrapping the operation in a lock? Could we solve it by logging all transactions, and replaying the log? Is there a simpler variant of the problem that might be tractable–maybe one that always overcounts, but never undercounts?

Consider your assumptions. We rely on layers of abstraction in writing software–that changing a variable is atomic, that lexical variables don’t change, that adding 1 and 1 always gives 2. Sometimes, parts of the computer fail to guarantee those abstractions hold. The CPU might–very rarely–fail to divide numbers correctly. A library might, for supposedly valid input, spit out a bad result. A numeric algorithm might fail to converge, and spit out wrong numbers. To avoid questioning everything, start in your own code, and work your way down to the assumptions themselves. See if you can devise tests that check the language or library is behaving as you expect.

Can you avoid solving the problem altogether? Is there a library, database, or language feature that does transaction management for us? Is integrating that library worth the reduced complexity in our application?

We’re not mathematicians; we’re engineers. Part theorist, yes, but also part mechanic. Some problems take a more abstract approach, and others are better approached by tapping it with a wrench and checking the service manual. If other people have solved your problem already, using their solution can be much simpler than devising your own.

Can you think of a way to get more diagnostic information? Perhaps we could log more data from the functions that are misbehaving, or find a way to dump and replay transactions from the live program. Some problems disappear when instrumented; these are the hardest to solve, but also the most rewarding.

Combine key phrases in a Google search: the name of the library you’re using, the type of exception thrown, any error codes or log messages. Often you’ll find a StackOverflow result, a mailing list post, or a Github issue that describes your problem. This works well when you know the technical terms for your problem–in our case, that we’re performing a atomic, transactional transfer between two variables. Sometimes, though, you don’t know the established names for your problem, and have to resort to blind queries like “variables out of sync” or “overwritten data”–which are much more difficult.

When you get stuck exploring on your own, try asking for help. Collect your description of the problem, the steps you took, and what you expected the program to do. Include any stacktraces or error messages, log files, and the smallest section of source code required to reproduce the problem. Also include the versions of software used–in Clojure, typically the JVM version (java -version), Clojure version (project.clj), and any other relevant library versions.

If the project has a Github page or public issue tracker, like Jira, you can try filing an issue there. Here’s a particularly well-written issue filed by a user on one of my projects. Note that this user included installation instructions, the command they ran, and the stacktrace it printed. The more specific a description you provide, the easier it is for someone else to understand your problem and help!

Sometimes you need to talk through a problem interactively. For that, I prefer IRC–many projects have a channel on the Freenode IRC network where you can ask basic questions. Remember to be respectful of the channel’s time; there may be hundreds of users present, and they have to sort through everything you write. Paste your problem description into a pastebin like Gist, then mention the link in IRC with a short–say a few sentences–description of the problem. I try asking in a channel devoted to a specific library or program first, then back off to a more general channel, like #clojure. There’s no need to ask “Can I ask a question” first–just jump in.

Since the transactional problem we’ve been exploring seems like a general issue with atoms, I might ask in #clojure

aphyr > Hi! Does anyone know the right way to change multiple atoms at the same time? aphyr > This function and test case (http://gist.github.com/...) seems to double- or under-count when invoked concurrently.

Finally, you can join the project’s email list, and ask your question there. Turnaround times are longer, but you’ll often find a more in-depth response to your question via email. This applies especially if you and the maintainer are in different time zones, or if they’re busy with life. You can also ask specific problems on StackOverflow or other message boards; users there can be incredibly helpful.

Remember, other engineers are taking time away from their work, family, friends, and hobbies to help you. It’s always polite to give them time to answer first–they may have other priorities. A sincere thank-you is always appreciated–as is paying it forward by answering other users' questions on the list or channel!

Dealing with abuse

Sadly, some women, LGBT people, and so on experience harassment on IRC or in other discussion circles. They may be asked inappropriate personal questions, insulted, threatened, assumed to be straight, to be a man, and so on. Sometimes other users will attack questioners for inexperience. Exclusion can be overt (“Read the fucking docs, faggot!”) or more subtle (“Hey dudes, what’s up?”). It only takes one hurtful experience this to sour someone on an entire community.

If this happens to you, place your own well-being first. You are not obligated to fix anyone else’s problems, or to remain in a social context that makes you uncomfortable.

That said, be aware the other people in a channel may not share your culture. English may not be their main language, or they may have said something hurtful without realizing its impact. Explaining how the comment made you feel can jar a well-meaning but unaware person into reconsidering their actions.

Other times, people are just mean–and it only takes one to ruin everybody’s day. When this happens, you can appeal to a moderator. On IRC, moderators are sometimes identified by an @ sign in front of their name; on forums, they may have a special mark on their username or profile. Large projects may have an official policy for reporting abuse on their website or in the channel topic. If there’s no policy, try asking whoever seems in charge for help. Most projects have a primary maintainer or community manager with the power to mute or ban malicious users.

Again, these ways of dealing with abuse are optional. You have no responsibility to provide others with endless patience, and it is not your responsibility to fix a toxic culture. You can always log off and try something else. There are many communities which will welcome and support you–it may just take a few tries to find the right fit.

If you don’t find community, you can build it. Starting your own IRC channel, mailing list, or discussion group with a few friends can be a great way to help each other learn in a supportive environment. And if trolls ever come calling, you’ll be able to ban them personally.

Now, back to problem-solving.

Execute the plan

Sometimes we can make a quick fix in the codebase, test it by hand, and move on. But for more serious problems, we’ll need a more involved process. I always try to get a reproducible test suite–one that runs in a matter of seconds–so that I can continually check my work.

Persist. Many problems require grinding away for some time. Mix blind experimentation with sitting back and planning. Periodically re-evaluate your work–have you made progress? Identified a sub-problem that can be solved independently? Developed a new notation?

If you get stuck, try a new tack. Save your approach as a comment or using git stash, and start fresh. Maybe using a different concurrency primitive is in order, or rephrasing the data structure entirely. Take a reading break and review the documentation for the library you’re trying to use. Read the source code for the functions you’re calling–even if you don’t understand exactly what it does, it might give you clues to how things work under the hood.

Bounce your problem off a friend. Grab a sheet of paper or whiteboard, describe the problem, and work through your thinking with that person. Their understanding of the problem might be totally off-base, but can still give you valuable insight. Maybe they know exactly what the problem is, and can point you to a solution in thirty seconds!

Finally, take a break. Go home. Go for a walk. Lift heavy, run hard, space out, drink with your friends, practice music, read a book. Just before sleep, go over the problem once more in your head; I often wake up with a new algorithm or new questions burning to get out. Your unconscious mind can come up with unexpected insights if given time away from the problem!

Some folks swear by time in the shower, others by hiking, or with pen and paper in a hammock. Find what works for you! The important thing seems to be giving yourself away from struggling with the problem.

Look back

Chances are you’ll know as soon as your solution works. The program compiles, transactions generate the correct amounts, etc. Now’s an important time to solidify your work.

Bolster your tests. You may have made the problem less likely, but not actually solved it. Try a more aggressive, randomized test; one that runs for longer, that generates a broader class of input. Try it on a copy of the production workload before deploying your change.

Identify why the new system works. Pasting something in from StackOverflow may get you through the day, but won’t help you solve similar problems in the future. Try to really understand why the program went wrong, and how the new pieces work together to prevent the problem. Is there a more general underlying problem? Could you generalize your technique to solve a related problem? If you’ll encounter this type of issue frequently, could you build a function or library to help build other solutions?

Document the solution. Write down your description of the problem, and why your changes fix it, as comments in the source code. Use that same description of the solution in your commit message, or attach it as a comment to the resources you used online, so that other people can come to the same understanding.

Debugging Clojure

With these general strategies in mind, I’d like to talk specifically about the debugging Clojure code–especially understanding its stacktraces. Consider this simple program for baking cakes:

(ns scratch.debugging) (defn bake "Bakes a cake for a certain amount of time, returning a cake with a new :tastiness level." [pie temp time] (assoc pie :tastiness (condp (* temp time) < 400 :burned 350 :perfect 300 :soggy)))

And in the REPL

user=> (bake {:flavor :blackberry} 375 10.25) ClassCastException java.lang.Double cannot be cast to clojure.lang.IFn scratch.debugging/bake (debugging.clj:8)

This is not particularly helpful. Let’s print a full stacktrace using pst:

user=> (pst) ClassCastException java.lang.Double cannot be cast to clojure.lang.IFn scratch.debugging/bake (debugging.clj:8) user/eval1223 (form-init4495957503656407289.clj:1) clojure.lang.Compiler.eval (Compiler.java:6619) clojure.lang.Compiler.eval (Compiler.java:6582) clojure.core/eval (core.clj:2852) clojure.main/repl/read-eval-print--6588/fn--6591 (main.clj:259) clojure.main/repl/read-eval-print--6588 (main.clj:259) clojure.main/repl/fn--6597 (main.clj:277) clojure.main/repl (main.clj:277) clojure.tools.nrepl.middleware.interruptible-eval/evaluate/fn--591 (interruptible_eval.clj:56) clojure.core/apply (core.clj:617) clojure.core/with-bindings* (core.clj:1788)

The first line tells us the type of the error: a ClassCastException. Then there’s some explanatory text: we can’t cast a java.lang.Double to a clojure.lang.IFn. The indented lines show the functions that led to the error. The first line is the deepest function, where the error actually occurred: the bake function in the scratch.debugging namespace. In parentheses is the file name (debugging.clj) and line number (8) from the code that caused the error. Each following line shows the function that called the previous line. In the REPL, our code is invoked from a special function compiled by the REPL itself–with an automatically generated name like user/eval1223, and that function is invoked by the Clojure compiler, and the REPL tooling. Once we see something like Compiler.eval at the repl, we can generally skip the rest.

As a general rule, we want to look at the deepest (earliest) point in the stacktrace that we wrote. Sometimes an error will arise from deep within a library or Clojure itself–but it was probably invoked by our code somewhere. We’ll skim down the lines until we find our namespace, and start our investigation at that point.

Our case is simple: bake.clj, on line 8, seems to be the culprit.

(condp (* temp time) <

Now let’s consider the error itself: ClassCastException: java.lang.Double cannot be cast to clojure.lang.IFn. This implies we had a Double and tried to cast it to an IFn–but what does “cast” mean? For that matter, what’s a Double, or an IFn?

A quick google search for java.lang.Double reveals that it’s a class (a Java type) with some basic documentation. “The Double class wraps a value of the primitive type double in an object” is not particularly informative–but the “class hierarchy” at the top of the page shows that a Double is a kind of java.lang.Number. Let’s experiment at the REPL:

user=> (type 4) java.lang.Long user=> (type 4.5) java.lang.Double

Indeed: decimal numbers in Clojure appear to be doubles. One of the expressions in that condp call was probably a decimal. At first we might suspect the literal values 300, 350, or 400–but those are Longs, not Doubles. The only Double we passed in was the time duration 10.25–which appears in condp as (* temp time). That first argument was a Double, but should have been an IFn.

What the heck is an IFn? Its source code has a comment:

IFn provides complete access to invoking any of Clojure’s API’s. You can also access any other library written in Clojure, after adding either its source or compiled form to the classpath.

So IFn has to do with invoking Clojure’s API. Ah–Fn probably stands for function–and this class is chock full of things like invoke(Object arg1, Object arg2). That suggests that IFn is about calling functions. And the I? Google suggests it’s a Java convention for an interface–whatever that is. Remember, we don’t have to understand everything–just enough to get by. There’s plenty to explore later.

Let’s check our hypothesis in the repl:

user=> (instance? clojure.lang.IFn 2.5) false user=> (instance? clojure.lang.IFn conj) true user=> (instance? clojure.lang.IFn (fn [x] (inc x))) true

So Doubles aren’t IFns–but Clojure built-in functions, and anonymous functions, both are. Let’s double-check the docs for condp again:

user=> (doc condp) ------------------------- clojure.core/condp ([pred expr & clauses]) Macro Takes a binary predicate, an expression, and a set of clauses. Each clause can take the form of either: test-expr result-expr test-expr :>> result-fn Note :>> is an ordinary keyword. For each clause, (pred test-expr expr) is evaluated. If it returns logical true, the clause is a match. If a binary clause matches, the result-expr is returned, if a ternary clause matches, its result-fn, which must be a unary function, is called with the result of the predicate as its argument, the result of that call being the return value of condp. A single default expression can follow the clauses, and its value will be returned if no clause matches. If no default expression is provided and no clause matches, an IllegalArgumentException is thrown.clj

That’s a lot to take in! No wonder we got it wrong! We’ll take it slow, and look at the arguments.

(condp (* temp time) <

Our pred was (* temp time) (a Double), and our expr was the comparison function <. For each clause, (pred test-expr expr) is evaluated, so that would expand to something like

((* temp time) 400 <)

Which evaluates to something like

(123.45 400 <)

But this isn’t a valid Lisp program! It starts with a number, not a function. We should have written (< 123.45 400). Our arguments are backwards!

(defn bake "Bakes a cake for a certain amount of time, returning a cake with a new :tastiness level." [pie temp time] (assoc pie :tastiness (condp < (* temp time) 400 :burned 350 :perfect 300 :soggy))) user=> (use 'scratch.debugging :reload) nil user=> (bake {:flavor :chocolate} 375 10.25) {:tastiness :burned, :flavor :chocolate} user=> (bake {:flavor :chocolate} 450 0.8) {:tastiness :perfect, :flavor :chocolate}

Mission accomplished! We read the stacktrace as a path to a part of the program where things went wrong. We identified the deepest part of that path in our code, and looked for a problem there. We discovered that we had reversed the arguments to a function, and after some research and experimentation in the REPL, figured out the right order.

An aside on types: some languages have a stricter type system than Clojure’s, in which the types of variables are explicitly declared in the program’s source code. Those languages can detect type errors–when a variable of one type is used in place of another, incompatible, type–and offer more precise feedback. In Clojure, the compiler does not generally enforce types at compile time, which allows for significant flexibility–but requires more rigorous testing to expose these errors.

Higher order stacktraces

The stacktrace shows us a path through the program, moving downwards through functions. However, that path may not be straightforward. When data is handed off from one part of the program to another, the stacktrace may not show the origin of an error. When functions are handed off from one part of the program to another, the resulting traces can be tricky to interpret indeed.

For instance, say we wanted to make some picture frames out of wood, but didn’t know how much wood to buy. We might sketch out a program like this:

(defn perimeter "Given a rectangle, returns a vector of its edge lengths." [rect] [(:x rect) (:y rect) (:z rect) (:y rect)]) (defn frame "Given a mat width, and a photo rectangle, figure out the size of the frame required by adding the mat width around all edges of the photo." [mat-width rect] (let [margin (* 2 rect)] {:x (+ margin (:x rect)) :y (+ margin (:y rect))})) (def failure-rate "Sometimes the wood is knotty or we screw up a cut. We'll assume we need a spare segment once every 8." 1/8) (defn spares "Given a list of segments, figure out roughly how many of each distinct size will go bad, and emit a sequence of spare segments, assuming we screw up `failure-rate` of them." [segments] (->> segments ; Compute a map of each segment length to the number of ; segments we'll need of that size. frequencies ; Make a list of spares for each segment length, ; based on how often we think we'll screw up. (mapcat (fn [ [segment n]] (repeat (* failure-rate n) segment))))) (def cut-size "How much extra wood do we need for each cut? Let's say a mitred cut for a 1-inch frame needs a full inch." 1) (defn total-wood [mat-width photos] "Given a mat width and a collection of photos, compute the total linear amount of wood we need to buy in order to make frames for each, given a 2-inch mat." (let [segments (->> photos ; Convert photos to frame dimensions (map (partial frame mat-width)) ; Convert frames to segments (mapcat perimeter))] ; Now, take segments (->> segments ; Add the spares (concat (spares segments)) ; Include a cut between each segment (interpose cut-size) ; And sum the whole shebang. (reduce +)))) (->> [{:x 8 :y 10} {:x 10 :y 8} {:x 20 :y 30}] (total-wood 2) (println "total inches:"))

Running this program yields a curious stacktrace. We’ll print the full trace (not the shortened one that comes with pst) for the last exception *e with the .printStackTrace function.

user=> (.printStackTrace *e) java.lang.ClassCastException: clojure.lang.PersistentArrayMap cannot be cast to java.lang.Number, compiling:(scratch/debugging.clj:73:23) at clojure.lang.Compiler.load(Compiler.java:7142) at clojure.lang.RT.loadResourceScript(RT.java:370) at clojure.lang.RT.loadResourceScript(RT.java:361) at clojure.lang.RT.load(RT.java:440) at clojure.lang.RT.load(RT.java:411) ... at java.lang.Thread.run(Thread.java:745) Caused by: java.lang.ClassCastException: clojure.lang.PersistentArrayMap cannot be cast to java.lang.Number at clojure.lang.Numbers.multiply(Numbers.java:146) at clojure.lang.Numbers.multiply(Numbers.java:3659) at scratch.debugging$frame.invoke(debugging.clj:26) at clojure.lang.AFn.applyToHelper(AFn.java:156) at clojure.lang.AFn.applyTo(AFn.java:144) at clojure.core$apply.invoke(core.clj:626) at clojure.core$partial$fn__4228.doInvoke(core.clj:2468) at clojure.lang.RestFn.invoke(RestFn.java:408) at clojure.core$map$fn__4245.invoke(core.clj:2557) at clojure.lang.LazySeq.sval(LazySeq.java:40) at clojure.lang.LazySeq.seq(LazySeq.java:49) at clojure.lang.RT.seq(RT.java:484) at clojure.core$seq.invoke(core.clj:133) at clojure.core$map$fn__4245.invoke(core.clj:2551) at clojure.lang.LazySeq.sval(LazySeq.java:40) at clojure.lang.LazySeq.seq(LazySeq.java:49) at clojure.lang.RT.seq(RT.java:484) at clojure.core$seq.invoke(core.clj:133) at clojure.core$apply.invoke(core.clj:624) at clojure.core$mapcat.doInvoke(core.clj:2586) at clojure.lang.RestFn.invoke(RestFn.java:423) at scratch.debugging$total_wood.invoke(debugging.clj:62) ...

First: this trace has two parts. The top-level error (a CompilerException) appears first, and is followed by the exception that caused the CompilerException: a ClassCastException. This makes the stacktrace read somewhat out of order, since the deepest part of the trace occurs in the first line of the last exception. We read C B A then F E D. This is an old convention in the Java language, and the cause of no end of frustration.

Notice that this representation of the stacktrace is less friendly than (pst). We’re seeing the Java Virtual Machine (JVM)’s internal representation of Clojure functions, which look like clojure.core$partial$fn__4228.doInvoke. This corresponds to the namespace clojure.core, in which there is a function called partial, inside of which is an anonymous function, here named fn__4228. Calling a Clojure function is written, in the JVM, as .invoke or .doInvoke.

So: the root cause was a ClassCastException, and it tells us that Clojure expected a java.lang.Number, but found a PersistentArrayMap. We might guess that PersistentArrayMap is something to do with the map data structure, which we used in this program:

user=> (type {:x 1}) clojure.lang.PersistentArrayMap

And we’d be right. We can also tell, by reading down the stacktrace looking for our scratch.debugging namespace, where the error took place: scratch.debugging$frame, on line 26.

(let [margin (* 2 rect)]

There’s our multiplication operation *, which we might assume expands to clojure.lang.Numbers.multiply. But the path to the error is odd.

(->> photos ; Convert photos to frame dimensions (map (partial frame mat-width))

In total-wood, we call (map (partial frame mat-width) photos) right away, so we’d expect the stacktrace to go from total-wood to map to frame. But this is not what happens. Instead, total-wood invokes something called RestFn–a piece of Clojure plumbing–which in turn calls mapcat.

at clojure.core$mapcat.doInvoke(core.clj:2586) at clojure.lang.RestFn.invoke(RestFn.java:423) at scratch.debugging$total_wood.invoke(debugging.clj:62)

Why doesn’t total-wood call map first? Well it did–but map doesn’t actually apply its function to anything in the photos vector when invoked. Instead, it returns a lazy sequence–one which applies frame only when elements are asked for.

user=> (type (map inc (range 10))) clojure.lang.LazySeq

Inside each LazySeq is a box containing a function. When you ask a LazySeq for its first value, it calls that function to return a new sequence–and that’s when frame gets invoked. What we’re seeing in this stacktrace is the LazySeq internal machinery at work–mapcat asks it for a value, and the LazySeq asks map to generate that value.

at clojure.core$partial$fn__4228.doInvoke(core.clj:2468) at clojure.lang.RestFn.invoke(RestFn.java:408) at clojure.core$map$fn__4245.invoke(core.clj:2557) at clojure.lang.LazySeq.sval(LazySeq.java:40) at clojure.lang.LazySeq.seq(LazySeq.java:49) at clojure.lang.RT.seq(RT.java:484) at clojure.core$seq.invoke(core.clj:133) at clojure.core$map$fn__4245.invoke(core.clj:2551) at clojure.lang.LazySeq.sval(LazySeq.java:40) at clojure.lang.LazySeq.seq(LazySeq.java:49) at clojure.lang.RT.seq(RT.java:484) at clojure.core$seq.invoke(core.clj:133) at clojure.core$apply.invoke(core.clj:624) at clojure.core$mapcat.doInvoke(core.clj:2586) at clojure.lang.RestFn.invoke(RestFn.java:423) at scratch.debugging$total_wood.invoke(debugging.clj:62)

In fact we pass through map’s laziness twice here: a quick peek at (source mapcat) shows that it expands into a map call itself, and then there’s a second map: the one we created in in total-wood. Then an odd thing happens–we hit something called clojure.core$partial$fn__4228.

(map (partial frame mat-width) photos)

The frame function takes two arguments: a mat width and a photo. We wanted a function that takes just one argument: a photo. (partial frame mat-width) took mat-width and generated a new function which takes one arg–call it photo–and calls (frame mad-width photo). That automatically generated function, returned by partial, is what map uses to generate new elements of its sequence on demand.

user=> (partial + 1) #<core$partial$fn__4228 clojure.core$partial$fn__4228@243634f2> user=> ((partial + 1) 4) 5

That’s why we see control flow through clojure.core$partial$fn__4228 (an anonymous function defined inside clojure.core/partial) on the way to frame.

Caused by: java.lang.ClassCastException: clojure.lang.PersistentArrayMap cannot be cast to java.lang.Number at clojure.lang.Numbers.multiply(Numbers.java:146) at clojure.lang.Numbers.multiply(Numbers.java:3659) at scratch.debugging$frame.invoke(debugging.clj:26) at clojure.lang.AFn.applyToHelper(AFn.java:156) at clojure.lang.AFn.applyTo(AFn.java:144) at clojure.core$apply.invoke(core.clj:626) at clojure.core$partial$fn__4228.doInvoke(core.clj:2468)

And there’s our suspect! scratch.debugging/frame, at line 26. To return to that line again:

(let [margin (* 2 rect)]

* is a multiplication, and 2 is obviously a number, but rect… rect is a map here. Aha! We meant to multiply the mat-width by two, not the rectangle.

(defn frame "Given a mat width, and a photo rectangle, figure out the size of the frame required by adding the mat width around all edges of the photo." [mat-width rect] (let [margin (* 2 mat-width)] {:x (+ margin (:x rect)) :y (+ margin (:y rect))}))

I believe we’ve fixed the bug, then. Let’s give it a shot!

The unbearable lightness of nil

There’s one more bug lurking in this program. This one’s stacktrace is short.

user=> (use 'scratch.debugging :reload) CompilerException java.lang.NullPointerException, compiling:(scratch/debugging.clj:73:23) user=> (pst) CompilerException java.lang.NullPointerException, compiling:(scratch/debugging.clj:73:23) clojure.lang.Compiler.load (Compiler.java:7142) clojure.lang.RT.loadResourceScript (RT.java:370) clojure.lang.RT.loadResourceScript (RT.java:361) clojure.lang.RT.load (RT.java:440) clojure.lang.RT.load (RT.java:411) clojure.core/load/fn--5066 (core.clj:5641) clojure.core/load (core.clj:5640) clojure.core/load-one (core.clj:5446) clojure.core/load-lib/fn--5015 (core.clj:5486) clojure.core/load-lib (core.clj:5485) clojure.core/apply (core.clj:626) clojure.core/load-libs (core.clj:5524) Caused by: NullPointerException clojure.lang.Numbers.ops (Numbers.java:961) clojure.lang.Numbers.add (Numbers.java:126) clojure.core/+ (core.clj:951) clojure.core.protocols/fn--6086 (protocols.clj:143) clojure.core.protocols/fn--6057/G--6052--6066 (protocols.clj:19) clojure.core.protocols/seq-reduce (protocols.clj:27) clojure.core.protocols/fn--6078 (protocols.clj:53) clojure.core.protocols/fn--6031/G--6026--6044 (protocols.clj:13) clojure.core/reduce (core.clj:6287) scratch.debugging/total-wood (debugging.clj:69) scratch.debugging/eval1560 (debugging.clj:81) clojure.lang.Compiler.eval (Compiler.java:6703)

On line 69, total-wood calls reduce, which dives through a series of functions from clojure.core.protocols before emerging in +: the function we passed to reduce. Reduce is trying to combine two elements from its collection of wood segments using +, but one of them was nil. Clojure calls this a NullPointerException. In total-wood, we constructed the sequence of segments this way:

(let [segments (->> photos ; Convert photos to frame dimensions (map (partial frame mat-width)) ; Convert frames to segments (mapcat perimeter))] ; Now, take segments (->> segments ; Add the spares (concat (spares segments)) ; Include a cut between each segment (interpose cut-size) ; And sum the whole shebang. (reduce +))))

Where did the nil value come from? The stacktrace doesn’t say, because the sequence reduce is traversing didn’t have any problem producing the nil. reduce asked for a value and the sequence happily produced a nil. We only had a problem when it came time to combine the nil with the next value, using +.

A stacktrace like this is something like a murder mystery: we know the program died in the reducer, that it was shot with a +, and the bullet was a nil–but we don’t know where the bullet came from. The trail runs cold. We need more forensic information–more hints about the nil’s origin–to find the culprit.

Again, this is a class of error largely preventable with static type systems. If you have worked with a statically typed language in the past, it may be interesting to consider that almost every Clojure function takes Option[A] and does something more-or-less sensible, returning Option[B]. Whether the error propagates as a nil or an Option, there can be similar difficulties in localizing the cause of the problem.

Let’s try printing out the state as reduce goes along:

(->> segments ; Add the spares (concat (spares segments)) ; Include a cut between each segment (interpose cut-size) ; And sum the whole shebang. (reduce (fn [acc x] (prn acc x) (+ acc x)))))) user=> (use 'scratch.debugging :reload) 12 1 13 14 27 1 28 nil CompilerException java.lang.NullPointerException, compiling:(scratch/debugging.clj:73:56)

Not every value is nil! There’s a 14 there which looks like a plausible segment for a frame, and two one-inch buffers from cut-size. We can rule out interpose because it inserts a 1 every time, and that 1 reduces correctly. But where’s that nil coming from? Is from segments or (spares segments)?

(let [segments (->> photos ; Convert photos to frame dimensions (map (partial frame mat-width)) ; Convert frames to segments (mapcat perimeter))] (prn :segments segments) user=> (use 'scratch.debugging :reload) :segments (12 14 nil 14 14 12 nil 12 24 34 nil 34)

It is present in segments. Let’s trace it backwards through the sequence’s creation. It’d be handy to have a function like prn that returned its input, so we could spy on values as they flowed through the ->> macro.

(defn spy [& args] (apply prn args) (last args)) (let [segments (->> photos ; Convert photos to frame dimensions (map (partial frame mat-width)) (spy :frames) ; Convert frames to segments (mapcat perimeter))] user=> (use 'scratch.debugging :reload) :frames ({:x 12, :y 14} {:x 14, :y 12} {:x 24, :y 34}) :segments (12 14 nil 14 14 12 nil 12 24 34 nil 34)

Ah! So the frames are intact, but the perimeters are bad. Let’s check the perimeter function:

(defn perimeter "Given a rectangle, returns a vector of its edge lengths." [rect] [(:x rect) (:y rect) (:z rect) (:y rect)])

Spot the typo? We wrote :z instead of :x. Since the frame didn’t have a :z field, it returned nil! That’s the origin of our NullPointerException. With the bug fixed, we can re-run and find:

user=> (use 'scratch.debugging :reload) total inches: 319

Whallah!

Recap

As we solve more and more problems, we get faster at debugging–at skipping over irrelevant log data, figuring out exactly what input was at fault, knowing what terms to search for, and developing a network of peers and mentors to ask for help. But when we encounter unexpected bugs, it can help to fall back on a family of problem-solving tactics.

We explore the problem thoroughly, localizing it to a particular function, variable, or set of inputs. We identify the boundaries of the problem, carving away parts of the system that work as expected. We develop new notation, maps, and diagrams of the problem space, precisely characterizing it in a variety of modes.

With the problem identified, we search for extant solutions–or related problems others have solved in the past. We trawl through issue trackers, mailing list posts, blogs, and forums like Stackoverflow, or, for more theoretical problems, academic papers, Mathworld, and Wikipedia, etc. If searching reveals nothing, we try rephrasing the problem, relaxing the constraints, adding debugging statements, and solving smaller subproblems. When all else fails, we ask for help from our peers, or from the community in IRC, mailing lists, and so on, or just take a break.

We learned to explore Clojure stacktraces as a trail into our programs, leading to the place where an error occurred. But not all paths are linear, and we saw how lazy operations and higher-order functions create inversions and intermediate layers in the stacktrace. Then we learned how to debug values that were distant from the trace, by adding logging statements and working our way closer to the origin.

Programming languages and us, their users, are engaged in a continual dialogue. We may speak more formally, verbosely, with many types and defensive assertions–or we may speak quickly, generally, in fuzzy terms. The more precise we are with the specifications of our program’s types, the more the program can assist us when things go wrong. Conversely, those specifications harden our programs into strong but rigid forms, and rigid structures are harder to bend into new shapes.

In Clojure we strike a more dynamic balance: we speak in generalities, but we pay for that flexibility. Our errors are harder to trace to their origins. While the Clojure compiler can warn us of some errors, like mis-spelled variable names, it cannot (without a library like core.typed) tell us when we have incorrectly assumed an object will be of a certain type. Even very rigid languages, like Haskell, cannot identify some errors, like reversing the arguments to a subtraction function. Some tests are always necessary, though types are a huge boon.

No matter what language we write in, we use a balance of types and tests to validate our assumptions, both when the program is compiled and when it is run.

The errors that arise in compilation or runtime aren’t rebukes so much as hints. Don’t despair! They point the way towards understanding one’s program in more detail–though the errors may be cryptic. Over time we get better at reading our language’s errors and making our programs more robust.

Earlier versions of Jepsen found glaring inconsistencies, but missed subtle ones. In particular, Jepsen was not well equipped to distinguish linearizable systems from sequentially or causally consistent ones. When people asked me to analyze systems which claimed to be linearizable, Jepsen could rule out obvious classes of behavior, like dropping writes, but couldn’t tell us much more than that. Since users and vendors are starting to rely on Jepsen as a basic check on correctness, it’s important that Jepsen be able to identify true linearization errors.

To understand why Jepsen was not a complete test of linearizability, we have to understand the structure of its original tests. Jepsen assumed, originally, that every system could be modeled as a set of integers. Each client would gradually add a sequence of integers–disjoint from all the other client sets–to the database’s set; then perform a final read. If any elements which had supposedly succeeded were missing, we know the system dropped data.

The original Jepsen tests were designed for AP systems, like Riak, without a linear order; using a set is appropriate because its contents are fundamentally unordered, and because addition to the set is associative and idempotent. To test a linearizable system, we implement set addition by performing a compare-and-set, replacing the old set with the current value plus the number being written. If a given CAS was successful, then that element should appear in the final read.

This does verify sequential consistency, and to varying degrees linearizability, but has limited power. The database may choose, for instance, to delay the visibility of changes, so long as they become visible before the final read. We can’t test operations other than a CAS. We can’t, for instance, test deletions. It’s also not clear how to verify systems like mutexes, queues, or semaphores.

Furthermore, if a test does fail, it’s not clear why. A missing number from the final set might be caused by a problem with that particular CAS–or a CAS executed hours later which happened to destroy the effects of a preceding write. Ideally, we’d like to know exactly why the system failed to linearize. With this in mind, I set out to design a linearizability checker suitable for analyzing both formal models and real software with no internal visibility.

Knossos

In the introduction to Knossos, I couched Knossos as a model checker, motivated by a particular algorithm discussed on the Redis mailing list. This was slightly disingenuous: in fact, I designed Knossos as a model checker for any type of history, including those recorded from real databases. This means that Jepsen can generate a series of random operations, execute them against a database, and verify that the resulting history is valid with respect to some model.

Given a sequence of operations that a database might go through–say, two processes attempting to acquire a mutex:

{:process 1, :type :invoke, :f :acquire, :value nil} {:process 2, :type :invoke, :f :acquire, :value nil} {:process 1, :type :ok, :f :acquire, :value nil} {:process 2, :type :fail :f :acquire, :value "lock failed; already held"}

… and a singlethreaded model of the system, like

(defrecord Mutex [locked?] Model (step [mutex op] (condp = (:f op) :acquire (if locked? (inconsistent "already held") (Mutex. true)) :release (if locked? (Mutex. false) (inconsistent "not held")))))

… Knossos can identify if the given concurrent history linearizes–that is, whether there exists some equivalent history in which every operation appears to take place atomically, in a well-defined order, between the invocation and completion times.

Linearizability, like sequential and serializable consistency, requires that every operation take place in some specific order; that there appears to be only one “true” state for the system at any given time. Therefore we can model any linearizable system as a single state, plus a function, called step, which applies an operation to that state and returns a new state.

In Clojure, we represent this model with a simple protocol, called Model, which defines a function (step current-model-state operation), and returns the new state. In our mutex example, there are four possibilities, depending on whether the operation is :acquire or :release, and whether the state locked? is true. If we try to lock an unlocked mutex, we return a new Mutex with the state true. If we try to lock a mutex which is already locked, we return a special kind of state: an inconsistent state.

Inconsistent states allow us to verify that a singlethreaded history is valid. We simply (reduce step initial-state operations); if the the result is inconsistent, we know that sequence of operations was prohibited by the model. The model formally expresses our definition of the allowable causal histories.

The plot thickens

But we don’t have a singlethreaded history to test. We have a multithreaded history, with any number of operations in play concurrently. Each client is invoking, waiting for, and then discovering the result of its operations. Our history contains pairs of :invoke, :ok messages, when an operation succeeds, or :invoke, :fail when the operation is known to not have taken place, or :invoke, :info, when we simply don’t know what happened.

If an operation times out, or the server returns an indeterminate response, we may never find out whether the operation really took place. In the history to the right, process 5 has hung and will never recover. Its operation could take place at any time, even years into the future. In general, a hung process is concurrent with every other subsequent operation.

Given a model, we know how to test if a particular sequence of operations is valid. But in a concurrent history, the ordering is ambiguous; each operation could take place at any time between its invocation and completion. One possible interleaving might be read 1, write 1, read 2, write 2, which is obviously incorrect. On the other hand, we could evaluate write 1, read 1, write 2, read 2 instead–which is a valid history for a register. This history is linearizable–but in order to prove that fact, we have to find a particular valid order.

Imagine something like a game of hopscotch: one must land on each cell in turn, always moving from left to right, finding a path in which the model’s constraints hold. Where there are many cells at the same time, finding a path becomes especially difficult. We must consider every possible permutation of those concurrent cells, which is O(n!). That’s the kind of hopscotch that, even when played by computer, makes one re-evaluate one’s life choices.

So what do we do, presented with a huge space of possibilities?

Exploit degeneracy

I’m a degenerate sort of person, so my first inclination is to look for symmetries in the state space. The key observation to make is that whether a given operation is valid or not depends solely on the current state of the model, not its history.

step(state, op) -> state'

It doesn’t matter how we got to the state; if you give me two registers containing the value 2, and ask me to apply the same operation to both, we only need to check one of the registers, because the results will be equivalent!

Unlike a formal model-checker or proof assistant, Knossos doesn’t know the structure of the system it’s analyzing; it can’t perform symmetry reduction based on the definition of step. What we can do, however, is look for cases where we come back to the same state and the same future series of operations–and when that occurs, drop all but one of the cases immediately–and this turns out to be equivalent to a certain class of symmetry reduction. In particular, we can compact interchangeable orders like concurrent reads, or writes that lead to the same value, etc. We keep a cache of visited worlds and avoid exploring any that have been seen before.

Laziness

Remember, we’re looking for any linearization, not all of them. If we can find a shortcut by not evaluating some highly-branching history, by not taking some expensive path, we can skip huge parts of the search. Like a lightning bolt feeling its way down the path of least resistance, we evaluate only those paths which seem easiest–coming back to the hard ones later. If the history is truly not linearizable, we’re forced to return to those expensive branches and check them, but if the history is valid, we can finish as soon as a single path is found.

Lazy evaluation is all about making control flow explicit instead of implicit. We use a data structure to describe where to explore next, instead of following the normal program flow. In Knossos, we represent the exploration of a particular order of operations as a world, which sits at some index along the multithreaded history. Each world carries with it a fixed history–the specific order of operations that occurred in that possible universe. The fixed history leads to a current model state. Finally, each world has a set of pending operations: operations that have been invoked, but have not yet taken effect.

For example, a world might have a fixed history of lock, unlock, lock, leading to a model state where locked is true, and a second lock attempt might be pending but not yet applied. An unlock operation could arrive and allow the pending lock to take place.

By representing the entire state of the computation as a data structure, we can write a single function that takes a world and explores it, returning a set of potential future worlds. We can explore those worlds in parallel.

Parallelization

Because our states are immutable representations of the computation, and the function we use to explore any given state is pure and deterministic, we can trivially parallelize the exploration process. Early versions of Knossos reduced over each operation in the history, applying that operation to every outstanding world by whacking it with a parallel map.

This parallelization strategy has a serious drawback, though: by exploring the state space one index at a time, we effectively perform a breadth-first search. We want to take shortcuts through the state space; running many searches at once. We don’t just want depth-first, either; instead, we want to explore those worlds which have the lowest branching factor, because those worlds are the cheapest to explore.

So instead of exploring the history one operation at a time, we spawn lots of threads and have each consume from a priority queue of worlds, ranked by how awful those worlds are to explore. As each explorer thread discovers new consequent worlds, it inserts them back into the pool. If any thread finds a world that encompasses every operation in the history, we’ve demonstrated the history is linearizable.

We pay some cost in synchronization: queues aren’t cheap, and the java.util.concurrent.BlockingPriorityQueue has some particularly nasty contention costs for both enqueues and dequeues. Luckily, the queue will usually contain plenty of elements, so we can stripe the queue into several subqueues, each with thread affinity. Affinity for each queue reduces lock contention, which dramatically reduces the time threads spend waiting to enqueue or dequeue worlds. When a thread exhausts its local queue, it steals worlds from its neighbors.

This approach costs us some degree of memory locality: transferring records through the queue tends to push them out of the CPU cache. We can tune how far each explorer thread will take a particular world to reduce the locality cost: if work is too chunky, threads can starve awaiting worlds to explore–but if work is too fine-grained, synchronization and cache misses dominate.

Memoization

Making control flow explicit (some might even say monadic) allows us to memoize computation as well. At RICON East, in 2013, Margo Seltzer gave a phenomenal talk on automatically parallelizing singlethreaded x86 programs. She pointed out that x86 can be thought of as a very large, very complicated, function that transforms a bit-vector of all the registers and all of memory into some subsequent state–depending on the instruction pointer, contents of registers, etc. It’s a very large value, but if you compress it and make even some modest predictions you can cache the results of computations that haven’t even happened yet, allowing the program to jump forward when it encounters a known state.

This works because parallel programs usually don’t change the entire memory space; they often read and write only a small portion of memory. for(i = 0; i < 100; i++) { arr[i]++ }, for instance, independently increments each number in arr. In that sense, the memory space is degenerate outside each particular element. That degeneracy allows speculative execution to have a chance of predicting an equivalent future state of the program: we can increment each number concurrently.

In Knossos we have a similarly degenerate state space; all fixed histories may be collapsed so long as the model and pending operations are identical. We also have a speculative and lazy execution strategy: operations are simultaneously explored at various points in the multiverse. Hence we can apply a similar memoization strategy: by caching visited worlds, we can avoid exploring equivalent paths twice.

In fact we don’t even need to store the results of the exploration, simply that we have reached that world. Think of exploring a maze with several friends, all looking for a path through. When anyone reaches a dead end, they can save time for everyone by coloring in the path they took. When someone comes to a branch in the maze, they only take the paths that nobody has colored in. We simply abort any exploration of a world equivalent to one already visited. This optimization is nondeterministic but synchronization-free, allowing memoization checks to be extremely cheap. Even though cache hitrates are typically low, each hit prunes an exponential number of descendant worlds, dramatically reducing runtimes.

Immutability and performance

When we explore a world, we’ll typically encounter many branching paths. Given two concurrent writes a and b, we need to explore [], [a], [b], [a b], and [b a], and in turn, each of those worlds will fork into hundreds, then thousands, then millions of consequent worlds. We have to make a lot of copies.

At this point in the essay, Haskell enthusiasts are nodding their heads sagely and muttering things about Coyoneda diffeomorphisms and trendofunctors. Haskell offers excellent support for immutable data structures and parallel execution of pure functions, which would make it an ideal choice for building this kind of checker.

But I am, sadly, not a Haskell wizard. When you get right down to it, I’m more of a Clojure Sith Lord. And as it turns out, this is a type of problem that Clojure is also well-suited for. We express the consistency model as a pure function over immutable models, and use Clojure’s immutable maps, vectors, and sets to store the state of each world, its histories, its pending operations, and so on. Forking the world into distinct paths doesn’t require copying the entire state; rather, Clojure uses a reference to the original data structure, and stores a delta on top. We can fork millions of worlds cheaply.

Because worlds are immutable, we can share them freely between threads. Because the functions that explore a world, returning subsequent possible worlds, are pure, we can explore worlds on any thread, at any time, and take advantage of memoization. But in order to execute that search process in parallel, we need that priority queue of worlds-at-the-edge: a fundamentally mutable data structure. The memoizing cache is also mutable: it must be, to share state between threads. We also need some book-keeping state: how far has the algorithm explored; have we reached the end; how large is the cache.

So as a layer atop the immutable core, we make limited use of mutable structures: a striped java.util.concurrent.PriorityQueue for keeping track of which worlds are up next, a concurrent hashmap to memoize results, Clojure’s atoms for bookkeeping, and some java.util.concurrent.atomic references for primitive CAS. Because this code is wildly nondeterministic, it’s the most difficult portion of Knossos to reason about and debug–yet that nondeterminism is a critical degree of freedom for parallel execution. By broadening the space of allowable execution orders, we reduce the need for inter-core synchronization.

Reducing synchronization is especially important because while I was working on Knossos, Comcast offered me a research grant specifically for Jepsen. As one does when offered unlimited resources by a galactic empire, I thought big.

I used Comcast’s grant to build a 24-core (48 HT) Xeon with 128GB of ECC; effectively demolishing the parallelism and heap barriers that limited earlier verification efforts. Extensive profiling with Yourkit (another great supporter of open-source projects) helped reduce lock and CAS contention which limited scalability to ~4 cores; a few weeks work removed almost all thread stalls and improved performance by two orders of magnitude.

The result is that Knossos can check 5-process, 150–200-element histories in a matter of minutes, not days–and it can do it on 48 cores.

There are several optimizations I haven’t made yet; for instance, detecting crashed processes and optimistically inserting a world in which that crashed process' operation never takes place. However, Knossos at this stage is more than capable of detecting linearization errors in real-world histories.

Proud of this technological terror I’d constructed, I consulted the small Moff Tarkin that lives in my head on what database to test next. “You would prefer another target? An open-source target? Then name the distributed system!”

“RabbitMQ. They’re on RabbitMQ.”

Previously: Logistics

Until this point in the book, we’ve dealt primarily in specific details: what an expression is, how math works, which functions apply to different data structures, and where code lives. But programming, like speaking a language, painting landscapes, or designing turbines, is about more than the nuts and bolts of the trade. It’s knowing how to combine those parts into a cohesive whole–and this is a skill which is difficult to describe formally. In this part of the book, I’d like to work with you on an integrative tour of one particular problem: modeling a rocket in flight.

We’re going to reinforce our concrete knowledge of the standard library by using maps, sequences, and math functions together. At the same time, we’re going to practice how to represent a complex system; decomposing a problem into smaller parts, naming functions and variables, and writing tests.

So you want to go to space

First, we need a representation of a craft. The obvious properties for a rocket are its dry mass (how much it weighs without fuel), fuel mass, position, velocity, and time. We’ll create a new file in our scratch project–src/scratch/rocket.clj–to talk about spacecraft.

For starters, let’s pattern our craft after an Atlas V launch vehicle. We’ll represent everything in SI units–kilograms, meters, newtons, etc. The Atlas V carries 627,105 lbs of LOX/RP-1 fuel, and a total mass of 334,500 kg gives only 50,050 kg of mass which isn’t fuel. It develops 4152 kilonewtons of thrust and runs for 253 seconds, with a specific impulse (effectively, exhaust velocity) of 3.05 kilometers/sec. Real rockets develop varying amounts of thrust depending on the atmosphere, but we’ll pretend it’s constant in our simulation.

(defn atlas-v [] {:dry-mass 50050 :fuel-mass 284450 :time 0 :isp 3050 :max-fuel-rate (/ 284450 253) :max-thrust 4.152e6})

How heavy is the craft?

(defn mass "The total mass of a craft." [craft] (+ (:dry-mass craft) (:fuel-mass craft)))

What about the position and velocity? We could represent them in Cartesian coordinates–x, y, and z–or we could choose spherical coordinates: a radius from the planet and angle from the pole and 0 degrees longitude. I’ve got a hunch that spherical coordinates will be easier for position, but accelerating the craft will be simplest in in x, y, and z terms. The center of the planet is a natural choice for the coordinate system’s origin (0, 0, 0). We’ll choose z along the north pole, and x and y in the plane of the equator.

Let’s define a space center where we launch from–let’s say it’s initially on the equator at y=0. To figure out the x coordinate, we’ll need to know how far the space center is from the center of the earth. The earth’s equatorial radius is ~6378 kilometers.

(def earth-equatorial-radius "Radius of the earth, in meters" 6378137)

How fast is the surface moving? Well the earth’s day is 86,400 seconds long,

(def earth-day "Length of an earth day, in seconds." 86400)

which means a given point on the equator has to go 2 * pi * equatorial radius meters in earth-day seconds:

(def earth-equatorial-speed "How fast points on the equator move, relative to the center of the earth, in meters/sec." (/ (* 2 Math/PI earth-equatorial-radius) earth-day))

So our space center is on the equator (z=0), at y=0 by choice, which means x is the equatorial radius. Since the earth is spinning, the space center is moving at earth-equatorial-speed in the y direction–and not changing at all in x or z.

(def initial-space-center "The initial position and velocity of the launch facility" {:time 0 :position {:x earth-equatorial-radius :y 0 :z 0} :velocity {:x 0 :y earth-equatorial-speed :z 0}})

:position and :velocity are both vectors, in the sense that they describe a position, or a direction, in terms of x, y, and z components. This is a different kind of vector than a Clojure vector, like [1 2 3]. We’re actually representing these logical vectors as Clojure maps, with :x, :y, and :z keys, corresponding to the distance along the x, y, and z directions, from the center of the earth. Throughout this chapter, I’ll mainly use the term coordinates to talk about these structures, to avoid confusion with Clojure vectors.

Now let’s create a function which positions our craft on the launchpad at time 0. We’ll just merge the spacecraft’s with the initial space center, overwriting the craft’s time and space coordinates.

(defn prepare "Prepares a craft for launch from an equatorial space center." [craft] (merge craft initial-space-center))

Forces

Gravity continually pulls the spacecraft towards the center of the Earth, accelerating it by 9.8 meters/second every second. To figure out what direction is towards the Earth, we’ll need the angles of a spherical coordinate system. We’ll use the trigonometric functions from java.lang.Math.

(defn magnitude "What's the radius of a given set of cartesian coordinates?" [c] ; By the Pythagorean theorem... (Math/sqrt (+ (Math/pow (:x c) 2) (Math/pow (:y c) 2) (Math/pow (:z c) 2)))) (defn cartesian->spherical "Converts a map of Cartesian coordinates :x, :y, and :z to spherical coordinates :r, :theta, and :phi." [c] (let [r (magnitude c)] {:r r :theta (Math/acos (/ (:z c) r)) :phi (Math/atan (/ (:y c) (:x c)))})) (defn spherical->cartesian "Converts spherical to Cartesian coordinates." [c] {:x (* (:r c) (Math/sin (:theta c)) (Math/cos (:phi c))) :y (* (:r c) (Math/sin (:theta c)) (Math/sin (:phi c))) :z (* (:r c) (Math/cos (:phi c)))})

With those angles in mind, computing the gravitational acceleration is easy. We just take the spherical coordinates of the spacecraft, and replace the radius with the total force due to gravity. Then we can transform that spherical force back into Cartesian coordinates.

(def g "Acceleration of gravity in meters/s^2" -9.8) (defn gravity-force "The force vector, each component in Newtons, due to gravity." [craft] ; Since force is mass times acceleration... (let [total-force (* g (mass craft))] (-> craft ; Now we'll take the craft's position :position ; in spherical coordinates, cartesian->spherical ; replace the radius with the gravitational force... (assoc :r total-force) ; and transform back to Cartesian-land spherical->cartesian)))

Rockets produce thrust by consuming fuel. Let’s say the fuel consumption is always the maximum, until we run out:

(defn fuel-rate "How fast is fuel, in kilograms/second, consumed by the craft?" [craft] (if (pos? (:fuel-mass craft)) (:max-fuel-rate craft) 0))

Now that we know how much fuel is being consumed, we can compute the force the rocket engine develops. That force is simply the mass consumed per second times the exhaust velocity–which is the specific impulse :isp. We’ll ignore atmospheric effects.

(defn thrust "How much force, in newtons, does the craft's rocket engines exert?" [craft] (* (fuel-rate craft) (:isp craft)))

Cool. What about the direction of thrust? Just for grins, let’s keep the rocket pointing entirely along the x axis.

(defn engine-force "The force vector, each component in Newtons, due to the rocket engine." [craft] (let [t (thrust craft)] {:x t :y 0 :z 0}))

The total force on a craft is just the sum of gravity and thrust. To sum these maps together, we’ll need a way to sum the x, y, and z components independently. Clojure’s merge-with function combines common fields in maps using a function, so this is surprisingly straightforward.

(defn total-force "Total force on a craft." [craft] (merge-with + (engine-force craft) (gravity-force craft)))

The acceleration of a craft, by Newton’s second law, is force divided by mass. This one’s a little trickier; given {:x 1 :y 2 :z 4} we want to apply a function–say, multiplication by a factor, to each number. Since maps are sequences of key/value pairs…

user=> (seq {:x 1 :y 2 :z 3}) ([:z 3] [:y 2] [:x 1])

… and we can build up new maps out of key/value pairs using into…

user=> (into {} [[:x 4] [:y 5]]) {:x 4, :y 5}

… we can write a function map-values which works like map, but affects the values of a map data structure.

(defn map-values "Applies f to every value in the map m." [f m] (into {} (map (fn [pair] [(key pair) (f (val pair))]) m)))

And that allows us to define a scale function which scales a set of coordinates by some factor:

(defn scale "Multiplies a map of x, y, and z coordinates by the given factor." [factor coordinates] (map-values (partial * factor) coordinates))

What’s that partial thing? It’s a function which takes a function, and some arguments, and returns a new function. What does the new function do? It calls the original function, with the arguments passed to partial, followed by any arguments passed to the new function. In short, (partial * factor) returns a function that takes any number, and multiplies it by factor.

So to divide each component of the force vector by the mass of the craft:

(defn acceleration "Total acceleration of a craft." [craft] (let [m (mass craft)] (scale (/ m) (total-force craft))))

Note that (/ m) returns 1/m. Our scale function can do double-duty as both multiplication and division.

With the acceleration and fuel consumption all figured out, we’re ready to apply those changes over time. We’ll write a function which takes the rocket at a particular time, and returns a version of it dt seconds later.

(defn step [craft dt] (assoc craft ; Time advances by dt seconds :t (+ dt (:t craft)) ; We burn some fuel :fuel-mass (- (:fuel-mass craft) (* dt (fuel-rate craft))) ; Our position changes based on our velocity :position (merge-with + (:position craft) (scale dt (:velocity craft))) ; And our velocity changes based on our acceleration :velocity (merge-with + (:velocity craft) (scale dt (acceleration craft)))))

OK. Let’s save the rocket.clj file, load that code into the REPL, and fire it up.

user=> (use 'scratch.rocket :reload) nil

use is like a shorthand for (:require ... :refer :all). We’re passing :reload because we want the REPL to re-read the file. Notice that in ns declarations, the namespace name scratch.rocket is unquoted–but when we call use or require at the repl, we quote the namespace name.

user=> (atlas-v) {:dry-mass 50050, :fuel-mass 284450, :time 0, :isp 3050, :max-fuel-rate 284450/253, :max-thrust 4152000.0}

Launch

Let’s prepare the rocket. We’ll use pprint to print it in a more readable form.

user=> (-> (atlas-v) prepare pprint) {:velocity {:x 0, :y 463.8312116386399, :z 0}, :position {:x 6378137, :y 0, :z 0}, :dry-mass 50050, :fuel-mass 284450, :time 0, :isp 3050, :max-fuel-rate 284450/253, :max-thrust 4152000.0}

Great; there it is on the launchpad. Wow, even “standing still”, it’s moving at 463 meters/sec because of the earth’s rotation! That means you and I are flying through space at almost half a kilometer every second! Let’s step forward one second in time.

user=> (-> (atlas-v) prepare (step 1) pprint) NullPointerException clojure.lang.Numbers.ops (Numbers.java:942)

In evaluating this expression, Clojure reached a point where it could not continue, and aborted execution. We call this error an exception, and the process of aborting throwing the exception. Clojure backs up to the function which called the function that threw, then the function which called that function, and so on, all the way to the top-level expression. The REPL finally intercepts the exception, prints an error to the console, and stashes the exception object in a special variable *e.

In this case, we know that the exception in question was a NullPointerException, which occurs when a function received nil unexpectedly. This one came from clojure.lang.Numbers.ops, which suggests some sort of math was involved. Let’s use pst to find out where it came from.

user=> (pst *e) NullPointerException clojure.lang.Numbers.ops (Numbers.java:942) clojure.lang.Numbers.add (Numbers.java:126) scratch.rocket/step (rocket.clj:125) user/eval1478 (NO_SOURCE_FILE:1) clojure.lang.Compiler.eval (Compiler.java:6619) clojure.lang.Compiler.eval (Compiler.java:6582) clojure.core/eval (core.clj:2852) clojure.main/repl/read-eval-print--6588/fn--6591 (main.clj:259) clojure.main/repl/read-eval-print--6588 (main.clj:259) clojure.main/repl/fn--6597 (main.clj:277) clojure.main/repl (main.clj:277) clojure.tools.nrepl.middleware.interruptible-eval/evaluate/fn--589 (interruptible_eval.clj:56)

This is called a stack trace: the stack is the context of the program at each function call. It traces the path the computer took in evaluating the expression, from the bottom to the top. At the bottom is the REPL, and Clojure compiler. Our code begins at user/eval1478–that’s the compiler’s name for the expression we just typed. That function called scratch.rocket/step, which in turn called Numbers.add, and that called Numbers.ops. Let’s start by looking at the last function we wrote before calling into Clojure’s standard library: the step function, in rocket.clj, on line 125.

123 (assoc craft 124 ; Time advances by dt seconds 125 :t (+ dt (:t craft))

Ah; we named the time field :time earlier, not :t. Let’s replace :t with :time, save the file, and reload.

user=> (use 'scratch.rocket :reload) nil user=> (-> (atlas-v) prepare (step 1) pprint) {:velocity {:x 0.45154055666826215, :y 463.8312116386399, :z -9.8}, :position {:x 6378137, :y 463.8312116386399, :z 0}, :dry-mass 50050, :fuel-mass 71681400/253, :time 1, :isp 3050, :max-fuel-rate 284450/253, :max-thrust 4152000.0}

Look at that! Our position is unchanged (because our velocity was zero), but our velocity has shifted. We’re now moving… wait, -9.8 meters per second south? That can’t be right. Gravity points down, not sideways. Something must be wrong with our spherical coordinate system. Let’s write a test in test/scratch/rocket_test.clj to explore.

(ns scratch.rocket-test (:require [clojure.test :refer :all] [scratch.rocket :refer :all])) (deftest spherical-coordinate-test (let [pos {:x 1 :y 2 :z 3}] (testing "roundtrip" (is (= pos (-> pos cartesian->spherical spherical->cartesian)))))) aphyr@waterhouse:~/scratch$ lein test lein test scratch.core-test lein test scratch.rocket-test lein test :only scratch.rocket-test/spherical-coordinate-test FAIL in (spherical-coordinate-test) (rocket_test.clj:8) roundtrip expected: (= pos (-> pos cartesian->spherical spherical->cartesian)) actual: (not (= {:z 3, :y 2, :x 1} {:x 1.0, :y 1.9999999999999996, :z 1.6733200530681513})) Ran 2 tests containing 4 assertions. 1 failures, 0 errors. Tests failed.

Definitely wrong. Looks like something to do with the z coordinate, since x and y look OK. Let’s try testing a point on the north pole:

(deftest spherical-coordinate-test (testing "spherical->cartesian" (is (= (spherical->cartesian {:r 2 :phi 0 :theta 0}) {:x 0.0 :y 0.0 :z 2.0}))) (testing "roundtrip" (let [pos {:x 1.0 :y 2.0 :z 3.0}] (is (= pos (-> pos cartesian->spherical spherical->cartesian))))))

That checks out OK. Let’s try some values in the repl.

user=> (cartesian->spherical {:x 0.00001 :y 0.00001 :z 2.0}) {:r 2.00000000005, :theta 7.071068104411588E-6, :phi 0.7853981633974483} user=> (cartesian->spherical {:x 1 :y 2 :z 3}) {:r 3.7416573867739413, :theta 0.6405223126794245, :phi 1.1071487177940904} user=> (spherical->cartesian (cartesian->spherical {:x 1 :y 2 :z 3})) {:x 1.0, :y 1.9999999999999996, :z 1.6733200530681513} user=> (cartesian->spherical {:x 1 :y 2 :z 0}) {:r 2.23606797749979, :theta 1.5707963267948966, :phi 1.1071487177940904} user=> (cartesian->spherical {:x 1 :y 1 :z 0}) {:r 1.4142135623730951, :theta 1.5707963267948966, :phi 0.7853981633974483}

Oh, wait, that looks odd. {:x 1 :y 1 :z 0} is on the equator: phi–the angle from the pole–should be pi/2 or ~1.57, and theta–the angle around the equator–should be pi/4 or 0.78. Those coordinates are reversed! Double-checking our formulas with Wolfram MathWorld shows that we mixed up phi and theta! Let’s redefine cartesian->polar correctly.

(defn cartesian->spherical "Converts a map of Cartesian coordinates :x, :y, and :z to spherical coordinates :r, :theta, and :phi." [c] (let [r (Math/sqrt (+ (Math/pow (:x c) 2) (Math/pow (:y c) 2) (Math/pow (:z c) 2)))] {:r r :phi (Math/acos (/ (:z c) r)) :theta (Math/atan (/ (:y c) (:x c)))})) aphyr@waterhouse:~/scratch$ lein test lein test scratch.core-test lein test scratch.rocket-test Ran 2 tests containing 5 assertions. 0 failures, 0 errors.

Great. Now let’s check the rocket trajectory again.

user=> (-> (atlas-v) prepare (step 1) pprint) {:velocity {:x 0.45154055666826204, :y 463.8312116386399, :z -6.000769315822031E-16}, :position {:x 6378137, :y 463.8312116386399, :z 0}, :dry-mass 50050, :fuel-mass 71681400/253, :time 1, :isp 3050, :max-fuel-rate 284450/253, :max-thrust 4152000.0}

This time, our velocity is increasing in the +x direction, at half a meter per second. We have liftoff!

Flight

We have a function that can move the rocket forward by one small step of time, but we’d like to understand the rocket’s trajectory as a whole; to see all positions it will take. We’ll use iterate to construct a lazy, infinite sequence of rocket states, each one constructed by stepping forward from the last.

(defn trajectory [dt craft] "Returns all future states of the craft, at dt-second intervals." (iterate #(step % 1) craft)) user=> (->> (atlas-v) prepare (trajectory 1) (take 3) pprint) ({:velocity {:x 0, :y 463.8312116386399, :z 0}, :position {:x 6378137, :y 0, :z 0}, :dry-mass 50050, :fuel-mass 284450, :time 0, :isp 3050, :max-fuel-rate 284450/253, :max-thrust 4152000.0} {:velocity {:x 0.45154055666826204, :y 463.8312116386399, :z -6.000769315822031E-16}, :position {:x 6378137, :y 463.8312116386399, :z 0}, :dry-mass 50050, :fuel-mass 71681400/253, :time 1, :isp 3050, :max-fuel-rate 284450/253, :max-thrust 4152000.0} {:velocity {:x 0.9376544222659078, :y 463.83049896253056, :z -1.200153863164406E-15}, :position {:x 6378137.451540557, :y 927.6624232772798, :z -6.000769315822031E-16}, :dry-mass 50050, :fuel-mass 71396950/253, :time 2, :isp 3050, :max-fuel-rate 284450/253, :max-thrust 4152000.0})

Notice that each map is like a frame of a movie, playing at one frame per second. We can make the simulation more or less accurate by raising or lowering the framerate–adjusting the parameter fed to trajectory. For now, though, we’ll stick with one-second intervals.

How high above the surface is the rocket?

(defn altitude "The height above the surface of the equator, in meters." [craft] (-> craft :position cartesian->spherical :r (- earth-equatorial-radius)))

Now we can explore the rocket’s path as a series of altitudes over time:

user=> (->> (atlas-v) prepare (trajectory 1) (map altitude) (take 10) pprint) (0.0 0.016865378245711327 0.519002066925168 1.540983198210597 3.117615718394518 5.283942770212889 8.075246102176607 11.52704851794988 15.675116359256208 20.555462017655373)

The million dollar question, though, is whether the rocket breaks orbit.

(defn above-ground? "Is the craft at or above the surface?" [craft] (<= 0 (altitude craft))) (defn flight "The above-ground portion of a trajectory." [trajectory] (take-while above-ground? trajectory)) (defn crashed? "Does this trajectory crash into the surface before 100 hours are up?" [trajectory] (let [time-limit (* 100 3600)] ; 1 hour (not (every? above-ground? (take-while #(<= (:time %) time-limit) trajectory))))) (defn crash-time "Given a trajectory, returns the time the rocket impacted the ground." [trajectory] (:time (last (flight trajectory)))) (defn apoapsis "The highest altitude achieved during a trajectory." [trajectory] (apply max (map altitude trajectory))) (defn apoapsis-time "The time of apoapsis" [trajectory] (:time (apply max-key altitude (flight trajectory))))

If the rocket goes below ground, we know it crashed. If the rocket stays in orbit, the trajectory will never end. That makes it a bit tricky to tell whether the rocket is in a stable orbit or not, because we can’t ask about every element, or the last element, of an infinite sequence: it’ll take infinite time to evaluate. Instead, we’ll assume that the rocket should crash within the first, say, 100 hours; if it makes it past that point, we’ll assume it made orbit successfully. With these functions in hand, we’ll write a test in test/scratch/rocket_test.clj to see whether or not the launch is successful:

(deftest makes-orbit (let [trajectory (->> (atlas-v) prepare (trajectory 1))] (when (crashed? trajectory) (println "Crashed at" (crash-time trajectory) "seconds") (println "Maximum altitude" (apoapsis trajectory) "meters at" (apoapsis-time trajectory) "seconds")) ; Assert that the rocket eventually made it to orbit. (is (not (crashed? trajectory))))) aphyr@waterhouse:~/scratch$ lein test scratch.rocket-test lein test scratch.rocket-test Crashed at 982 seconds Maximum altitude 753838.039645385 meters at 532 seconds lein test :only scratch.rocket-test/makes-orbit FAIL in (makes-orbit) (rocket_test.clj:26) expected: (not (crashed? trajectory)) actual: (not (not true)) Ran 2 tests containing 3 assertions. 1 failures, 0 errors. Tests failed.

We made it to an altitude of 750 kilometers, and crashed 982 seconds after launch. We’re gonna need a bigger boat.

Stage II

The Atlas V isn’t big enough to make it into orbit on its own. It carries a second stage, the Centaur), which is much smaller and uses more efficient engines.

(defn centaur "The upper rocket stage. http://en.wikipedia.org/wiki/Centaur_(rocket_stage) http://www.astronautix.com/stages/cenaurde.htm" [] {:dry-mass 2361 :fuel-mass 13897 :isp 4354 :max-fuel-rate (/ 13897 470)})

The Centaur lives inside the Atlas V main stage. We’ll re-write atlas-v to take an argument: its next stage.

(defn atlas-v "The full launch vehicle. http://en.wikipedia.org/wiki/Atlas_V" [next-stage] {:dry-mass 50050 :fuel-mass 284450 :isp 3050 :max-fuel-rate (/ 284450 253) :next-stage next-stage})

Now, in our tests, we’ll construct the rocket like so:

(let [trajectory (->> (atlas-v (centaur)) prepare (trajectory 1))]

When we exhaust the fuel reserves of the primary stage, we’ll de-couple the main booster from the Centaur. In terms of our simulation, the Atlas V will be replaced by its next stage, the Centaur. We’ll write a function stage which separates the vehicles when ready:

(defn stage "When fuel reserves are exhausted, separate stages. Otherwise, return craft unchanged." [craft] (cond ; Still fuel left (pos? (:fuel-mass craft)) craft ; No remaining stages (nil? (:next-stage craft)) craft ; Stage! :else (merge (:next-stage craft) (select-keys craft [:time :position :velocity]))))

We’re using cond to handle three distinct cases: where there’s fuel remaining in the craft, where there is no stage to separate, and when we’re ready for stage separation. Separation is easy: we simply return the next stage of the current craft, with the current craft’s time, position, and velocity merged in.

Finally, we’ll have to update our step function to take into account the possibility of stage separation.

(defn step [craft dt] (let [craft (stage craft)] (assoc craft ; Time advances by dt seconds :time (+ dt (:time craft)) ; We burn some fuel :fuel-mass (- (:fuel-mass craft) (* dt (fuel-rate craft))) ; Our position changes based on our velocity :position (merge-with + (:position craft) (scale dt (:velocity craft))) ; And our velocity changes based on our acceleration :velocity (merge-with + (:velocity craft) (scale dt (acceleration craft))))))

Same as before, only now we call stage prior to the physics simulation. Let’s try a launch.

aphyr@waterhouse:~/scratch$ lein test scratch.rocket-test lein test scratch.rocket-test Crashed at 2415 seconds Maximum altitude 4598444.289945109 meters at 1446 seconds lein test :only scratch.rocket-test/makes-orbit FAIL in (makes-orbit) (rocket_test.clj:27) expected: (not (crashed? trajectory)) actual: (not (not true)) Ran 2 tests containing 3 assertions. 1 failures, 0 errors. Tests failed.

Still crashed–but we increased our apoapsis from 750 kilometers to 4,598 kilometers. That’s plenty high, but we’re still not making orbit. Why? Because we’re going straight up, then straight back down. To orbit, we need to move sideways, around the earth.

Orbital insertion

Our spacecraft is shooting upwards, but in order to remain in orbit around the earth, it has to execute a second burn: an orbital injection maneuver. That injection maneuver is also called a circularization burn because it turns the orbit from an ascending parabola into a circle (or something roughly like it). We don’t need to be precise about circularization–any trajectory that doesn’t hit the planet will suffice. All we have to do is burn towards the horizon, once we get high enough.

To do that, we’ll need to enhance the rocket’s control software. We assumed that the rocket would always thrust in the +x direction; but now we’ll need to thrust in multiple directions. We’ll break up the engine force into two parts: thrust (how hard the rocket motor pushes) and orientation (which determines the direction the rocket is pointing.)

(defn unit-vector "Scales coordinates to magnitude 1." [coordinates] (scale (/ (magnitude coordinates)) coordinates)) (defn engine-force "The force vector, each component in Newtons, due to the rocket engine." [craft] (scale (thrust craft) (unit-vector (orientation craft))))

We’re taking the orientation of the craft–some coordinates–and scaling it to be of length one with unit-vector. Then we’re scaling the orientation vector by the thrust, returning a thrust vector.

As we go back and redefine parts of the program, you might see an error like

Exception in thread "main" java.lang.RuntimeException: Unable to resolve symbol: unit-vector in this context, compiling:(scratch/rocket.clj:69:11) at clojure.lang.Compiler.analyze(Compiler.java:6380) at clojure.lang.Compiler.analyze(Compiler.java:6322)

This is a stack trace from the Clojure compiler. It indicates that in scratch/rocket.clj, on line 69, column 11, we used the symbol unit-vector–but it didn’t have a meaning at that point in the program. Perhaps unit-vector is defined below that line. There are two ways to solve this.

1. Organize your functions so that the simple ones come first, and those that depend on them come later. Read this way, namespaces tell a story, progressing from smaller to bigger, more complex problems.

2. Sometimes, ordering functions this way is impossible, or would put related ideas too far apart. In this case you can (declare unit-vector) near the top of the namespace. This tells Clojure that unit-vector isn’t defined yet, but it’ll come later.

Now that we’ve broken up engine-force into thrust and orientation, we have to control the thrust properly for our two burns. We’ll start by defining the times for the initial ascent and circularization burn, expressed as vectors of start and end times, in seconds.

(def ascent "The start and end times for the ascent burn." [0 3000]) (def circularization "The start and end times for the circularization burn." [4000 1000])

Now we’ll change the thrust by adjusting the rate of fuel consumption. Instead of burning at maximum until running out of fuel, we’ll execute two distinct burns.

(defn fuel-rate "How fast is fuel, in kilograms/second, consumed by the craft?" [craft] (cond ; Out of fuel (<= (:fuel-mass craft) 0) 0 ; Ascent burn (<= (first ascent) (:time craft) (last ascent)) (:max-fuel-rate craft) ; Circularization burn (<= (first circularization) (:time craft) (last circularization)) (:max-fuel-rate craft) ; Shut down engines otherwise :else 0))

We’re using cond to express four distinct possibilities: that we’ve run out of fuel, executing either of the two burns, or resting with the engines shut down. Because the comparison function <= takes any number of arguments and asserts that they occur in order, expressing intervals like “the time is between the first and last times in the ascent” is easy.

Finally, we need to determine the direction to burn in. This one’s gonna require some tricky linear algebra. You don’t need to worry about the specifics here–the goal is to find out what direction the rocket should burn to fly towards the horizon, in a circle around the planet. We’re doing that by taking the rocket’s velocity vector, and flattening out the velocity towards or away from the planet. All that’s left is the direction the rocket is flying around the earth.

(defn dot-product "Finds the inner product of two x, y, z coordinate maps. See http://en.wikipedia.org/wiki/Dot_product." [c1 c2] (+ (* (:x c1) (:x c2)) (* (:y c1) (:y c2)) (* (:z c1) (:z c2)))) (defn projection "The component of coordinate map a in the direction of coordinate map b. See http://en.wikipedia.org/wiki/Vector_projection." [a b] (let [b (unit-vector b)] (scale (dot-product a b) b))) (defn rejection "The component of coordinate map a *not* in the direction of coordinate map b." [a b] (let [a' (projection a b)] {:x (- (:x a) (:x a')) :y (- (:y a) (:y a')) :z (- (:z a) (:z a'))}))

With the mathematical underpinnings ready, we’ll define the orientation control software:

(defn orientation "What direction is the craft pointing?" [craft] (cond ; Initially, point along the *position* vector of the craft--that is ; to say, straight up, away from the earth. (<= (first ascent) (:time craft) (last ascent)) (:position craft) ; During the circularization burn, we want to burn *sideways*, in the ; direction of the orbit. We'll find the component of our velocity ; which is aligned with our position vector (that is to say, the vertical ; velocity), and subtract the vertical component. All that's left is the ; *horizontal* part of our velocity. (<= (first circularization) (:time craft) (last circularization)) (rejection (:velocity craft) (:position craft)) ; Otherwise, just point straight ahead. :else (:velocity craft)))

For the ascent burn, we’ll push straight away from the planet. For circularization, we use the rejection function to find the part of the velocity around the planet, and thrust in that direction. By default, we’ll leave the rocket pointing in the direction of travel.

With these changes made, the rocket should execute two burns. Let’s re-run the tests and see.

aphyr@waterhouse:~/scratch$ lein test scratch.rocket-test lein test scratch.rocket-test Ran 2 tests containing 3 assertions. 0 failures, 0 errors.

We finally did it! We’re rocket scientists!

Review

(ns scratch.rocket) ;; Linear algebra for {:x 1 :y 2 :z 3} coordinate vectors. (defn map-values "Applies f to every value in the map m." [f m] (into {} (map (fn [pair] [(key pair) (f (val pair))]) m))) (defn magnitude "What's the radius of a given set of cartesian coordinates?" [c] ; By the Pythagorean theorem... (Math/sqrt (+ (Math/pow (:x c) 2) (Math/pow (:y c) 2) (Math/pow (:z c) 2)))) (defn scale "Multiplies a map of x, y, and z coordinates by the given factor." [factor coordinates] (map-values (partial * factor) coordinates)) (defn unit-vector "Scales coordinates to magnitude 1." [coordinates] (scale (/ (magnitude coordinates)) coordinates)) (defn dot-product "Finds the inner product of two x, y, z coordinate maps. See http://en.wikipedia.org/wiki/Dot_product" [c1 c2] (+ (* (:x c1) (:x c2)) (* (:y c1) (:y c2)) (* (:z c1) (:z c2)))) (defn projection "The component of coordinate map a in the direction of coordinate map b. See http://en.wikipedia.org/wiki/Vector_projection." [a b] (let [b (unit-vector b)] (scale (dot-product a b) b))) (defn rejection "The component of coordinate map a *not* in the direction of coordinate map b." [a b] (let [a' (projection a b)] {:x (- (:x a) (:x a')) :y (- (:y a) (:y a')) :z (- (:z a) (:z a'))})) ;; Coordinate conversion (defn cartesian->spherical "Converts a map of Cartesian coordinates :x, :y, and :z to spherical coordinates :r, :theta, and :phi." [c] (let [r (magnitude c)] {:r r :phi (Math/acos (/ (:z c) r)) :theta (Math/atan (/ (:y c) (:x c)))})) (defn spherical->cartesian "Converts spherical to Cartesian coordinates." [c] {:x (* (:r c) (Math/cos (:theta c)) (Math/sin (:phi c))) :y (* (:r c) (Math/sin (:theta c)) (Math/sin (:phi c))) :z (* (:r c) (Math/cos (:phi c)))}) ;; The earth (def earth-equatorial-radius "Radius of the earth, in meters" 6378137) (def earth-day "Length of an earth day, in seconds." 86400) (def earth-equatorial-speed "How fast points on the equator move, relative to the center of the earth, in meters/sec." (/ (* 2 Math/PI earth-equatorial-radius) earth-day)) (def g "Acceleration of gravity in meters/s^2" -9.8) (def initial-space-center "The initial position and velocity of the launch facility" {:time 0 :position {:x earth-equatorial-radius :y 0 :z 0} :velocity {:x 0 :y earth-equatorial-speed :z 0}}) ;; Craft (defn centaur "The upper rocket stage. http://en.wikipedia.org/wiki/Centaur_(rocket_stage) http://www.astronautix.com/stages/cenaurde.htm" [] {:dry-mass 2361 :fuel-mass 13897 :isp 4354 :max-fuel-rate (/ 13897 470)}) (defn atlas-v "The full launch vehicle. http://en.wikipedia.org/wiki/Atlas_V" [next-stage] {:dry-mass 50050 :fuel-mass 284450 :isp 3050 :max-fuel-rate (/ 284450 253) :next-stage next-stage}) ;; Flight control (def ascent "The start and end times for the ascent burn." [0 300]) (def circularization "The start and end times for the circularization burn." [400 1000]) (defn orientation "What direction is the craft pointing?" [craft] (cond ; Initially, point along the *position* vector of the craft--that is ; to say, straight up, away from the earth. (<= (first ascent) (:time craft) (last ascent)) (:position craft) ; During the circularization burn, we want to burn *sideways*, in the ; direction of the orbit. We'll find the component of our velocity ; which is aligned with our position vector (that is to say, the vertical ; velocity), and subtract the vertical component. All that's left is the ; *horizontal* part of our velocity. (<= (first circularization) (:time craft) (last circularization)) (rejection (:velocity craft) (:position craft)) ; Otherwise, just point straight ahead. :else (:velocity craft))) (defn fuel-rate "How fast is fuel, in kilograms/second, consumed by the craft?" [craft] (cond ; Out of fuel (<= (:fuel-mass craft) 0) 0 ; Ascent burn (<= (first ascent) (:time craft) (last ascent)) (:max-fuel-rate craft) ; Circularization burn (<= (first circularization) (:time craft) (last circularization)) (:max-fuel-rate craft) ; Shut down engines otherwise :else 0)) (defn stage "When fuel reserves are exhausted, separate stages. Otherwise, return craft unchanged." [craft] (cond ; Still fuel left (pos? (:fuel-mass craft)) craft ; No remaining stages (nil? (:next-stage craft)) craft ; Stage! :else (merge (:next-stage craft) (select-keys craft [:time :position :velocity])))) ;; Dynamics (defn thrust "How much force, in newtons, does the craft's rocket engines exert?" [craft] (* (fuel-rate craft) (:isp craft))) (defn mass "The total mass of a craft." [craft] (+ (:dry-mass craft) (:fuel-mass craft))) (defn gravity-force "The force vector, each component in Newtons, due to gravity." [craft] ; Since force is mass times acceleration... (let [total-force (* g (mass craft))] (-> craft ; Now we'll take the craft's position :position ; in spherical coordinates, cartesian->spherical ; replace the radius with the gravitational force... (assoc :r total-force) ; and transform back to Cartesian-land spherical->cartesian))) (declare altitude) (defn engine-force "The force vector, each component in Newtons, due to the rocket engine." [craft] ; Debugging; useful for working through trajectories in detail. ; (println craft) ; (println "t " (:time craft) "alt" (altitude craft) "thrust" (thrust craft)) ; (println "fuel" (:fuel-mass craft)) ; (println "vel " (:velocity craft)) ; (println "ori " (unit-vector (orientation craft))) (scale (thrust craft) (unit-vector (orientation craft)))) (defn total-force "Total force on a craft." [craft] (merge-with + (engine-force craft) (gravity-force craft))) (defn acceleration "Total acceleration of a craft." [craft] (let [m (mass craft)] (scale (/ m) (total-force craft)))) (defn step [craft dt] (let [craft (stage craft)] (assoc craft ; Time advances by dt seconds :time (+ dt (:time craft)) ; We burn some fuel :fuel-mass (- (:fuel-mass craft) (* dt (fuel-rate craft))) ; Our position changes based on our velocity :position (merge-with + (:position craft) (scale dt (:velocity craft))) ; And our velocity changes based on our acceleration :velocity (merge-with + (:velocity craft) (scale dt (acceleration craft)))))) ;; Launch and flight (defn prepare "Prepares a craft for launch from an equatorial space center." [craft] (merge craft initial-space-center)) (defn trajectory [dt craft] "Returns all future states of the craft, at dt-second intervals." (iterate #(step % 1) craft)) ;; Analyzing trajectories (defn altitude "The height above the surface of the equator, in meters." [craft] (-> craft :position cartesian->spherical :r (- earth-equatorial-radius))) (defn above-ground? "Is the craft at or above the surface?" [craft] (<= 0 (altitude craft))) (defn flight "The above-ground portion of a trajectory." [trajectory] (take-while above-ground? trajectory)) (defn crashed? "Does this trajectory crash into the surface before 10 hours are up?" [trajectory] (let [time-limit (* 10 3600)] ; 10 hours (not (every? above-ground? (take-while #(<= (:time %) time-limit) trajectory))))) (defn crash-time "Given a trajectory, returns the time the rocket impacted the ground." [trajectory] (:time (last (flight trajectory)))) (defn apoapsis "The highest altitude achieved during a trajectory." [trajectory] (apply max (map altitude (flight trajectory)))) (defn apoapsis-time "The time of apoapsis" [trajectory] (:time (apply max-key altitude (flight trajectory))))

As written here, our first non-trivial program tells a story–though a different one than the process of exploration and refinement that brought the rocket to orbit. It builds from small, abstract ideas: linear algebra and coordinates; physical constants describing the universe for the simulation; and the basic outline of the spacecraft. Then we define the software controlling the rocket; the times for the burns, how much to thrust, in what direction, and when to separate stages. Using those control functions, we build a physics engine including gravity and thrust forces, and use Newton’s second law to build a basic Euler Method solver. Finally, we analyze the trajectories the solver produces to answer key questions: how high, how long, and did it explode?

We used Clojure’s immutable data structures–mostly maps–to represent the state of the universe, and defined pure functions to interpret those states and construct new ones. Using iterate, we projected a single state forward into an infinite timeline of the future–evaluated as demanded by the analysis functions. Though we pay a performance penalty, immutable data structures, pure functions, and lazy evaluation make simulating complex systems easier to reason about.

Had we written this simulation in a different language, different techniques might have come into play. In Java, C++, or Ruby, we would have defined a hierarchy of datatypes called classes, each one representing a small piece of state. We might define a Craft type, and created subtypes Atlas and Centaur. We’d create a Coordinate type, subdivided into Cartesian and Spherical, and so on. The types add complexity and rigidity, but also prevent mis-spellings, and can prevent us from interpreting, say, coordinates as craft or vice-versa.

To move the system forward in a language emphasizing mutable data structures, we would have updated the time and coordinates of a single craft in-place. This introduces additional complexity, because many of the changes we made depended on the current values of the craft. To ensure the correct ordering of calculations, we’d scatter temporary variables and explicit copies throughout the code, ensuring that functions didn’t see inconsistent pictures of the craft state. The mutable approach would likely be faster, but would still demand some copying of data, and sacrifice clarity.

More imperative languages place less emphasis on laziness, and make it harder to express ideas like map and take. We might have simulated the trajectory for some fixed time, constructing a history of all the intermediate results we needed, then analyzed it by moving explicitly from slot to slot in that history, checking if the craft had crashed, and so on.

Across all these languages, though, some ideas remain the same. We solve big problems by breaking them up into smaller ones. We use data structures to represent the state of the system, and functions to alter that state. Comments and docstrings clarify the story of the code, making it readable to others. Tests ensure the software is correct, and allow us to work piecewise towards a solution.

Exercises

1. We know the spacecraft reached orbit, but we have no idea what that orbit looks like. Since the trajectory is infinite in length, we can’t ask about the entire history using max–but we know that all orbits have a high and low point. At the highest point, the difference between successive altitudes changes from increasing to decreasing, and at the lowest point, the difference between successive altitudes changes from decreasing to increasing. Using this technique, refine the apoapsis function to find the highest point using that inflection in altitudes–and write a corresponding periapsis function that finds the lowest point in the orbit. Display both periapsis and apoapsis in the test suite.

2. We assumed the force of gravity resulted in a constant 9.8 meter/second/second acceleration towards the earth, but in the real world, gravity falls off with the inverse square law. Using the mass of the earth, mass of the spacecraft, and Newton’s constant, refine the gravitational force used in this simulation to take Newton’s law into account. How does this affect the apoapsis?

3. We ignored the atmosphere, which exerts drag on the craft as it moves through the air. Write a basic air-density function which falls off with altitude. Make some educated guesses as to how much drag a real rocket experiences, and assume that the drag force is proportional to the square of the rocket’s velocity. Can your rocket still reach orbit?

4. Notice that the periapsis and apoapsis of the rocket are different. By executing the circularization burn carefully, can you make them the same–achieving a perfectly circular orbit? One way to do this is to pick an orbital altitude and velocity of a known satellite–say, the International Space Station–and write the control software to match that velocity at that altitude.

Previously, we covered state and mutability.

Up until now, we’ve been programming primarily at the REPL. However, the REPL is a limited tool. While it lets us explore a problem interactively, that interactivity comes at a cost: changing an expression requires retyping the entire thing, editing multi-line expressions is awkward, and our work vanishes when we restart the REPL–so we can’t share our programs with others, or run them again later. Moreover, programs in the REPL are hard to organize. To solve large problems, we need a way of writing programs durably–so they can be read and evaluated later.

In addition to the code itself, we often want to store ancillary information. Tests verify the correctness of the program. Resources like precomputed databases, lookup tables, images, and text files provide other data the program needs to run. There may be documentation: instructions for how to use and understand the software. A program may also depend on code from other programs, which we call libraries, packages, or dependencies. In Clojure, we have a standardized way to bind together all these parts into a single directory, called a project.

Project structure

We created a project at the start of this book by using Leiningen, the Clojure project tool.

$ lein new scratch

scratch is the name of the project, and also the name of the directory where the project’s files live. Inside the project are a few files.

$ cd scratch; ls doc project.clj README.md resources src target test

project.clj defines the project: its name, its version, dependencies, and so on. Notice the name of the project (scratch) comes first, followed by the version (0.1.0-SNAPSHOT). -SNAPSHOT versions are for development; you can change them at any time, and any projects which depend on the snapshot will pick up the most recent changes. A version which does not end in -SNAPSHOT is fixed: once published, it always points to the same version of the project. This allows projects to specify precisely which projects they depend on. For example, scratch’s project.clj says scratch depends on org.clojure/clojure version 1.5.1.

(defproject scratch "0.1.0-SNAPSHOT" :description "FIXME: write description" :url "http://example.com/FIXME" :license {:name "Eclipse Public License" :url "http://www.eclipse.org/legal/epl-v10.html"} :dependencies [[org.clojure/clojure "1.5.1"] ])

README.md is the first file most people open when they look at a new project, and Lein generates a generic readme for you to fill in later. We call this kind of scaffolding or example a “stub”; it’s just there to remind you what sort of things to write yourself. You’ll notice the readme includes the name of the project, some notes on what it does and how to use it, a copyright notice where your name should go, and a license, which sets the legal terms for the use of the project. By default, Leiningen suggests the Eclipse Public License, which allows everyone to use and modify the software, so long as they preserve the license information.

The doc directory is for documentation; sometimes hand-written, sometimes automatically generated from the source code. resources is for additional files, like images. src is where Clojure code lives, and test contains the corresponding tests. Finally, target is where Leiningen stores compiled code, built packages, and so on.

Namespaces

Every lein project starts out with a stub namespace containing a simple function. Let’s take a look at that namespace now–it lives in src/scratch/core.clj:

(ns scratch.core) (defn foo "I don't do a whole lot." [x] (println x "Hello, World!"))

The first part of this file defines the namespace we’ll be working in. The ns macro lets the Clojure compiler know that all following code belongs in the scratch.core namespace. Remember, scratch is the name of our project. scratch.core is for the core functions and definitions of the scratch project. As projects expand, we might add new namespaces to separate our work into smaller, more understandable pieces. For instance, Clojure’s primary functions live in clojure.core, but there are auxiliary functions for string processing in clojure.string, functions for interoperating with Java’s input-output system in clojure.java.io, for printing values in clojure.pprint, and so on.

def, defn, and peers always work in the scope of a particular namespace. The function foo in scratch.core is different from the function foo in scratch.pad.

scratch.foo=> (ns scratch.core) nil scratch.core=> (def foo "I'm in core") #'scratch.core/foo scratch.core=> (ns scratch.pad) nil scratch.pad=> (def foo "I'm in pad!") #'scratch.pad/foo

Notice the full names of these vars are different: scratch.core/foo vs scratch.pad/foo. You can always refer to a var by its fully qualified name: the namespace, followed by a slash /, followed by the short name.

Inside a namespace, symbols resolve to variables which are defined in that namespace. So in scratch.pad, foo refers to scratch.pad/foo.

scratch.pad=> foo "I'm in pad!"

Namespaces automatically include clojure.core by default; which is where all the standard functions, macros, and special forms come from. let, defn, filter, vector, etc: all live in clojure.core, but are automatically included in new namespaces so we can refer to them by their short names.

Notice that the values for foo we defined in scratch.pad and scratch.core aren’t available in other namespaces, like user.

scratch.pad=> (ns user) nil user=> foo CompilerException java.lang.RuntimeException: Unable to resolve symbol: foo in this context, compiling:(NO_SOURCE_PATH:1:602)

To access things from other namespaces, we have to require them in the namespace definition.

user=> (ns user (:require [scratch.core])) nil user=> scratch.core/foo "I'm in core"

The :require part of the ns declaration told the compiler that the user namespace needed access to scratch.core. We could then refer to the fully qualified name scratch.core/foo.

Often, writing out the full namespace is cumbersome–so you can give a short alias for a namespace like so:

user=> (ns user (:require [scratch.core :as c])) nil user=> c/foo "I'm in core"

The :as directive indicates that anywhere we write c/something, the compiler should expand that to scratch.core/something. If you plan on using a var from another namespace often, you can refer it to the local namespace–which means you may omit the namespace qualifier entirely.

user=> (ns user (:require [scratch.core :refer [foo]])) nil user=> foo "I'm in core"

You can refer functions into the current namespace by listing them: [foo bar ...]. Alternatively, you can suck in every function from another namespace by saying :refer :all:

user=> (ns user (:require [scratch.core :refer :all])) nil user=> foo "I'm in core"

Namespaces control complexity by isolating code into more understandable, related pieces. They make it easier to read code by keeping similar things together, and unrelated things apart. By making dependencies between namespaces explicit, they make it clear how groups of functions relate to one another.

If you’ve worked with Erlang, Modula-2, Haskell, Perl, or ML, you’ll find namespaces analogous to modules or packages. Namespaces are often large, encompassing hundreds of functions; and most projects use only a handful of namespaces.

By contrast, object-oriented programming languages like Java, Scala, Ruby, and Objective C organize code in classes, which combine names and state in a single construct. Because all functions in a class operate on the same state, object-oriented languages tend to have many classes with fewer functions in each. It’s not uncommon for a typical Java project to define hundreds or thousands of classes containing only one or two functions each. If you come from an object-oriented language, it can feel a bit unusual to combine so many functions in a single scope–but because functional programs isolate state differently, this is normal. If, on the other hand, you move to an object-oriented language after Clojure, remember that OO languages compose differently. Objects with hundreds of functions are usually considered unwieldy and should be split into smaller pieces.

Code and tests

It’s perfectly fine to test small programs in the REPL. We’ve written and refined hundreds of functions that way: by calling the function and seeing what happens. However, as programs grow in scope and complexity, testing them by hand becomes harder and harder. If you change the behavior of a function which ten other functions rely on, you may have to re-test all ten by hand. In real programs, a small change can alter thousands of distinct behaviors, all of which should be verified.

Wherever possible, we want to automate software tests–making the test itself another program. If the test suite runs in a matter of seconds, we can make changes freely–re-running the tests continuously to verify that everything still works.

As a simple example, let’s write and test a single function in src/scratch/core.clj. How about exponentiation–raising a number to the given power?

(ns scratch.core) (defn pow "Raises base to the given power. For instance, (pow 3 2) returns three squared, or nine." [base power] (apply * (repeat base power)))

So we repeat the base power times, then call * with that sequence of bases to multiply them all together. Seems straightforward enough. Now we need to test it.

By default, all lein projects come with a simple test stub. Let’s see it in action by running lein test.

aphyr@waterhouse:~/scratch$ lein test lein test scratch.core-test lein test :only scratch.core-test/a-test FAIL in (a-test) (core_test.clj:7) FIXME, I fail. expected: (= 0 1) actual: (not (= 0 1)) Ran 1 tests containing 1 assertions. 1 failures, 0 errors. Tests failed.

A failure is when a test returns the wrong value. An error is when a test throws an exception. In this case, the test named a-test, in the file core_test.clj, on line 7, failed. That test expected zero to be equal to one–but found that 0 and 1 were (in point of fact) not equal. Let’s take a look at that test, in test/scratch/core_test.clj.

(ns scratch.core-test (:require [clojure.test :refer :all] [scratch.core :refer :all])) (deftest a-test (testing "FIXME, I fail." (is (= 0 1))))

These tests live in a namespace too! Notice that namespaces and file names match up: scratch.core lives in src/scratch/core.clj, and scratch.core-test lives in test/scratch/core_test.clj. Dashes (-) in namespaces correspond to underscores (_) in filenames, and dots (.) correspond to directory separators (/).

The scratch.core-test namespace is responsible for testing things in scratch.core. Notice that it requires two namespaces: clojure.test, which provides testing functions and macros, and scratch.core, which is the namespace we want to test.

Then we define a test using deftest. deftest takes a symbol as a test name, and then any number of expressions to evaluate. We can use testing to split up tests into smaller pieces. If a test fails, lein test will print out the enclosing deftest and testing names, to make it easier to figure out what went wrong.

Let’s change this test so that it passes. 0 should equal 0.

(deftest a-test (testing "Numbers are equal to themselves, right?" (is (= 0 0)))) aphyr@waterhouse:~/scratch$ lein test lein test scratch.core-test Ran 1 tests containing 1 assertions. 0 failures, 0 errors.

Wonderful! Now let’s test the pow function. I like to start with a really basic case and work my way up to more complicated ones. 1¹ is 1, so:

(deftest pow-test (testing "unity" (is (= 1 (pow 1 1))))) aphyr@waterhouse:~/scratch$ lein test lein test scratch.core-test Ran 1 tests containing 1 assertions. 0 failures, 0 errors.

Excellent. How about something harder?

(deftest pow-test (testing "unity" (is (= 1 (pow 1 1)))) (testing "square integers" (is (= 9 (pow 3 2))))) aphyr@waterhouse:~/scratch$ lein test lein test scratch.core-test lein test :only scratch.core-test/pow-test FAIL in (pow-test) (core_test.clj:10) square integers expected: (= 9 (pow 3 2)) actual: (not (= 9 8)) Ran 1 tests containing 2 assertions. 1 failures, 0 errors. Tests failed.

That’s odd. 3² should be 9, not 8. Let’s double-check our code in the REPL. base was 3, and power was 2, so…

user=> (repeat 3 2) (2 2 2) user=> (* 2 2 2) 8

Ah, there’s the problem. We’re mis-using repeat. Instead of repeating 3 twice, we repeated 2 thrice.

user=> (doc repeat) ------------------------- clojure.core/repeat ([x] [n x]) Returns a lazy (infinite!, or length n if supplied) sequence of xs.

Let’s redefine pow with the correct arguments to repeat:

(defn pow "Raises base to the given power. For instance, (pow 3 2) returns three squared, or nine." [base power] (apply * (repeat power base)))

How about 0^0? By convention, mathematicians define 0⁰ as 1.

(deftest pow-test (testing "unity" (is (= 1 (pow 1 1)))) (testing "square integers" (is (= 9 (pow 3 2)))) (testing "0^0" (is (= 1 (pow 0 0))))) aphyr@waterhouse:~/scratch$ lein test lein test scratch.core-test Ran 1 tests containing 3 assertions. 0 failures, 0 errors.

Hey, what do you know? It works! But why?

user=> (repeat 0 0) ()

What happens when we call * with an empty list of arguments?

user=> (*) 1

Remember when we talked about how the zero-argument forms of +, and * made some definitions simpler? This is one of those times. We didn’t have to define a special exception for zero powers because (*) returns the multiplicative identity 1, by convention.

Exploring data

The last bit of logistics we need to talk about is working with other people’s code. Clojure projects, like most modern programming environments, are built to work together. We can use libraries to parse data, solve mathematical problems, render graphics, perform simulations, talk to robots, or predict the weather. As a quick example, I’d like to imagine that you and I are public-health researchers trying to identify the best location for an ad campaign to reduce drunk driving.

The FBI’s Uniform Crime Reporting database tracks the annual tally of different types of arrests, broken down by county–but the data files provided by the FBI are a mess to work with. Helpfully, Matt Aliabadi has helpfully organized the UCR’s somewhat complex format into nice, normalized files in a data format called JSON, and made them available on Github. Let’s download the most recent year’s normalized data, and save it in the scratch directory.

What’s in this file, anyway? Let’s take a look at the first few lines using head:

aphyr@waterhouse:~/scratch$ head 2008.json [ { "icpsr_study_number": null, "icpsr_edition_number": 1, "icpsr_part_number": 1, "icpsr_sequential_case_id_number": 1, "fips_state_code": "01", "fips_county_code": "001", "county_population": 52417, "number_of_agencies_in_county": 3,

This is a data format called JSON, and it looks a lot like Clojure’s data structures. That’s the start of a vector on the first line, and the second line starts a map. Then we’ve got string keys like "icpsr_study_number", and values which look like null (nil), numbers, or strings. But in order to work with this file, we’ll need to parse it into Clojure data structures. For that, we can use a JSON parsing library, like Cheshire.

Cheshire, like most Clojure libraries, is published on an internet repository called Clojars. To include it in our scratch project, all we have to do is add open project.clj in a text editor, and add a line specifying that we want to use a particular version of Cheshire.

(defproject scratch "0.1.0-SNAPSHOT" :description "Just playing around" :url "http://example.com/FIXME" :license {:name "Eclipse Public License" :url "http://www.eclipse.org/legal/epl-v10.html"} :dependencies [[org.clojure/clojure "1.5.1"] [cheshire "5.3.1"]])

Now we’ll exit the REPL with Control+D (^D), and restart it with lein repl. Leiningen, the Clojure package manager, will automatically download Cheshire from Clojars and make it available in the new REPL session.

Now let’s figure out how to parse the JSON file. Looking at Cheshire’s README shows an example that looks helpful:

;; parse some json and get keywords back (parse-string "{\"foo\":\"bar\"}" true) ;; => {:foo "bar"}

So Cheshire includes a parse-string function which can take a string and return a data structure. How can we get a string out of a file? Using slurp:

user=> (use 'cheshire.core) nil user=> (parse-string (slurp "2008.json")) ...

Woooow, that’s a lot of data! Let’s chop it down to something more manageable. How about the first entry?

user=> (first (parse-string (slurp "2008.json"))) {"syntheticdrug_salemanufacture" 1, "all_other_offenses_except_traffic" 900, "arson" 3, ...} user=> (-> "2008.json" slurp parse-string first)

It’d be nicer if this data used keywords instead of strings for its keys. Let’s use the second argument to Chesire’s parse-string to convert all the keys in maps to keywords.

user=> (first (parse-string (slurp "2008.json") true)) {:other_assaults 288, :gambling_all_other 0, :arson 3, ... :drunkenness 108}

Since we’re going to be working with this dataset over and over again, let’s bind it to a variable for easy re-use.

user=> (def data (parse-string (slurp "2008.json") true)) #'user/data

Now we’ve got a big long vector of counties, each represented by a map–but we’re just interested in the DUIs of each one. What does that look like? Let’s map each county to its :driving_under_influence.

user=> (->> data (map :driving_under_influence)) (198 1095 114 98 135 4 122 587 204 53 177 ...

What’s the most any county has ever reported?

user=> (->> data (map :driving_under_influence) (apply max)) 45056

45056 counts in one year? Wow! What about the second-worst county? The easiest way to find the top n counties is to sort the list, then look at the final elements.

user=> (->> data (map :driving_under_influence) sort (take-last 10)) (8589 10432 10443 10814 11439 13983 17572 18562 26235 45056)

So the top 10 counties range from 8549 counts to 45056 counts. What’s the most common count? Clojure comes with a built-in function called frequencies which takes a sequence of elements, and returns a map from each element to how many times it appeared in the sequence.

user=> (->> data (map :driving_under_influence) frequencies) {0 227, 1024 1, 45056 1, 32 15, 2080 1, 64 12 ...

Now let’s take those [drunk-driving, frequency] pairs and sort them by key to produce a histogram. sort-by takes a function to apply to each element in the collection–in this case, a key-value pair–and returns something that can be sorted, like a number. We’ll choose the key function to extract the key from each key-value pair, effectively sorting the counties by number of reported incidents.

user=> (->> data (map :driving_under_influence) frequencies (sort-by key) pprint) ([0 227] [1 24] [2 17] [3 20] [4 17] [5 24] [6 23] [7 23] [8 17] [9 19] [10 29] [11 20] [12 18] [13 21] [14 25] [15 13] [16 18] [17 16] [18 17] [19 11] [20 8] ...

So a ton of counties (227 out of 3172 total) report no drunk driving; a few hundred have one incident, a moderate number have 10-20, and it falls off from there. This is a common sort of shape in statistics; often a hallmark of an exponential distribution.

How about the 10 worst counties, all the way out on the end of the curve?

user=> (->> data (map :driving_under_influence) frequencies (sort-by key) (take-last 10) pprint) ([8589 1] [10432 1] [10443 1] [10814 1] [11439 1] [13983 1] [17572 1] [18562 1] [26235 1] [45056 1])

So it looks like 45056 is high, but there are 8 other counties with tens of thousands of reports too. Let’s back up to the original dataset, and sort it by DUIs:

user=> (->> data (sort-by :driving_under_influence) (take-last 10) pprint) ({:other_assaults 3096, :gambling_all_other 3, :arson 106, :have_stolen_property 698, :syntheticdrug_salemanufacture 0, :icpsr_sequential_case_id_number 220, :drug_abuse_salemanufacture 1761, ...

What we’re looking for is the county names, but it’s a little hard to read these enormous maps. Let’s take a look at just the keys that define each county, and see which ones might be useful. We’ll take this list of counties, map each one to a list of its keys, and concatenate those lists together into one big long list. mapcat maps and concatenates in a single step. We expect the same keys to show up over and over again, so we’ll remove duplicates by merging all those keys into a sorted-set.

user=> (->> data (sort-by :driving_under_influence) (take-last 10) (mapcat keys) (into (sorted-set)) pprint) #{:aggravated_assaults :all_other_offenses_except_traffic :arson :auto_thefts :bookmaking_horsesport :burglary :county_population :coverage_indicator :curfew_loitering_laws :disorderly_conduct :driving_under_influence :drug_abuse_salemanufacture :drug_abuse_violationstotal :drug_possession_other :drug_possession_subtotal :drunkenness :embezzlement :fips_county_code :fips_state_code :forgerycounterfeiting :fraud :gambling_all_other :gambling_total :grand_total :have_stolen_property :icpsr_edition_number :icpsr_part_number :icpsr_sequential_case_id_number :icpsr_study_number :larceny :liquor_law_violations :marijuana_possession :marijuanasalemanufacture :multicounty_jurisdiction_flag :murder :number_of_agencies_in_county :numbers_lottery :offenses_against_family_child :opiumcocaine_possession :opiumcocainesalemanufacture :other_assaults :otherdang_nonnarcotics :part_1_total :property_crimes :prostitutioncomm_vice :rape :robbery :runaways :sex_offenses :suspicion :synthetic_narcoticspossession :syntheticdrug_salemanufacture :vagrancy :vandalism :violent_crimes :weapons_violations}

Ah, :fips_county_code and :fips_state_code look promising. Let’s compact the dataset to just drunk driving and those codes, using select-keys.

user=> (->> data (sort-by :driving_under_influence) (take-last 10) (map #(select-keys % [:driving_under_influence :fips_county_code :fips_state_code])) pprint) ({:fips_state_code "06", :fips_county_code "067", :driving_under_influence 8589} {:fips_state_code "48", :fips_county_code "201", :driving_under_influence 10432} {:fips_state_code "32", :fips_county_code "003", :driving_under_influence 10443} {:fips_state_code "06", :fips_county_code "065", :driving_under_influence 10814} {:fips_state_code "53", :fips_county_code "033", :driving_under_influence 11439} {:fips_state_code "06", :fips_county_code "071", :driving_under_influence 13983} {:fips_state_code "06", :fips_county_code "059", :driving_under_influence 17572} {:fips_state_code "06", :fips_county_code "073", :driving_under_influence 18562} {:fips_state_code "04", :fips_county_code "013", :driving_under_influence 26235} {:fips_state_code "06", :fips_county_code "037", :driving_under_influence 45056})

Now we’re getting somewhere–but we need a way to interpret these state and county codes. Googling for “FIPS” led me to Wikipedia’s account of the FIPS county code system, and the NOAA’s ERDDAP service, which has a table mapping FIPS codes to state and county names. Let’s save that file as fips.json.

Now we’ll slurp that file into the REPL and parse it, just like we did with the crime dataset.

user=> (def fips (parse-string (slurp "fips.json") true))

Let’s take a quick look at the structure of this data:

user=> (keys fips) (:table) user=> (keys (:table fips)) (:columnNames :columnTypes :rows) user=> (->> fips :table :columnNames) ["FIPS" "Name"]

Great, so we expect the rows to be a list of FIPS code and Name.

user=> (->> fips :table :rows (take 3) pprint) (["02000" "AK"] ["02013" "AK, Aleutians East"] ["02016" "AK, Aleutians West"])

Perfect. Now that’s we’ve done some exploratory work in the REPL, let’s shift back to an editor. Create a new file in src/scratch/crime.clj:

(ns scratch.crime (:require [cheshire.core :as json])) (def fips "A map of FIPS codes to their county names." (->> (json/parse-string (slurp "fips.json") true) :table :rows (into {})))

We’re just taking a snippet we wrote in the REPL–parsing the FIPS dataset–and writing it down for use as a part of a bigger program. We use (into {}) to convert the sequence of [fips, name] pairs into a map, just like we used into (sorted-set) to merge a list of keywords into a set earlier. into works just like conj, repeated over and over again, and is an incredibly useful tool for building up collections of things.

Back in the REPL, let’s check if that worked:

user=> (use 'scratch.crime :reload) nil user=> (fips "10001") "DE, Kent"

Remember, maps act like functions in Clojure, so we can use the fips map to look up the names of counties efficiently.

We also have to load the UCR crime file–so let’s split that load-and-parse code into its own function:

(defn load-json "Given a filename, reads a JSON file and returns it, parsed, with keywords." [file] (json/parse-string (slurp file) true)) (def fips "A map of FIPS codes to their county names." (->> "fips.json" load-json :table :rows (into {})))

Now we can re-use load-json to load the UCR crime file.

(defn most-duis "Given a JSON filename of UCR crime data for a particular year, finds the counties with the most DUIs." [file] (->> file load-json (sort-by :driving_under_influence) (take-last 10) (map #(select-keys % [:driving_under_influence :fips_county_code :fips_state_code])))) user=> (use 'scratch.crime :reload) (pprint (most-duis "2008.json")) nil ({:fips_state_code "06", :fips_county_code "067", :driving_under_influence 8589} {:fips_state_code "48", :fips_county_code "201", :driving_under_influence 10432} {:fips_state_code "32", :fips_county_code "003", :driving_under_influence 10443} {:fips_state_code "06", :fips_county_code "065", :driving_under_influence 10814} {:fips_state_code "53", :fips_county_code "033", :driving_under_influence 11439} {:fips_state_code "06", :fips_county_code "071", :driving_under_influence 13983} {:fips_state_code "06", :fips_county_code "059", :driving_under_influence 17572} {:fips_state_code "06", :fips_county_code "073", :driving_under_influence 18562} {:fips_state_code "04", :fips_county_code "013", :driving_under_influence 26235} {:fips_state_code "06", :fips_county_code "037", :driving_under_influence 45056})

Almost there. We need to join together the state and county FIPS codes into a single string, because that’s how fips represents the county code:

(defn fips-code "Given a county (a map with :fips_state_code and :fips_county_code keys), returns the five-digit FIPS code for the county, as a string." [county] (str (:fips_state_code county) (:fips_county_code county)))

Let’s write a quick test in test/scratch/crime_test.clj to verify that function works correctly:

(ns scratch.crime-test (:require [clojure.test :refer :all] [scratch.crime :refer :all])) (deftest fips-code-test (is (= "12345" (fips-code {:fips_state_code "12" :fips_county_code "345"})))) aphyr@waterhouse:~/scratch$ lein test scratch.crime-test lein test scratch.crime-test Ran 1 tests containing 1 assertions. 0 failures, 0 errors.

Great. Note that lein test some-namespace runs only the tests in that particular namespace. For the last step, let’s take the most-duis function and, using fips and fips-code, construct a map of county names to DUI reports.

(defn most-duis "Given a JSON filename of UCR crime data for a particular year, finds the counties with the most DUIs." [file] (->> file load-json (sort-by :driving_under_influence) (take-last 10) (map (fn [county] [(fips (fips-code county)) (:driving_under_influence county)])) (into {}))) user=> (use 'scratch.crime :reload) (pprint (most-duis "2008.json")) nil {"CA, Orange" 17572, "CA, San Bernardino" 13983, "CA, Los Angeles" 45056, "CA, Riverside" 10814, "NV, Clark" 10443, "WA, King" 11439, "AZ, Maricopa" 26235, "CA, San Diego" 18562, "TX, Harris" 10432, "CA, Sacramento" 8589}

Our question is, at least in part, answered: Los Angeles and Maricopa counties, in California and Arizona, have the most reports of drunk driving out of any counties in the 2008 Uniform Crime Reporting database. These might be good counties for a PSA campaign. California has either lots of drunk drivers, or aggressive enforcement, or both! Remember, this only tells us about reports of crimes; not the crimes themselves. Numbers vary based on how the state enforces the laws!

(ns scratch.crime (:require [cheshire.core :as json])) (defn load-json "Given a filename, reads a JSON file and returns it, parsed, with keywords." [file] (json/parse-string (slurp file) true)) (def fips "A map of FIPS codes to their county names." (->> "fips.json" load-json :table :rows (into {}))) (defn fips-code "Given a county (a map with :fips_state_code and :fips_county_code keys), returns the five-digit FIPS code for the county, as a string." [county] (str (:fips_state_code county) (:fips_county_code county))) (defn most-duis "Given a JSON filename of UCR crime data for a particular year, finds the counties with the most DUIs." [file] (->> file load-json (sort-by :driving_under_influence) (take-last 10) (map (fn [county] [(fips (fips-code county)) (:driving_under_influence county)])) (into {})))

Recap

In this chapter, we expanded beyond transient programs written in the REPL. We learned how projects combine static resources, code, and tests into a single package, and how projects can relate to one another through dependencies. We learned the basics of Clojure’s namespace system, which isolates distinct chunks of code from one another, and how to include definitions from one namespace in another via require and use. We learned how to write and run tests to verify our code’s correctness, and how to move seamlessly between the repl and code in .clj files. We made use of Cheshire, a Clojure library published on Clojars, to parse JSON–a common data format. Finally, we brought together our knowledge of Clojure’s basic grammar, immutable data structures, core functions, sequences, threading macros, and vars to explore a real-world problem.

Exercises

1. most-duis tells us about the raw number of reports, but doesn’t account for differences in county population. One would naturally expect counties with more people to have more crime! Divide the :driving_under_influence of each county by its :county_population to find a prevalence of DUIs, and take the top ten counties based on prevalence. How should you handle counties with a population of zero?

2. How do the prevalence counties compare to the original counties? Expand most-duis to return vectors of [county-name, prevalence, report-count, population] What are the populations of the high-prevalence counties? Why do you suppose the data looks this way? If you were leading a public-health campaign to reduce drunk driving, would you target your intervention based on report count or prevalence? Why?

3. We can generalize the most-duis function to handle any type of crime. Write a function most-prevalent which takes a file and a field name, like :arson, and finds the counties where that field is most often reported, per capita.

4. Write a test to verify that most-prevalent is correct.

A few weeks ago I criticized a proposal by Antirez for a hypothetical linearizable system built on top of Redis WAIT and a strong coordinator. I showed that the coordinator he suggested was physically impossible to build, and that anybody who tried to actually implement that design would run into serious problems. I demonstrated those problems (and additional implementation-specific issues) in an experiment on Redis' unstable branch.

Antirez' principal objections, as I understand them, are:

1. Some readers mistakenly assumed that the system I discussed was a proposal for Redis Cluster.
2. I showed that the proposal was physically impossible, but didn’t address its safety if it were possible.
3. The impossible parts of the proposed system could be implemented in a real asynchronous network by layering in additional constraints on the leader election process.

I did not assert that this was a design for Redis Cluster, and the term “Redis Cluster” appeared nowhere in the post. To be absolutely clear; at no point in these posts have I discussed Redis Cluster. Antirez acknowledges that Cluster makes essentially no safety guarantees, so I haven’t felt the need to write about it.

I did, however, provide ample reference to multiple points in the mailing list thread where Antirez made strong claims about the consistency of hypothetical systems built with Redis WAIT and strong failover coordinators, and cited the gist in question as the canonical example thereof. I also thought it was clear that the system Antirez proposed were physically impossible, and that in addition to those flaws I analyzed weaker, practically achievable designs. However, comments on the post, on Twitter, and on Hacker News suggest a clarification is in order.

If Aphyr was interested in a real discussion, I could just agree about the obvious, that if you can totally control the orchestration of the system then synchronous replication is obviously a building block that can be part of a strong consistent system. Apparently he as just interested in spreading FUD. Congratulations.

Allow me to phrase this unambiguously: not only is this system impossible to build, but even if it were possible, it would not be linearizable.

There are obvious flaws in Antirez’s proposal, but I’m not convinced that simply explaining those flaws will do enough good. This is unlikely to be the last of Antirez'–or anyone else’s–consistency schemes, and I can’t possibly QA all of them! Instead, I’d like to raise the level of discussion around linearizability by showing how to find problems in concurrent algorithms–even if you don’t know where those problems lie.

So here, have a repo.

Knossos

Named after the ruins where Linear B was discovered, Knossos identifies whether or not a history of events from a concurrent system is linearizable. We’re going to be working through knossos.core and knossos.redis in this post. I’ll elide some code in this post for clarity, but it’s all there in the repo.

In Knossos, we analyze histories. Histories are a sequence of operations, each of which is a map:

[{:process :c2, :type :invoke, :f :write, :value 850919} {:process :c1, :type :ok, :f :write, :value 850914} {:process :c1, :type :invoke, :f :read, :value 850919} {:process :c1, :type :ok, :f :read, :value 850919}]

:process is the logical thread performing the operation. :invoke marks the start of an operation, and :ok marks its completion. :f is the kind of operation being invoked, and :value is an arbitrary argument for that operation, e.g. the value of a read or write. The interpretation of :f and :value depends on the datatype we’re modeling: for a set, we might support :add, :remove, and :contains.

To verify the history, we need a model which verifies that a sequence of operations applied in a particular order is valid. For instance, if we’re describing a register (e.g. a variable in a programming language–a mutable reference that points to a single value), we would like to enforce that every read sees the most recently written value. If we write 1, then write 2, then read, the read should see 2.

We represent a model with the function knossos.core/step which takes a model’s state, and an operation, and returns a new model. If the operation applied to that state would be invalid, step throws.

(defprotocol Model (step [model op])) (defrecord Register [value] Model (step [r op] (condp = (:f op) :write (Register. (:value op)) :read (if (or (nil? (:value op)) ; We don't know what the read was (= value (:value op))) ; Read was a specific value r (throw (RuntimeException. (str "read " (pr-str (:value op)) " from register " value)))))))

A Register implements the Model protocol and defines two functions: :write, which returns a modified copy of the register with the new value, and :read, which returns the register itself–if the read corresponds to the current value.

In a real experiment (as opposed to a mathematical model), we may not know what the read’s value will be until it returns. We allow any read with an unknown (nil?) value to succeed; when the read comes back we can re-evaluate the model with the value in mind.

This definition of step lets us reduce a sequence of operations over the model to produce a final state:

user=> (reduce step (Register. 0) [{:process :c1, :type :ok, :f :write, :value 4} {:process :c2, :type :ok, :f :read, :value 4}] #knossos.core.Register{:value 4} user=> (reduce step (Register. 0) [{:process :c1, :type :ok, :f :write, :value 4} {:process :c2, :type :ok, :f :read, :value 7}]) RuntimeException read 7 from register 4 knossos.core.Register (core.clj:43)

Now our problem consists of taking a history with pairs of (invoke, ok) operations, and finding an equivalent history of single operations which is consistent with the model. This equivalent single-threaded history is called a linearization; a system is linearizable if at least one such history exists. The actual definition is a bit more complicated, accounting for unmatched invoke/ok pairs, but this a workable lay definition.

Finding linearizations

The space of possible histories is really big. If we invoke 10 operations and none of them return OK, any subset of those operations might have taken place. So first we have to take the power set for any incomplete operations: that’s 2^n. Then for each of those subsets we have to compute every possible interleaving of operations. If every operations' invocation and completion overlap, we construct a full permutation. That’s m!.

“Did you just tell me to go fuck myself?”

“I believe I did, Bob.”

My initial approach was to construct a radix tree of all possible histories (or, equivalently, a transition graph), and try to exploit degeneracy to prune the state space. Much of the literature on linearizability generates the full set of sequential histories and tests each one separately. Microsoft Research’s PARAGLIDER, in the absence of known linearization points, relies on this brute-force approach using the SPIN model checker.

A straightforward way to automatically check whether a concurrent history has a corresponding linearization is to simply try all possible permutations of the concurrent history until we either find a linearization and stop, or fail to find one and report that the concurrent history is not linearizable. We refer to this approach as Automatic Linearization… Despite its inherent complexity costs, we do use this method for checking concurrent histories of small length (e.g. less than 20). In practice, the space used for concurrent algorithms is typically small because incorrect algorithms often exhibit an incorrect concurrent history which is almost sequential.

In my experiments, enumerating all interleavings and testing each one started to break down around 12 to 16-operation histories.

Burckhardt, Dern, Musuvathi, and Tan wrote Line-Up, which verifies working C# algorithms by enumerating all thread interleavings through the CHESS model checker. This limits Line-Up to verifying only algorithms with a small state space–though this tradeoff allows them to do some very cool things around blocking and data races.

Two papers I know of attempt to reduce the search space itself. Golab, Li, and Shah developed a wicked-smart online checker using Gibbons and Korach’s algorithm and dynamic programming, but GK applies only to registers; I’d like to be able to test sets, queues, and other, more complex datatypes. Yang Liu, et al use both state space symmetry and commutative operations to drastically prune the search space for their linearizability analysis, using the PAT model checker.

I haven’t built symmetry reduction yet, but I do have a different trick: pruning the search space incrementally, as we move through the history, by using the model itself. This is a lot more complex than simply enumerating all possible interleavings–but if we can reject a branch early in the history, it saves huge amounts of work later in the search. The goal is to keep the number of possible worlds bounded by the concurrency of the history, not the length of the history.

So let’s do something paradoxical. Let’s make the problem even harder by multiplying the state space by N. Given a history of four invocations

[a b c d]

Let’s consider the N histories

[] [a] [a b] [a b c] [a b c d]

[] is trivially linearizable; nothing happens. [a] has two possible states: in one timeline, a completes. In another, a does not complete–remember, calls can fail. Assuming [a] passes the model, both are valid linearizations.

For the history [a b] we have five options. Neither a nor b can occur, one or the other could occur, or both could occur, in either order.

[] [a] [b] [a b] [b a]

Let’s say the register is initially nil, a is “write 5”, and b is “read 5”. [b] can’t take place on its own because we can’t read nil and get 5, and [b a] is invalid for the same reason. So we test five possibilities and find three linearizations. Not too bad, but we’re starting to see a hint of that n! explosion. By the third juncture we’ll have 16 sequential histories to test:

user=> (mapcat permutations (subsets ['a 'b 'c])) ([] (a) (b) (c) (a b) (b a) (a c) (c a) (b c) (c b) (a b c) (a c b) (b a c) (b c a) (c a b) (c b a))

And by the time we have to work with 10 operations concurrently, we’ll be facing 9864101 possible histories to test; it’ll take several minutes to test that many. But here’s the key: only some of those histories are even reachable, and we already have a clue as to which.

The 3-operation histories will include some histories which we already tested. [b a c], for instance, begins with [b a]; so if we already tested [b a] and found it impossible, we don’t even have to test [b a c] at all. The same goes for [b c a]–and every history, of any length, which begins with b.

So instead of testing all six 3-operation histories, we only have to test four. If the model rejects some of those, we can use those prefixes to reject longer histories, and so on. This dramatically cuts the state space, allowing us to test much longer histories in reasonable time.

Knossos uses Clojure’s shared-state immutable data structures to implement this search efficiently. We reduce over the history in order, maintaining a set of possible worlds. Every invocation bifurcates the set of worlds into those in which the operation happens immediately, and those in which it is deferred for later. Every completion prunes the set of worlds to only those in which the given operation completed. We can then ask Knossos to produce a set of worlds–linearized histories and the resulting states of their models–which are consistent with a given concurrent history.

Testing a model

Now let’s apply that linearizability checker to a particular system. We could measure a system experimentally, like I’ve done with Jepsen, or we could generate histories based on a formal model of a system. As an example, let’s test the model suggested by Antirez, describing a linearizable system built on top of Redis, WAIT, and a magical coordinator. As I described earlier, this model is physically impossible; it can not be built because the coordinator would need to violate the laws of physics. But let’s pretend we live on Planet Terah, and see whether the system is actually sound.

Antirez writes:

There are five nodes, using master-slave replication. When we start A is the master.

The nodes are capable of synchronous replication, when a client writes, it gets as relpy the number or replicas that received the write. A client can consider a write accepted only when “3” or more is returned, otherwise the result is not determined (false negatives are possbile).

Every node has a serial number, called the replication offset. It is always incremented as the replication stream is processed by a replica. Replicas are capable of telling an external entity, called “the controller”, what is the replication offset processed so far.

At some point, the controller, dictates that the current master is down, and decides that a failover is needed, so the master is switched to another one, in this way:

1. The controller completely partition away the current master.
2. The controller selects, out of a majority of replicas that are still available, the one with the higher replication offset.
3. The controller tells all the reachable slaves what is the new master: the slaves start to get new data from the new master.
4. The controller finally reconfigure all the clients to write to the new master.

So everything starts again. We assume that a re-appearing master, or other slaves that are again available after partitions heal, are capable of understand what the new master is. However both the old master and the slaves can’t accept writes. Slaves are read-only, while the re-apprearing master will not be able to return the majority on writes, so the client will not be able to consider the writes accepted.

In this model, it is possible to reach linearizability? I believe, yes, because we removed all the hard part, for which the strong protocols like Raft use epochs.

If you’ve spotted some of the problems in this approach, good work! But let’s say there were no obvious problems, and we weren’t sure how to find some. To do this, we’ll need a description of the system which is unambiguous and complete. Something a computer can understand.

First off, let’s describe a node:

(defn node "A node consists of a register, a primary it replicates from, whether it is isolated from all other nodes, a local replication offset, and a map of node names to known replication offsets." [name] {:name name :register nil :primary nil :isolated false :offset 0 :offsets {}})

Seems straightforward enough. This is a really simple model of a Redis server–one which only has a single register to read and write. We could extend it with more complex types, like lists and sets, but we’re trying to keep things simple. Notice how things like “Each node has a serial number, called the replication offset” have been translated into a field in a structure. We’ve also encoded things which were implicit in the proposal, like the fact that the WAIT command relies on the node knowing the replication offsets of its peers.

Remember, in proofs we try to deal as much as possible with immutable, pure systems; Clojure, Erlang, ML, and Haskell all lend themselves naturally to this approach. If you’re writing your checker in something like Ruby or Java, try to write immutable code anyway. It may be a bit unnatural, but it’ll really simplify things later.

(defn client "A client is a singlethreaded process which can, at any time, have at most one request in-flight to the cluster. It has a primary that it uses for reads and writes, and an in-flight request. Clients can be waiting for a response, in which case :wait will be the replication offset from the primary they're awaiting. :waiting is the value they're waiting for, if conducting a write." [name] {:name name :node nil :writing nil :waiting nil})

We’ll also need a coordinator. This one’s simple:

(defn coordinator "A controller is an FSM which manages the election process for nodes. It comprises a state (the phase of the election cycle it's in), and the current primary." [primary] {:state :normal :primary primary})

Next we’ll put all these pieces together into a full system. Phrases like “When we start A is the master,” are translated into code which picks the first node as the primary, and code which ensures that primary state is reflected by the other nodes and the coordinator.

(defn system "A system is comprised of a collection of nodes, a collection of clients, and a coordinator; plus a *history*, which is the set of operations we're verifying is linearizable." [] (let [node-names [:n1 :n2 :n3] nodes (->> node-names (map node) ; Fill in offset maps (map (fn [node] (->> node-names (remove #{(:name node)}) (reduce #(assoc %1 %2 0) {}) (assoc node :offsets))))) ; Initial primary/secondary state [primary & secondaries] nodes nodes (cons primary (map #(assoc % :primary (:name primary)) secondaries)) ; Construct a map of node names to nodes nodes (->> nodes (map (juxt :name identity)) (into {})) ; Construct clients clients (->> [:c1 :c2] (map client) (map #(assoc % :node (:name primary))) (map (juxt :name identity)) (into {}))] {:coordinator (coordinator (:name primary)) :clients clients :nodes nodes :history []}))

Note that we’ve introduced, for any given state of the system, the history of operation which brought us to this point. This is the same history that we’ll be evaluating using our linearizability checker.

This formally describes the state of the model. Now we need to enumerate the state transitions which bring the system from one state to another.

State transitions

First, we need a model of Redis reads and writes. Writes have two phases: an invocation and a response to the client–implemented with WAIT.

(def write-state (atom 0)) (defn client-write "A client can send a write operation to a node." [system] (->> system clients (filter free-client?) (filter (partial valid-client? system)) (map (fn [client] (let [; Pick a value to write value (swap! write-state inc) ; Find the node name for this client node (:node client) ; And the new offset. offset (inc (get-in system [:nodes node :offset]))] (-> system (assoc-in [:nodes node :register] value) (assoc-in [:nodes node :offset] offset) (assoc-in [:clients (:name client) :waiting] offset) (assoc-in [:clients (:name client) :writing] value) (log (invoke-op (:name client) :write value))))))))

client-write is a function which takes a system and returns a sequence of possible systems, each of which corresponds to one client initiating a write to its primary. We encode multiple constraints here:

1. Clients can only initiate a write when they are not waiting for another response–i.e. clients are singlethreaded.
2. Clients must be connected to a node which is not isolated and thinks that it is a primary. Note that this assumes a false linearization point: in the real world, these checks are not guaranteed to be instantaneous. We are being overly generous to simplify the model.

For each of these clients, we generate a unique number to write using (swap write-state inc), set the primary’s register to that value, increment the primary’s offset, and update the client–it is now waiting for that particular replication offset to be acknowledged by a majority of nodes. We also keep track of the value we wrote, just so we can fill it into the history later.

Finally, we update the history of the system, adding an invocation of a write, from this client, for the particular value.

When a client’s primary determines that a majority of nodes have acknowledged the offset that the client is waiting for, we can complete the write operation.

(defn client-write-complete "A reachable primary node can inform a client that its desired replication offset has been reached." [system] (->> system clients (remove free-client?) (filter (partial valid-client? system)) (keep (fn [client] (let [offset (-> system :nodes (get (:node client)) majority-acked-offset)] (when (<= (:waiting client) offset) (-> system (assoc-in [:clients (:name client) :waiting] nil) (assoc-in [:clients (:name client) :writing] nil) (log (ok-op (:name client) :write (:writing client))))))))))

Again, note the constraints: we can’t always complete writes. Only when the client is waiting, and the client is connected to a valid non-isolated primary, and the replication offset is acked by a majority of nodes, can these transitions take place.

keep is a Clojure function analogous to map and filter combined: only non-nil results appear in the output sequence. We use keep here to compactly express that only clients which have satisfied the majority offset acknowledgement constraint are eligible for completion.

Reads are similar to writes, but we make another generous allowance: reads are assumed to be a linearization point of the model, and therefore take place instantaneously. We add both invocation and completion operations to the log in one step.

(defn client-read "A client can read a value from its node, if primary and reachable. Reads are instantaneous." [system] (->> system clients (filter free-client?) (filter (partial valid-client? system)) (map (fn [client] (let [node (:node client) value (get-in system [:nodes node :register])] (-> system (log (invoke-op (:name client) :read nil)) (log (ok-op (:name client) :read value))))))))

Replication

Redis replication is asynchronous: in one phase the client copies data from the primary, and after that, updates the primary with its replication offset. We assume that each phase takes place instantaneously. Is replication actually a linearization point in Redis? I don’t know–but we’ll be generous again.

(defn replicate-from-primary "A node can copy the state of its current primary, if the primary is reachable." [system] (->> system nodes (remove :isolated) (keep (fn [node] (when-let [primary (get-node system (:primary node))] (when-not (:isolated primary) (-> system (assoc-in [:nodes (:name node) :register] (:register primary)) (assoc-in [:nodes (:name node) :offset] (:offset primary)) (log (op (:name node) :info :replicate-from-primary (:primary node))))))))))

Pretty straightforward: each node can, if it has a primary and neither is isolated, copy its register state and offset. We’ll be generous and assume the primary’s total oplog is applied instantly and atomically.

The acknowledgement process is basically the reverse: we update the offset cache in the primary, so long as nodes are connected.

(defn ack-offset-to-primary "A node can inform its current primary of its offset, if the primary is reachable." [system] (->> system nodes (remove :isolated) (keep (fn [node] (when-let [primary (get-node system (:primary node))] (when-not (:isolated primary) (-> system (assoc-in [:nodes (:primary node) :offsets (:name node)] (:offset node)) (log (op (:name node) :info :ack-offset-to-primary (:primary node))))))))))

Failover

Four functions, corresponding to each of the four steps in the algorithm. We ensure they happen in order by ensuring that a transition can only take place if the coordinator just completed the previous step.

1) The controller completely partition away the current master.

(defn failover-1-isolate "If the coordinator is in normal mode, initiates failover by isolating the current primary." [system] (let [coord (:coordinator system)] (when (= :normal (:state coord)) (-> system (assoc-in [:coordinator :state] :isolated) (assoc-in [:coordinator :primary] nil) (assoc-in [:nodes (:primary coord) :isolated] true) (log (op :coord :info :failover-1-isolate (:primary coord)))))))

Notice how we formalized the English statement by encoding properties of the network throughout the model: each state transition checks the partitioned state of the nodes involved. This is an oversimplification of the real system, because this part of the algorithm is impossible in an asynchronous network: it modifies the current primary’s state directly instead of sending it a message. We’re being generous by assuming the network propagates messages instantly; a more thorough model would explicitly model the loss and delay of messages.

2) The controller selects, out of a majority of replicas that are still available, the one with the higher replication offset.

Again, translation is straightforward; in the model we can freely violate the laws of physics.

(defn failover-2-select "If the coordinator has isolated the old primary, selects a new primary by choosing the reachable node with the highest offset." [system] (let [coord (:coordinator system)] (when (= :isolated (:state coord)) (let [candidates (->> system nodes (remove :isolated))] ; Gotta reach a majority (when (<= (inc (Math/floor (/ (count (nodes system)) 2))) (count candidates)) (let [primary (:name (apply max-key :offset candidates))] (-> system (assoc-in [:coordinator :state] :selected) (assoc-in [:coordinator :primary] primary) (log (op :coord :info :failover-2-select primary)))))))))

3) The controller tells all the reachable slaves what is the new master: the slaves start to get new data from the new master.

You know the drill. We create a false point of linearization and assume this broadcast is atomic.

(defn failover-3-inform-nodes "If the coordinator has selected a new primary, broadcasts that primary to all reachable nodes." [system] (let [coord (:coordinator system) primary (:primary coord)] (when (= :selected (:state coord)) (-> system (assoc-in [:coordinator :state] :informed-nodes) (assoc :nodes (->> system :nodes (map (fn [ [name node] ] [name (cond ; If the node is isolated, state is ; unchanged. (:isolated node) node ; If this is the new primary node, make ; it a primary. (= primary name) (assoc node :primary nil) ; Otherwise, set the primary. :else (assoc node :primary primary))])) (into {}))) (log (op :coord :info :failover-3-inform-nodes primary))))))

4) The controller finally reconfigure all the clients to write to the new master.

Here too!

(defn failover-4-inform-clients "If the coordinator has informed all nodes of the new primary, update all client primaries." [system] (let [coord (:coordinator system) primary (:primary coord)] (when (= :informed-nodes (:state coord)) (-> system (assoc-in [:coordinator :state] :normal) (assoc :clients (->> system :clients (map (fn [ [name client] ] [name (assoc client :node primary)])) (into {}))) (log (op :coord :info :failover-4-inform-clients primary))))))

At each step there is exactly one failover transition that can happen–since the coordinator is magically sequential and never fails.

(defn failover "All four failover stages combined." [system] (when-let [system' (or (failover-1-isolate system) (failover-2-select system) (failover-3-inform-nodes system) (failover-4-inform-clients system))] (list system')))

Putting it all together

We assume that a re-appearing master, or other slaves that are again available after partitions heal, are capable of understand what the new master is.

I struggled with this, and I actually don’t know how to interpret this part of the proposal. Erring on the side of safety, let’s omit any resurrection of isolated nodes. Once a node fails, it stays dead forever. If you let them come back, things get much more dangerous.

Only one last part remains: we need to express, in a single function, every allowable state transition.

(defn step "All systems reachable in a single step from a given system." [system] (concat (client-write system) (client-write-complete system) (client-read system) (replicate-from-primary system) (ack-offset-to-primary system) (failover system)))

OK. So now we can evolve any particular state of the system in various directions. Let’s take a look at a basic system:

user=> (use 'knossos.redis) nil user=> (-> (system) pprint) {:coordinator {:state :normal, :primary :n1}, :clients {:c1 {:name :c1, :node :n1, :writing nil, :waiting nil}, :c2 {:name :c2, :node :n1, :writing nil, :waiting nil}}, :nodes {:n1 {:name :n1, :register nil, :primary nil, :isolated false, :offset 0, :offsets {:n3 0, :n2 0}}, :n2 {:name :n2, :register nil, :primary :n1, :isolated false, :offset 0, :offsets {:n3 0, :n1 0}}, :n3 {:name :n3, :register nil, :primary :n1, :isolated false, :offset 0, :offsets {:n2 0, :n1 0}}}, :history []}

What happens if we do a write?

user=> (-> (system) client-write rand-nth pprint) {:coordinator {:state :normal, :primary :n1}, :clients {:c1 {:name :c1, :node :n1, :writing nil, :waiting nil}, :c2 {:name :c2, :node :n1, :writing 10, :waiting 1}}, :nodes {:n1 {:name :n1, :register 10, :primary nil, :isolated false, :offset 1, :offsets {:n3 0, :n2 0}}, :n2 {:name :n2, :register nil, :primary :n1, :isolated false, :offset 0, :offsets {:n3 0, :n1 0}}, :n3 {:name :n3, :register nil, :primary :n1, :isolated false, :offset 0, :offsets {:n2 0, :n1 0}}}, :history [{:process :c2, :type :invoke, :f :write, :value 10}]}

Notice that client-write returns two systems: one in which :c1 writes, and one in which :c2 writes. We pick a random possibility using rand-nth. In this case, :c2 wrote the number 10 to :n1, and is waiting for replication offset 1 to be acknowledged. :n1, but not :n2 or :n3, has received the write. Note the history of this system reflects the invocation, but not the completion, of this write.

Let’s try to complete the write:

user=> (-> (system) client-write rand-nth client-write-complete pprint) ()

There are no possible worlds where the write can complete at this point. Why? Because the replication offset on the primary hasn’t completed yet. This is the whole point of Redis WAIT: we can’t consider a write complete until it’s been acknowledged.

user=> (-> (system) client-write rand-nth replicate-from-primary first ack-offset-to-primary first client-write-complete pprint) ({:coordinator {:state :normal, :primary :n1}, :clients {:c1 {:name :c1, :node :n1, :writing nil, :waiting nil}, :c2 {:name :c2, :node :n1, :writing nil, :waiting nil}}, :nodes {:n1 {:name :n1, :register 15, :primary nil, :isolated false, :offset 1, :offsets {:n3 0, :n2 1}}, :n2 {:name :n2, :register 15, :primary :n1, :isolated false, :offset 1, :offsets {:n3 0, :n1 0}}, :n3 {:name :n3, :register nil, :primary :n1, :isolated false, :offset 0, :offsets {:n2 0, :n1 0}}}, :history [{:process :c1, :type :invoke, :f :write, :value 15} {:process :n2, :type :info, :f :replicate-from-primary, :value :n1} {:process :n2, :type :info, :f :ack-offset-to-primary, :value :n1} {:process :c1, :type :ok, :f :write, :value 15}]})

A successful write! The value 15 has been replicated to both :n1 and :n2, and with the offset map on :n1 updated, the WAIT request for the client can complete. The history reflects the invocation and completion of :c1’s write request.

Having written down the state of the system, and encoded all possible state transitions in the step function, we can find random trajectories through the system by interleaving calls to step and rand-nth. Because we don’t allow the resurrection of nodes, this system can simply halt, unable to make progress. In that case, we simply return the terminal state.

(defn trajectory "Returns a system from a randomized trajectory, `depth` steps away from the given system." [system depth] (if (zero? depth) system (let [possibilities (step system)] (if (empty? possibilities) ; Dead end system ; Descend (recur (rand-nth possibilities) (dec depth))))))

Because our trajectory evolution is randomized, the histories it generates will often contain extraneous garbage–repeated sequences of identical reads, for instance, or replicating the same state over and over again. We could go back and re-explore the state space, omitting certain transitions in the search of a simpler trajectory–but for now, we’ll take the random trajectories.

Model checking

We’ve built a simple model of a single-threaded linearizable register, a concurrent model of a hypothetical Redis system, and a verifier which tests that a history is linearizable with respect to a singlethreaded model. Now let’s combine these three elements.

First, a way to show the system that we wound up in, and the history that led us there. We’ll use linearizable-prefix to find the longest string of the history that was still linearizable–that’ll help show where, exactly, we ran out of options.

(defn print-system [system history] (let [linearizable (linearizable-prefix (->Register nil) history)] (locking *out* (println "\n\n### No linearizable history for system ###\n") (pprint (dissoc system :history)) (println "\nHistory:\n") (pprint linearizable) (println "\nUnable to linearize past this point!\n") (pprint (drop (count linearizable) history)))))

Then we’ll generate a bunch of trajectories of, say, 15 steps apiece, and show any which have nonlinearizable histories.

(deftest redis-test (dothreads [i 4] ; hi haters (dotimes [i 10000] (let [system (trajectory (system) 15)] ; Is this system linearizable? (let [history (complete (:history system)) linears (linearizations (->Register nil) history)] (when (empty? linears) (print-system system history)) (is (not (empty? linears)))))))

And we’re ready to go. Is the model Antirez proposed linearizable?

$ lein test knossos.redis-test ### No linearizable history for system ### {:coordinator {:state :normal, :primary :n2}, :clients {:c1 {:name :c1, :node :n2, :writing nil, :waiting nil}, :c2 {:name :c2, :node :n2, :writing 9, :waiting 2}}, :nodes {:n1 {:name :n1, :register 9, :primary nil, :isolated true, :offset 2, :offsets {:n3 0, :n2 1}}, :n2 {:name :n2, :register 5, :primary nil, :isolated false, :offset 1, :offsets {:n3 0, :n1 0}}, :n3 {:name :n3, :register nil, :primary :n2, :isolated false, :offset 0, :offsets {:n2 0, :n1 0}}}} History: [{:process :c2, :type :invoke, :f :write, :value 5} {:process :n2, :type :info, :f :replicate-from-primary, :value :n1} {:process :n2, :type :info, :f :ack-offset-to-primary, :value :n1} {:process :c2, :type :ok, :f :write, :value 5} {:process :n2, :type :info, :f :replicate-from-primary, :value :n1} {:process :c2, :type :invoke, :f :write, :value 9} {:process :n3, :type :info, :f :ack-offset-to-primary, :value :n1} {:process :c1, :type :invoke, :f :read, :value 9} {:process :c1, :type :ok, :f :read, :value 9} {:process :coord, :type :info, :f :failover-1-isolate, :value :n1} {:process :coord, :type :info, :f :failover-2-select, :value :n2} {:process :coord, :type :info, :f :failover-3-inform-nodes, :value :n2} {:process :coord, :type :info, :f :failover-4-inform-clients, :value :n2} {:process :n3, :type :info, :f :ack-offset-to-primary, :value :n2} {:process :n3, :type :info, :f :ack-offset-to-primary, :value :n2} {:process :c1, :type :invoke, :f :read, :value 5}] Unable to linearize past this point! ({:process :c1, :type :ok, :f :read, :value 5}) lein test :only knossos.redis-test/redis-test FAIL in (redis-test) (redis_test.clj:44) expected: (not (empty? linears)) actual: (not (not true)) Ran 1 tests containing 38340 assertions. 6 failures, 0 errors.

No, it isn’t.

What happened here?

Knossos generated a state of the system which it believes is possible, under the rules of the Redis model we constructed, but not linearizable with respect to the register model. Up until the final read, Knossos could still construct a world where things made sense, but that last read was inconsistent with every possible interpretation. Why?

Well, in the final state, n1 is isolated with value 9 at offset 2, n2 is a primary with value 5 at offset 1, and n3 thinks the value is nil. n3’s offset is 0; it never participated in this history, so we can ignore it.

1. First, c2 writes 5 to n1. n2 replicates and acknowledges the write of 5, and c2’s write completes.
2. n2 initiates a (noop) replication from n1.
3. c2 initiates a write of 9 to n1. c1 concurrently initiates a read from n1, which will see 9.
4. n2 completes its replication; state is unchanged.
5. Then, a failover occurs. The coordinator performs all four steps atomically, so no concurrency questions there. n2 is selected as the new primary and n1 is isolated.
6. n3 acknowledges its offset of 0 to n2 twice; both of which are noops since n2 already thinks n3’s offset is 0.
7. Finally, c1 invokes a read from n2 and sees 5. This is the read which proves the system is inconsistent. Up until this point the history has been linearizable–we could have assumed, for instance, that the write of 9 failed and the register has always been 5, but that assumption was invalidated by the successful read of 9 by c1 earlier. We also could have assumed that the final read of 5 failed–but when it succeeded, Knossos ran out of options.

This case demonstrates that reads are a critical aspect of linearizability. Redis WAIT is not transactional. It allows clients to read unreplicated state from the primary node, which is just as invalid as reading stale data from secondaries.

I hope this illustrates beyond any shred of doubt: not only is Antirez’s proposal physically impossible, but even wildly optimistic formal interpretations of his proposal are trivially non-linearizable.

Yeah, this is Fear, Uncertainty, and Doubt. You should be uncertain about algorithms without proofs. You should doubt a distributed system without a formal model. You should be fearful that said system will not live up to its claims.

Now you’ve got another tool to validate that uncertainty for yourself.

Math is hard; let’s go model checking

Proving linearizability is hard. Much harder than proving a system is not linearizable, when you get down to it. All I had to do here was find a single counterexample; but proving linearizability requires showing that every history is valid. Traditionally one does this by identifying all the linearization points of an algorithm–the points where things take place atomically–which is a subtle and complex process, especially where the linearization point depends on runtime behavior or lies outside the code itself.

Moreover, I am not that great at proofs–and I don’t want to exclude readers who don’t have the benefit of formal training. I want to equip ordinary programmers with the motivation and tools to reason about their systems–and for that, model checking is a terrific compromise.

There are many tools available for formal modeling of concurrency. Leslie Lamport’s TLA+ is the canonical tool for concurrency proofs, but its learning curve is steep to say the least and I have a lot of trouble trying to compose its models. Bell Labs' Spin is more accessible for programmers, encoding its models in a language called Promela. Spin has excellent tooling–it can even extract models from C code with assistance. There’s also Erigone, a reimplementation of Spin, and the aforementioned Line-Up for C#.

Knossos is a dead-simple verification system I hacked out in a week; it takes advantage of Clojure’s concise data-structure literals, immutable shared-state data structures, and concise syntax to make designing models and checking their linearizability easier. Knossos probably has some bugs, so be sure to check the failure cases by hand!

No matter which model checker you use, all of these systems let you formalize your algorithms by writing them down in a concise, unambiguous form–either a modeling language or a full programming language– and then verify that those models conform to certain invariants by exploring the state space. By working with a proof assistant, some of these specifications can also prove that the invariants hold always, instead of only proving that the invariants can fail to hold.

We verified a toy system in this blog post, but all the key elements are there. State, transition functions, invariants, and a model to verify against. We use hierarchical data structures and functions to break up the model into smaller, more manageable pieces. We generated counterexamples from probabilistic trajectories through the model.

Real models look just like this. Take a look at the model and proof sketch of the RAFT consensus algorithm, and see if you can spot the definitions of state, transitions, and invariants. Note that this isn’t a full proof–more like a sketch–and it relies on some propositions like type safety which are not mechanically verified, but this paper illustrates both formal and English proof techniques nicely.

This is the kind of argument you need to make, as a database engineer, before asserting a given system is linearizable. Formal verification will catch both obvious and subtle bugs before you, or your readers, try to implement them.