leff@DEPT.CSCI.UNT.EDU ("Dr. Laurence L. Leff") (04/08/90)
TRLIST is now back on the air. Thanks for your patience. If you all
get this, five more items are on their way.
DEPARTMENT OF COMPUTER SCIENCES
TECHNICAL REPORT CENTER
TAYLOR HALL 2.124
THE UNIVERSITY OF TEXAS AT AUSTIN
AUSTIN, TEXAS 78712-1188
(512) 471-9595
ELECTRONIC MAIL ADDRESS: trcenter@cs.utexas.edu
TECHNICAL REPORTS, SEPTEMBER 1989 - DECEMBER 1989
PREPAYMENT IS REQUIRED.
Please make U.S. bank checks or international money orders payable to:
"The University of Texas."
[] TR-88-21 (Revision) $2.50
[] TR-88-41 (Revision) $1.50
[] TR-89-24 $1.50 [] TR-89-32 $3.00
[] TR-89-25 $1.50 [] TR-89-33 $1.50
[] TR-89-26 $2.00 [] TR-89-34 $1.50
[] TR-89-27 $1.50 [] TR-89-35 $5.00
[] TR-89-28 $1.50 [] TR-89-36 $1.50
[] TR-89-29 $1.50 [] TR-89-37 $2.00
[] TR-89-30 $1.50 [] TR-89-38 $5.00
[] TR-89-31 $2.00 [] TR-89-39 $1.50
___________________________________________________________________________
TR-88-21 A RELATIONAL NOTATION FOR STATE TRANSITION SYSTEMS
Simon S. Lam and A. Udaya Shankar
August 1989 (Revision)
42 pages
ABSTRACT: The relational notation has two basic constructs:
state formulas that represent sets of states, and event formu-
las that represent sets of state transitions. A relational
specification consists of a state transition system, given in
the relational notation, and a set of fairness assumptions.
Several refinement relations between specifications are
defined. To illustrate our concepts and methods, three specifi-
cations of the alternating-bit protocol are given. We also
apply the theory to explain `auxiliary variables.' Other appli-
cations of the theory to protocol verification, composition,
and conversion are discussed. Our approach is compared with the
approaches of other authors.
Keywords: Specification, protocols, distributed systems, tem-
poral logic, refinement, projection, auxiliary variables.
TR-88-41 DELIVERY AND DISCRIMINATION: THE SEINE PROTOCOL
M. G. Gouda, N. F. Maxemchuk, U. Mukherji, and K. Sabnani
December 1989 (Revision)
17 pages
ABSTRACT: We present a family of protocols for data transmis-
sion from multiple identical senders to a single receiver. At
each instant, every sender sends one bit, and the sent bits are
or-ed together into one bit before being received by the
receiver. If a sender has a data message to send, it sends the
message bits one by one; otherwise it sends zero bits.
Clearly, if the sending of two messages by two senders overlap
in time, then the resulting ``collision'' can cause the
receiver to receive a corrupted message, i.e., one that was not
sent by either sender. The function of the protocol is to
allow the receiver to detect and deliver those and only those
messages that are not corrupted by collision. (In other words,
the receiver acts as a discriminating seine that catches and
delivers only uncorrupted messages; hence the title.) The
seine protocol has been implemented in a class of fiber-optic
local area networks.
Keywords: Balanced coding, communication protocol, collision,
local area network, protocol verification.
TR-89-24 LOG-DRIVEN BACKUPS: A RECOVERY SCHEME FOR LARGE MEMORY DATABASE
SYSTEMS
Eliezer Levy and Abraham Silberschatz
September 1989
24 pages
ABSTRACT: A new recovery scheme for main memory databases sys-
tems (MMDBS) is presented. The scheme is both practical and
unique compared to other proposals in this area, since it is
geared to accommodate databases that are not entirely memory-
resident, and that use standard concurrency control mechanisms.
It is assumed that a substantial portion of the database is
memory-resident, and that the absent portion is accessed less
frequently. Thus, the scheme capitalizes on the performance
advantages offered by MMDBS, without precluding the possibility
of having some portions of the database on secondary storage.
The heart of the scheme is a novel and innovative approach to
recovery processing in MMDBS, that eliminates expensive check-
pointing activity. The advanced I/O technology of disk arrays
is incorporated for the implementation of the approach.
Keywords: Main memory databases, transaction recovery, logging,
disk I/O.
TR-89-25 COMPOSITE REGISTERS
James H. Anderson
September 1989
24 pages
ABSTRACT: We introduce a shared data object, called a composite
register, that generalizes the notion of an atomic register. A
composite register is an array-like variable that is parti-
tioned into a number of components. An atomic operation of
such a register either writes a value to one of the components,
or reads the values of all components. A composite register
reduces to an ordinary atomic register when there is only one
component. We show that atomic registers can be used to imple-
ment a composite register in which there is only one writer per
component. (In a related paper, we show how to use the compo-
site register construction of this paper to implement a compo-
site register in which multiple writers per component are
allowed.) Composite registers are quite powerful and can be
used to implement a number of interesting shared data objects.
For example, a composite register can be used to implement a
shared variable whose value can either be read or incremented
in one atomic operation.
Keywords: Atomicity, atomic register, concurrency, interleaving
semantics, linearizability, shared variable. CR Categories:
D.4.1, D.4.2, F.3.1
TR-89-26 MULTIPLE-WRITER COMPOSITE REGISTERS
James H. Anderson
September 1989
36 pages
ABSTRACT: A composite register is an array-like variable that
is partitioned into a number of components. An atomic opera-
tion of such a register either writes a value to one of the
components, or reads the values of all components. A composite
register reduces to an ordinary atomic register when there is
only one component. In a related paper, we showed that atomic
registers can be used to implement a composite register in
which there is only one writer per component. In this paper,
we show that a composite register with multiple writers per
component can be implemented from a composite register with one
writer per component. Together, these two constructions show
that composite registers can be implemented from atomic regis-
ters.
Keywords: Atomicity, atomic register, concurrency, interleaving
semantics, linearizability, shared variable. CR Categories:
D.4.1, D.4.2, F.3.1
TR-89-27 A MECHANICALLY DERIVED SYSTOLIC IMPLEMENTATION OF PYRAMID
INITIALIZATION
Christian Lengauer, Bikash Sabata, and Farshid Arman
September 1989
16 pages
ABSTRACT: Pyramidal algorithms manipulate hierarchical
representations of data and are used in many image processing
applications, for example, image segmentation and border
extraction. We present a systolic network which performs the
first phase of pyramidal algorithms: initialization. The
derivation of the systolic solution is governed by a mechanical
method whose input is a known Pascal-like pyramidal algorithm.
After a few manual program transformations that prepare the
algorithm for the method, parallelism is infused mechanically.
A processor layout is selected, and the channel connections
follow immediately.
Keywords: Pyramid Initialization, Pyramid Node Linking, Sys-
tolic Array, Systolic Design Method.
TR-89-28 A COMBINATION OF RITT-WU'S METHOD AND COLLINS' METHOD
Shang-Ching Chou, Xiao-Shan Gao, and Nicholas McPhee
October 1989
21 pages
ABSTRACT: We propose a method for the decision problem in real
closed fields. The method is a combination of the Tarski-
Seidenberg-Collins (TSC) method and the Ritt-Wu method. To
decide whether a system of polynomial equations and inequations
has common zeros (solutions) in a real closed field, we first
apply Ritt-Wu's decomposition method to delete those components
that do not have common zeros in an algebraically closed field.
Then we apply the TSC method to the remaining components to
complete the solution. Many non-trivial examples have been
solved by this method, including the 8 configuration problem.
3
Keywords: Mechanical geometry theorem proving, Tarski-
Seidenberg-Collins' method, Ritt-Wu's method, Algebraically
closed field, Real closed field, Axioms of geometry, Axioms of
order, Unordered metric geometry, Euclidean geometry, the 8
3
configuration problem.
TR-89-29 ADAPTIVE PROGRAMMING
Mohamed G. Gouda and Ted Herman
October 1989
24 pages
ABSTRACT: An adaptive program is one that changes its behavior
based on the current state of its environment. The environment
state is assumed to go through successive periods of change and
stability, and the adaptive program is only required to perform
its intended function during periods of stability. In this
paper, this notion of adaptivity is formalized and a logic for
reasoning about adaptive programs is presented. The logic
includes several composition operators that can be used to
define an adaptive program in terms of given constituent pro-
grams; programs resulting from these compositions retain all
the adaptive properties of their constituent programs.
Keywords: Adaptivity, distributed computing, self-
stabilization.
TR-89-30 PARALLELIZING TRANSFORMATIONS FOR A CONCURRENT RULE EXECUTION
LANGUAGE
Daniel P. Miranker, Chin-Ming Kuo, and James C. Browne
October 1989
14 pages
ABSTRACT: Most work on parallelizing forward-chaining produc-
tion system programs may be described as parallelizing sequen-
tial production system interpreters. We are now studying an
approach that parallelizes the entire execution of a production
system program. We first modify the semantics of the OPS5 pro-
duction system language into a rule language suitable for
parallel execution. We then define a compilation method that
partitions rule systems into disjoint subsets that execute
asynchronously with respect to each other and which communicate
through asynchronous message passing. Within each subset rules
may be fired in parallel. The approach is similar to the
methods used in parallelizing compilers for block structured
languages and is founded on the formalisms developed for assur-
ing the correct operation of concurrent database systems. Our
primary results to date involve the definition of the syntax
and semantics of a parallel production system language and the
development of an ensemble of optimizing transforms.
Keywords: Parallel Compilation, Production System, Rule-based
programming, parallel programming.
TR-89-31 ON THE MECHANICAL PROOF OF GEOMETRY THEOREMS INVOLVING INEQUAL-
ITIES
Shang-Ching Chou, Xiao-Shan Gao, and Dennis S. Arnon
October 1989
35 pages
ABSTRACT: In the past decade highly successful algebraic
methods for mechanical geometry theorem proving have been
developed. The first step in these methods is to assign (vari-
able) coordinates to key points, and then translate the
hypotheses and conclusion of a geometric proposition into (mul-
tivariate) polynomial equations and inequalities, Next, the
algebraic provers apply either the ``Wu-Ritt" or ``Grobner
Basis" method to analyze zeros of polynomials. To date, the
manner in which the Wu-Ritt and Grobner Basis methods have been
employed has limited the algebraic provers to propositions that
can be encoded entirely with polynomial equations, i.e.
without inequalities. In this paper we explore two techniques
for extending Wu-Ritt and Grobner provers to handle proposi-
tions involving inequalities: reduction of polynomials to
canonical form modulo a (polynomial) ideal, and the
Rabinowitsch/Seidenberg device of converting (polynomial) ine-
qualities to equations by introducing new variables. We illus-
trate the practical value of these techniques by numerous exam-
ples of their use in conjunction with a Wu-Ritt prover.
Keywords: Geometry Theorem Proving, Automated Theorem Proving,
Decision Procedures, Wu-Ritt Method, Grobner Bases, Construc-
tive Polynomial Ideal Theory, Euclidean Geometry, Computational
Algebraic Geometry, Computer Algebra, Collins Method, Cylindri-
cal Algebraic Decompositions, Definiteness of Polynomials.
TR-89-32 AN ANALYSIS OF LOOP CHECKING MECHANISMS FOR LOGIC PROGRAMS
Roland N. Bol, Krzysztof R. Apt, and Jan Willem Klop
October 1989
56 pages
ABSTRACT: We systemically study loop checking mechanisms for
logic programs by considering their soundness, completeness,
relative strength and related concepts. We introduce a natural
concept of a simple loop check and prove that no sound and com-
plete simple loop check exists, even for programs without func-
tion symbols. Then we introduce a number of sound simple loop
checks and identify natural classes of PROLOG programs without
function symbols for which they are complete. In these classes
a limited form of recursion is allowed. As a by-product we
obtain an implementation of the closed world assumption of
Reiter and a query evaluation algorithm for these classes of
logic programs.
Keywords: loop checking, termination, PROLOG, soundness, com-
pleteness, query processing.
TR-89-33 SERIALIZABLE PROGRAMS, PARALLELIZABLE ASSERTIONS: A BASIS FOR
INTERLEAVING
Mohamed G. Gouda
November 1989
6 pages
ABSTRACT: In order for interleaving to be acceptable in our
reasoning about the behaviour of a concurrent program, all the
assertions (concerning program behaviour) that arise in the
course of our reasoning should be parallelizable. This means
that if these assertions hold for the program under interleav-
ing, i.e., when its actions are executed one at a time, then
they should also hold when the actions are executed in paral-
lel. In this note, we identify a large family of concurrent
programs, called serializable programs, for which rich classes
of assertions are shown to be parallelizable. It follows that
reasoning about the behaviour of serializable programs can be
carried out under interleaving.
Keywords: Concurrent programs, formal reasoning, parallelism,
serializability.
TR-89-34 PROBABILISTIC SELF-STABILIZATION
Ted Herman
November 1989
18 pages
ABSTRACT: A probabilistic self-stabilizing algorithm for a ring
of identical processes is presented; the number of processes in
the ring is odd, the processes operate synchronously, and com-
munication is unidirectional in the ring. The normal function
of the algorithm is to circulate a single token in the ring. If
the initial state of the ring is abnormal, i.e. the number of
tokens differs from one, then execution of the algorithm
results probabilistically in convergence to a normal state with
one token.
Keywords: Distributed Computing, Probabilistic Algorithms,
Self-Stabilization, Uniform Rings.
TR-89-35 EVALUATION AND IMPLEMENTATION OF PROTOCOLS IN THE LOCAL AREA
NETWORK TESTBED ENVIRONMENT
Benjamin Lewis Barnett, III
November 1989
261 pages
ABSTRACT: This thesis presents the results of the Local Area
Network Testbed experience. The design of the testbed, the
results of several experiments and the results of a formal pro-
tocol analysis are included. Three data link layer protocols
for Carrier Sense Multiple Access with Collision Detection
(CSMA/CD) bus networks were implemented in the testbed. The
performance of these three protocols under several different
artificial workloads is compared. The three protocols were the
commercially available Ethernet, the Enet II protocol proposed
by Molloy, and the Virtual Time CSMA/CD (VTCSMA/CD) protocol
proposed by Molle. The three protocols represent three funda-
mentally different approaches to handling collisions among
users of a broadcast channel. Ethernet randomizes retransmis-
sion attempts for the conflicting packets in an attempt to
minimize the likelihood of successive collisions. Enet II uses
a probabilistic algorithm to schedule the retransmissions of
conflicting packets to resolve the collision. VTCSMA/CD uses a
technique which reduces the initial likelihood of collisions.
Enet II is shown to have significantly better variance of delay
than Ethernet. VTCSMA/CD has the best variance of delay of the
three protocols due to the success of its collision avoidance
method.
The implementation of Enet II demonstrates that techniques usu-
ally reserved for slotted networks can be beneficially employed
on their unslotted counterparts. To investigate the adaptation
of slotted protocols to unslotted use, a well known slotted
Collision Resolution Protocol (CRP), the Gallager First-Come,
First-Served (FCFS) protocol, is adapted to unslotted operation
and proven to have bounded delay. A second adaptation of the
protocol which responds to collisions differently is shown to
deadlock. Deadlock detection and recovery methods are
presented. A new CRP based on the deadlock recovery method and
using information about the location of colliding stations is
proposed.
Keywords: Broadcast Bus Protocols, Protocol performance meas-
urement, Protocol Verification.
TR-89-36 USING TRANSFORMATIONS TO VERIFY PARALLEL PROGRAMS
Ernst-Rudiger Olderog and Krzysztof R. Apt
November 1989
27 pages
ABSTRACT: We argue that the verification of parallel programs
can be considerably simplified by using program transforma-
tions. We illustrate this approach by proving correctness of
two parallel programs under the assumption of fairness: asyn-
chronous fixed point computation and parallel zero search
Keywords: Program transformations, fairness, verification.
TR-89-37 A CLASS OF GEOMETRY STATEMENTS OF CONSTRUCTIVE TYPE AND
GEOMETRY THEOREM PROVING
Shang-Ching Chou and Xiao-Shan Gao
November 1989
32 pages
ABSTRACT: This paper is a technical extension of our previous
work not published fully. It describes how to generate non-
degenerate conditions in geometric form for a class of geometry
statements of constructive type, called Class C, using Wu's
method. We reemphasize a mathematical theorem found by us stat-
ing that in the irreducible case, the non-degenerate conditions
generated by our method are sufficient for a geometry statement
in Class C to be valid in metric geometry. We prove a new
theorem: if an irreducible statement in Class C is confirmed to
be generally true, then that statement is valid under the
geometric non-degenerate conditions generated by our method. As
a direct consequence, most of the geometry theorems proved (to
be generally true) by our technique based on the Grobner basis
method are valid under those geometric non-degenerate condi-
tions. We also find subclasses of Class C and prove a theorem
that the non-degenerate conditions generated by our method are
sufficient for a statement in those subclasses to be valid in
Euclidean geometry.
Keywords: Geometry theorem proving, Wu's method, the Grobner
basis method, non-degenerate condition, generally true, con-
structive geometry statement, Euclidean geometry, metric
geometry, Minkowskian geometry, algebraically closed field,
Simson]s theorem, the Butterfly theorem.
TR-89-38 EFFICIENT PORTABLE PARALLEL MATRIX COMPUTATIONS
James Walter Juszczak
December 1989
87 pages
ABSTRACT: In this thesis we exercise a method of developing
parallel algorithms for matrix computations that facilitates
efficient and portable implementations. The method includes
defining a set of communication primitives, selecting a storage
scheme, embedding a logical communications topology in the phy-
sical architecture, and synchronizing data flow and computa-
tions to reduce the overhead of communications. Several algo-
rithms are implemented using the column wrapped storage scheme
and communication primitives which are independent of the
underlying parallel architecture. Theoretical and experimental
results are presented.
Keywords: Matrix algorithms, parallel processing, multicomput-
ers, MIMD.
TR-89-39 INVESTIGATING SKEW AND SCALABILITY IN PARALLEL JOINS
Christopher B. Walton
December 1989
30 pages
ABSTRACT: This research will improve understanding of the
interaction between data skew and scalability in parallel join
algorithms. Previous work in this area assumes that data are
uniformly distributed, but data skew is widespread in existing
databases. This research makes three major contributions:
1. Several distinct types of skew are identified. Previous
work treats skew as a homogeneous phenomenon, but simple
analytic analysis shows that each type of skew has a dif-
ferent effect on response time.
2. The relative partition model of skew is defined. It is a
simple analytic model that allows worst-case analysis of
each type of data skew. The use of this model is demon-
strated in an analysis of the sort-merge join algorithm.
3. A systematic plan for investigating skew and scalability.
The interplay between simple analytic models and detailed
simulations is vital: Analytic models bound the results
expected from simulation, while more detailed simulation
results validate the analytic models.
Keywords: skew, scalability, joins, performance, parallelism,
database, multicomputers.