Principles for Computer System Design

Butler Lampson

We have learned depressingly little in the last ten years about how to build computer systems. But we have learned something about how to do the job more precisely, by writing more precise specifications, and by showing more precisely that an implementation meets its specification. Methods for doing this are of both intellectual and practical interest. I will explain the most useful such method and illustrate it with two examples:

Connection establishment: Sending a reliable message over an unreliable network.

Transactions: Making a large atomic action out of a sequence of small ones.

Principles for
Computer System Design

10 years ago: Hints for Computer System Design

Not that much learned since then—disappointing

Instead of standing on each other’s shoulders, we stand on each other’s toes. (Hamming)

One new thing: How to build systems more precisely

If you think systems are expensive, try chaos.

Collaborators

Bob Taylor

Chuck Thacker Workstations: Alto, Dorado, Firefly
Networks: AN1, AN2

Charles Simonyi Bravo wysiwyg editor

Nancy Lynch Reliable messages

Howard Sturgis Transactions

Martin Abadi Security
Mike Burrows
Morrie Gasser
Andy Goldstein
Charlie Kaufman
Ted Wobber

From Interfaces to Specifications

Make modularity precise

Divide and conquer (Roman motto)

Design

Correctness

Documentation

Do it recursively

Any idea is better when made recursive (Randell)

Refinement: One man’s implementation is another man’s spec.
(adapted from Perlis)

Composition: Use actions from one spec in another.

Specifying a System with State

A safety property: nothing bad ever happens
Defined by a state machine:

state: a set of values, usually divided into named variables

actions: named changes in the state

A liveness property: something good eventually happens

These define behavior: all the possible sequence of actions

Examples of systems with state:

Data abstractions

Concurrent systems

Distributed systems

You can’t observe the actual state of the system from outside.
All you can see is the results of actions.

Editable Formatted Text

This interface was used in the Bravo editor.
The implementation was about 20k lines of code.

How to Write a Spec

Figure out what the state is

Choose it to make the spec clear, not to match the code.

Describe the actions

What they do to the state

What they return

Helpful hints

Notation is important; it helps you to think about what’s going on.

Invent a suitable vocabulary.

Fewer actions are better. Less is more.

More non-determinism is better; it allows more implementations.

I’m sorry I wrote you such a long letter; I didn’t have time to write a short one. (Pascal)

Reliable Messages

Spec for Reliable Messages

q : sequence[M] := < >
status : {OK, lost, ?} := lost
rec_s/r : Boolean := false (short for ‘recovering’)

Name		Guard	Effect	Name	Guard	Effect
**put(m)			append m to q, status := ?	*get(m)	m first on q	remove head of q, if q = <>, status = ?
*getAck(a)	status = a		status := lost			then status := OK
lose		recs or recr	delete some element from q; if it’s the last then status := lost, or status := lost

What “Implements” Means?

Divide actions into external and internal.

Y implements X if

every external behavior of Y is an external behavior of X, and

Y’s liveness property implies X’s liveness property.

This expresses the idea that Y implements X if
you can’t tell Y apart from X by looking only at the external actions.

Proving that Y implements X

Define an abstraction function f from the state of Y to the state of X.

Show that Y simulates X:

1) f maps initial states of Y to initial states of X.

2) For each Y-action and each state y
there is a sequence of X-actions that is the same externally,
such that the diagram commutes.

This always works!

Delayed-Decision Spec: Example

The implementer wants the spec as non-deterministic as possible,
to give him more freedom and make it easier to show correctness.

A Generic Protocol G (1)

A Generic Protocol G (2)

A Generic Protocol G (3)

A Generic Protocol G (4)

G at Work

Abstraction Function for G

cur-q = <msg> if msg ≠ nil and (last_s = nil or last_s Î g_r)
< > otherwise

old-q = the messages in sr with i’s that are good and not = last_s

q	old-q + cur-q
status	? if cur-q ≠ < > OK if lasts = lastr ≠ nil lost if lasts Ï (gr È {lastr}) or lasts = nil
recs/r	recs/r

The Handshake Protocol H (1)

The Handshake Protocol H (2)

The Handshake Protocol H (3)

The Handshake Protocol H (4)

The Handshake Protocol H (5)

The Handshake Protocol H (6)

Abstraction Function for H

G	H
gs	the i’s with (js, i) in rs
gr	{ir} – {nil}
sr and rs	the (I, M) and (I, A) messages in sr and rs

new_s/r, last_s/r, and msg are the same in G and H

growr(i)	receiver sets ir to an identifier from newr
grows(i)	receiver sends (js, i)
shrinks(i)	channel rs loses the last copy of (js, i)
shrinkr(i)	receiver gets (ir, done)

An efficient program is an exercise in logical brinksmanship.
(Dijkstra)

Reliable Messages: Summary

Ideas

Identifiers on messages

Sets of good identifiers, sender’s Í receiver’s

Cleanup

The spec is simple.

Implementations are subtle because of crashes.

The abstraction functions reveal their secrets.

The subtlety can be factored in a precise way.

Atomic Actions

S : State

Name	Guard	Effect
do(a):Val		(S, val) := a(S)

A distributed system is a system in which I can’t get my work done because a computer has failed that I’ve never even heard of.
(Lamport)

Transactions: One Action at a Time

S , s : State

Name	Guard	Effect
do(a):Val		(s, val) := a(s)
commit		S := s
crash		s := S

Server Failures

S , s : State
f : {nil, run} := nil

Name	Guard	Effect
begin	f = nil	f := run
do(a):Val	f = run	(s, val) := a(s)
commit	f = run	S := s, f := nil
crash		s := S, f := nil

Note that we clean up the auxiliary state f.

Incremental State Changes: Logs (1)

S , s : State S = S + L
L , l : seq Action := < > s, f = s, f
f : {nil, run} := nil

Name	Guard	Effect
begin	f = nil	f := run
do(a):Val	f = run	(s, val) := a(s), l +:= a
commit	f = run	L := l, f := nil
. . .
crash		l := L, s := S+L, f:=nil

Incremental State Changes: Logs (2)

S , s : State S = S + L
L , l : seq Action s, f = s, f
f : {nil, run}

Name	Guard	Effect
begin, do, and commit as before
apply(a)	a = head(l)	S := S + a, l := tail(l)
cleanLog	L in S	L := < >
crash		l := L, s := S+L, f:=nil

Incremental Log Changes