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
rec
r

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 (lasts = nil or lasts Î gr)
< >        otherwise

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

 

 

q

old-q + cur-q

status

?              if cur-q ≠ < >                                                   

OK          if lasts = lastrnil                                            

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

news/r, lasts/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

 

Si    , si   : State                                              f  = run  if all fi = run
L
i   , li    : seq Action                                           com if      any fi = com
Fi , fi    : {nil, run*, commit}                                          and any Li ≠ < >
S, L,
F are the products of the Si, Li, Fi                         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;
s
i := 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 Kca  to authenticate any name:

Kca => Anybody

Then CA can authenticate channels:

Kca   says Kws       => WS
K
ca   says Kbwl       => 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.

Ksrc says Lampson => SRC
K
ca  says Ksrc         => 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