Now you might hope to do some static checking on this. It might be hard oreasy. But even having the property written down in a formal way is a realhelp. You can test it by generating test data, which is, indeed, just whatQuickCheck does.

So rather than trying to write down specifications for all that a programdoes I think it’s much more productive to write down partial specifications.Perhaps multiple partial specifications. And then check them either bytesting or by dynamic checks or by static checks. You never prove that yourprogram is right. You just increase your confidence that it’s right. And Ithink that’s all that anybody ever does.

Seibel: So you define however many properties, covering the things youcare about. And then you can choose to confirm that those propertiesactually hold either statically or dynamically, depending on what’s actuallyfeasible. Because we may not know how to statically check them all?

Peyton Jones: Right. But in a functional setting, you have a better chance.But we’ve still been dragging our feet a bit about demonstrating that.Nevertheless—step one is to write down these properties in the first place.

But I think the big thing is to get away from this monolithic, all-or-nothingstory about specification and to say that you can do useful static anddynamic tests on partial specifications. These will increase your confidencein the correctness of your program and that is all you can possibly hope for.

Even the allegedly complete specifications miss out—you know, it has towork in .1 of a second. Or must fit in 10KB of memory. Resource things areoften not covered. Or timing things. There’s endless little stuff that meansthe program might actually not function as desired even though it meets itsformal specification. So I think we’re kidding ourselves to say we’ve actuallyproved the whole thing is completely right. Best thing to do is toacknowledge that and say we’re improving our confidence—that’s whatwe’re doing. And that can start quite modestly—you might have improvedyour confidence by 75 percent with only 5 percent of the effort. That’d begood.

Seibel: Let’s talk about concurrency a little bit. Guy Steele asked me to askyou: “Is STM going to save the world?”

Peyton Jones: Oh, no. STM is not going to save the world on its own.Concurrency, and parallel programming generally, is a many-faceted beastand I don’t think it will be slain by a single bullet. I’m a diversifist when itcomes to concurrency.

It’s tempting to say, “Use one programming paradigm for writing concurrentprograms and implement it really well and that’s it;” people should just learnhow to write concurrent programs using that paradigm. But I just don’tbelieve it. I think for some styles of programming you might want to usemessage passing. For others you might want to use STM. For others dataparallelism is much better. The programmer is going to need to grapple withmore than one way to do it.

But if you ask me, is STM better than locks and condition variables? Nowyou’re comparing like with like. Yes. I think it completely dominates locksand condition variables. So just forget locks and condition variables. Formultiple program counters, multiple threads, diddling on shared memory ona shared-memory multicore: STM. But is that the only way to writeconcurrent programs? Absolutely not.

Seibel: A criticism I’ve heard of STM was that when it really gets down toit, optimistic concurrency won’t allow as much concurrency as you hope. Ithink the claim was you can fairly easily get in these situations where you’rereally not making progress.

Peyton Jones: You do have to worry about starvation. My favoriteexample here is of one big transaction that keeps failing to commit becausea little transaction gets in there and commits first. So an example would be alibrarian who’s reorganizing their library. They start optimisticallyreorganizing their library. And they’ve got two-thirds of the way throughand an undergraduate comes along and borrows a book. Well, he commitshis transaction successfully because the library reorganization hasn’tcommitted. The librarian gets to the end and discovers, ah, I saw aninconsistent view of memory because the library changed while I wasreorganizing it so I just have to go back and start again.

Seibel: In a locks-and-condition-variables program it would probably go theother way—the librarian would lock the library and nobody could check outbooks until it’s completely reorganized. So you would probably look at thisproblem and immediately say, “We can’t lock the library until we’re done,”disallowing checkouts so we have to come up with some hairier lockingscheme.

Peyton Jones: Right. Make a little sub-library or something—put thecommonly borrowed books out there so undergraduates can borrow themwhile you lock the main library and reorganize it or something. So nowyou’ve got to think of an application-specific strategy and now you’ve got toexpress it in some way. Well, the same problem arises in both cases—youneed an application-specific strategy so you can reorganize the librarydespite not wanting to block out all sorts of borrowing. Once you’ve donethe hard thinking about how you wish to do it, now you’ve got to expressthat. What is the medium in which to express it? STM is a clear win. It’s justmuch better than locks and condition variables for expressing concurrentprograms.

Seibel: What if I don’t even want to allow for the possibility that someonecomes in and looks for the 21st most-requested book and gets blocked? Inthe physical world you can imagine that when someone checks out a bookwe swap in a proxy for the book that the librarian then reorganizes andwhenever a book comes back we put it back wherever the proxy is now.But you are modifying the library which seems, in an STM world, like itwould cause the librarian to have to retry his whole transaction.

Peyton Jones: But there’s something that stayed the same—the key on thebook is guaranteed not to change somehow, right? So there’s a number ofways you could do this. One is you could say, “What you do when youreplace it with a proxy is you don’t modify the library at all”—that’sunchanged. What you do is you modify the book itself. And you don’tmodify its key field—you only modify its value field, where it’s currentlyliving. Now the index can be reorganized while the book is somewhere else.That’s cool—and you can express that perfectly naturally.

With STM, at the end the librarian looks through all the memory locationsthat he has read and sees if they contain now the same values that they didwhen he read them. So the locations that he has read will include the keyfield of the book because that determined where he put it. But he hasn’tread the contents of the book. So he’ll say, “Ah, this book—does this keyfield still contain 73; oh, yes it does.”

But I don’t want to minimize the problem of starvation because it’s a bitinsidious. You need good profiling tools that point you at transactions thatare failing to commit because they keep getting bumped so that, rather thanthe program just silently not doing very much, you get some feedback aboutit. The same is true of a lock-based program. I hate it when thosehourglasses appear.

Seibel: I guess in locked-based programs we’ve just learned to try holdlocks for as short a duration as possible since that will give us the leastcontention.

Peyton Jones: Right. But, of course, then it’s harder to program. Finergrainedlocking is tricky to get right. I think this is one of the huge wins ofSTM, is it gives you the fine granularity of very fine-grained locking alongwith very simple reasoning principles.

Here’s a reasoning principle that STM gives you that locks absolutely do not.I’ll establish my top-level invariants—I’ve got a bunch of bank accounts, thetotal sum of money in all the bank accounts added together is N. Moneymoves between bank accounts—that’s all. So there’s my invariant. Anytransaction assumes that invariant at the beginning and restores it at theend. How do you reason that it does? We look at any one transaction thatsays, “Take three out of that one and put three into that one.” Good,invariant maintained. How is my reasoning in that done? Purely sequentialreasoning. Once I’ve described some top-level invariants, I can reasoncompletely sequentially about each transaction separately.