COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "setup.csr[bib,csr]" source file
C00003 00003	%3CSL TR-189:%1
C00008 00004	%3CSL TR-190:%1
C00013 00005	%3CSL TR-192:%1
C00015 00006	.next page <<CSL order form>>
C00019 ENDMK
C⊗;
.require "setup.csr[bib,csr]" source file;
.font A "math55";
.begin center;select 3
Stanford University 
Computer Systems Laboratory Reports
.end

@%1Listed here are abstracts of the most recent reports published by the
Computer Science Laboratory at Stanford University.  These reports are
available by writing directly to Naomi Schulman, Computer Systems Laboratory,
ERL-234, Stanford University, Stanford, California 94305.

%3CSL TR-189:%1
.once preface 0
@%2Center-Bases Broadcasting%1 by
David W. Wall and Susan S. Owicki (25 pages, June 1980)

@We consider the problem of routing broadcast messages in a
loosely-coupled store-and-forward network like the ARPANET.  Dalal
discussed a solution to this problem that minimizes the cost of
a broadcast; in contrast, we are interested in performing broadcast
with small delay.  Existing algorithms can minimize the delay
but seem unsuitable for use in a distributed environment because they
involve a high degree of overhead in the form of redundant messages
or data-structure space.  We propose the schemes of center-based
forwarding: the routing of all broadcasts via the shortest-path
tree for some selected node called the center.  These
algorithms have small delay and also are easy to implement in a
distributed system.

@To evaluate center-based forwarding, we define four measures of
the delay associated with a given broadcast mechanism, and then propose
three ways of selecting a center node.  For each of the three forms of
center-based forwarding we compare the delay to the minimum delay for
any broadcasting mechanism and also to the minimum delay for any single
tree.  In most cases, a given measure of the delay on the centered tree
is bounded by a small constant factor relative to either of these two
minimum delays.  When it is possible, we give a tight bound on the
ratio between the center-based delay and the minimum delay; otherwise we
demonstrate that no bound is possible.  These results give corollary
bounds on how bad the three centered trees can be with respect to each
other; most of these bounds are immediately tight, and the rest are
replaced by better bounds that are also shown to be tight.

%3CSL TR-190:%1
.once preface 0
@%2Mechanisms for Broadcast and Selective Broadcast%1 by
David W. Wall (112 pages, June 1980)

@This thesis deals with a problem in the effective use of a
loosely-coupled store-and-forward network like the ARPANET.  Many
applications assume the existence of a mechanism to send a broadcast
message to every node in the network, or a selective broadcast message
to a specified group of nodes.  Previous work in this field has resulted
in several techniques for broadcasting to the entire network.  These
include an algorithm for imposing a minimum spanning tree on the network
and maintaining it in the face of failures and changing costs, so that a
broadcast can be routed along the branches of the MST at a minimum cost
to the network as a whole.

@We extend this work in two directions.  First of all, we discuss
ways of adapting existing broadcast mechanisms to the more general
problem of selective broadcast.  In one case this involves generalizing
the MST problem to the problem of finding a minimum Steiner tree, a
problem which is NP-complete.  we examine an existing approximation
algorithm and show how to modify it for use in a distributed
environment.  In the process we show that if we make a reasonable
assumption about the way ties between edges are broken then we can
considerably simplify this algorithm.

@Second, we propose an original broadcasting technique that
forwards along the branches of a single tree in the same manner as the
MST-based algorithm.  The tree used is a shortest-path tree for a
particular node that is, in some sense, ``in the center'' of the
network; hence this method is called center-based forwarding.  Using
such a tree allows us to provide a broadcast facility with a small delay
rather than a small cost; unfortunately it is impossible in general to
minimize the delay from every source if we use only a single tree.

@To evaluate center-based forwarding, we define four measures of
the delay associated with a given broadcast mechanism, and then propose
three ways of selecting a center node.  For each of the three forms of
center-based forwarding we compare the delay to the minimum delay for
any broadcasting mechanism and also to the minimum delay for any single
tree.  In most cases, a given measure of the delay on the centered tree
is bounded by a small constant factor multiplied by either of these two
minimum delays.  When it is possible, we give a tight bound on the
ratio between the center-based delay and the minimum delay; otherwise we
demonstrate that no bound is possible.  These results immediately imply
bounds on how bad the three centered trees can be with respect to each
other; most of these bounds are immediately tight, and the rest are
replaced by better bounds that are also shown to be tight.

%3CSL TR-192:%1
.once preface 0
@%2Verifying Network Protocols Using Temporal Logic%1 
by Brent T. Hailpern and Susan S. Owicki (June 1980)

@Programs that implement computer communications protocols can exhibit extremely
complicated behavior, and neither informal reasoning nor testing is reliable
enough to establish their correctness.  In this paper we discuss the application
of program verification techniques to protocols.  This approach is more reliable
than informal reasoning, but has the advantage over formal reasoning based on
finite-state models that the complexity of the proof does not grow unmanageably
as the size of the program increases.  Certain tools of concurrent program
verification that are especially useful for protocols are presented:  history
variables that record sequences of input and output values, temporal logic for
expressing properties that must hold in a future system state (such as eventual
receipt of a message), and module specification and composition rules.  The use
of these techniques is illustrated by verifying a simple data transfer protocol
from the literature.

.next page <<CSL order form>>
.once center
%3CSL REPORT ORDER FORM%1

@To order reports, 
complete and return this form 
to the Stanford Department of Computer
Systems Laboratory.  To return this form to us; simply fold it so that the Lab's
address shows, staple, affix the
appropriate postage and mail.
Please do %2not%1 send any money with your order.  Wait until you receive an
invoice (which will be enclosed with the reports when they are sent).
.skip
.begin nofill
Name:

Address:

City:

State:									Zip Code:

Country:
.end

.once center
Check off the reports you want.
.begin bf
.tabs 3,8,28,43,46,50,70
\\Hardcopy\\\\Microfiche
.skip
|B\1.\CSL TR-189\$    \|B\2.\CSL TR-189\FREE
|B\3.\CSL TR-190\$    \|B\4.\CSL TR-190\FREE
|B\5.\CSL TR-192\$    \|B\6.\CSL TR-192\FREE
|B\7.\CSL       \$    \|B\8.\CSL       \FREE
|B\9.\CSL       \$    \|B\A.\CSL       \FREE
.end
.skip