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

S , s : State L = L if f = com else < >
L , l : seq Action f = f if f ≠ com else nil
F , f : {nil, run*, commit}

Name	Guard		Effect
begin and do as before
flush	f = run		copy some of l to L
commit	f = run, L = l		F := f := commit
apply(a)	f = commit, "		"
cleanLog	head(L) in S or f = nil		L := tail(L)
cleanup	L = < >		F := f := nil
crash		l := < > if F = nil else L; s := S + l, f := F

Distributed State and Log

S_i , s_i : State f = run if all f_i = run
L_i , l_i : seq Action com if any f_i = com
F_i , f_i : {nil, run*, commit} and any L_i ≠ < >
S, L, F are the products of the S_i, L_i, F_i nil otherwise

Name	Guard		Effect
begin and do as before
flushi	fi = run		copy some of li to Li
preparei	fi = run, Li=li		Fi := run
commit	f = run, L = l		some Fi :=fi :=commit
cleanLog and cleanup as before
crashi		li := < >if Fi = nil else Li; si := Si + li, fi := Fi

High Availability

The F = commit is a possible single point of failure.

With the usual two-phase commit (2PC) this is indeed a limitation on availability.

If data is replicated, an unreplicated commit is a weakness.

Deal with this by using a highly available consensus algorithm for F.

Lamport’s Paxos algorithm is the best currently known.

Transactions: Summary

Ideas

Logs

Commit records

Stable writes at critical points: prepare and commit

Lazy cleanup

The spec is simple.

Implementations are subtle because of crashes.

The abstraction functions reveal their secrets.

The subtlety can be added one step at a time.

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)

Security: The Access Control Model

Guards control access to valued resources.

Rules control the operations allowed
for each principal and object.

Principal may do	Operation on	Object
Taylor	Read	File “Raises”
Jones	Pay invoice 4325	Account Q34
Schwarzkopf	Fire three rounds	Bow gun

A Distributed System

Principals

Authentication: Who sent a message?

Authorization: Who is trusted?

Principal — abstraction of "who":

People Lampson, Taylor

Machines VaxSN12648, Jumbo

Services SRC-NFS, X-server

Groups SRC, DEC-Employees

Channels Key #7438

Theory of Principals

Principal says statement

P says s

Lampson says “read /SRC/Lampson/foo”

SRC-CA says “Lampson’s key is #7438”

Principal A speaks for B

A => B

If A says something, B says it too. So A is stronger than B.

A secure channel:

says things directly

C says s

If P is the only sender on C

C => P

Examples

Lampson => SRC

Key #7438 => Lampson

Handing Off Authority

Handoff rule:

If A says B => A then B => A

Reasonable if A is competent and accessible.

Examples:

SRC says Lampson => SRC

Node key says Channel key => Node key

Any problem in computer science can be solved
with another level of indirection. (Wheeler).

Authenticating to the Server

Access Control

Checking access:

Given a request Q says read O
an ACL P may read O

Check that Q speaks for P

Q => P

Auditing

Each step is justified by

a signed statement, or

a rule

Authenticating a Channel

Authentication — who can send on a channel.

C => P; C is the channel, P the sender.

To get new C => P facts, must trust some principal,
a certification authority, to tell them to you.

Simplest: trust K_ca to authenticate any name:

K_ca => Anybody

Then CA can authenticate channels:

K_ca says K_ws => WS
K_ca says K_bwl => bwl

Authenticated Channels: Example

Groups and Group Credentials

Defining groups: A group is a principal; its members speak for it.

Lampson => SRC

Taylor => SRC

. . .

Proving group membership: Use certificates.

K_src says Lampson => SRC
K_ca says K_src => SRC

Authenticating a Group

Security: Summary

Ideas

Principals

Channels as principals

“Speaks for” relation

Handoff of authority

Give precise rules.

Apply them to cover many cases.

References

Hints Lampson, Hints for Computer System Design. ieee Software, Jan. 1984.

Specifications Lamport, A simple approach to specifying concurrent systems. Communications of the acm, Jan. 1989.

Reliable messages in Mullender, ed., Distributed Systems, Addison-Wesley, 1993 (summer)

Transactions Gray and Reuter, Transaction Processing: Concepts and Techniques. Morgan Kaufman, 1993.

Security Lampson, Abadi, Burrows, and Wobber, Authentication in distributed systems: Theory and practice. acm Transactions on Computer Systems, Nov. 1992.

Collaborators

Charles Simonyi Bravo: WYSIWYG editor

Bob Sproull Alto operating system
Dover: laser printer
Interpress: page description language

Mel Pirtle 940 project, Berkeley Computer Corp.

Peter Deutsch 940 operating system
QSPL: system programming language

Chuck Geschke Mesa: system programming language
Jim Mitchell
Ed Satterthwaite

Jim Horning Euclid: verifiable programming language

Ron Rider Ears: laser printer
Gary Starkweather

Severo Ornstein Dover: laser printer

Collaborators

Roy Levin Wildflower: Star workstation prototype
Vesta: software configuration

Andrew Birrell, Roger Needham, Mike Schroeder
Global name service and authentication

Eric Schmidt System models: software configuration

Rod Burstall Pebble: polymorphic typed language