leff@smu.UUCP (Laurence Leff) (09/29/89)
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, MAY 1989 - AUGUST 1989
PREPAYMENT IS REQUIRED.
Please make U.S. bank checks or international money orders payable to:
"The University of Texas."
[] TR-88-30 (Revision) $2.00
[] TR-89-12 $1.50 [] TR-89-18 $1.50
[] TR-89-13 $1.50 [] TR-89-19 $1.50
[] TR-89-14 $1.50 [] TR-89-20 $1.50
[] TR-89-15 $1.50 [] TR-89-21 $1.50
[] TR-89-16 $1.50 [] TR-89-22 $5.00
[] TR-89-17 $2.00 [] TR-89-23 $2.50
---------------------------------------------------------------------------
TR-88-30 SPECIFYING IMPLEMENTATIONS TO SATISFY INTERFACES: A STATE TRAN-
SITION SYSTEM APPROACH
Simon S. Lam and A. Udaya Shankar
June 1989 (Revision)
37 pages
ABSTRACT: We present a formalism to specify interfaces and
implementations of program modules in a hierarchy. Our formal-
ism is based upon the relational notation for specifying state
transition systems and a refinement relation between such
specifications. We define what it means for a program module to
offer an upper interface to a user, and to use a lower inter-
face offered by another program module. We then solve the prob-
lem posed by Leslie Lamport to participants of the Specifica-
tion Logics session of the 1987 Lake Arrowhead Workshop. A for-
mal specification of a serializable database interface is first
presented. Specifications of two database implementations,
using a two-phase locking protocol and a multi-version times-
tamp protocol, are then given, together with a proof that each
implementation satisfies the interface. In the two-phase lock-
ing implementation, we assume that it uses a lower interface to
access a physical database.
Keywords: Specification, interfaces, module implementation,
safety, progress, refinement, projection mapping, program com-
position, concurrency control, serializability, two-phase lock-
ing, timestamps.
TR-89-12 OPPORTUNISTIC ALGORITHMS FOR COVERING WITH SUBSETS
Paul Pritchard
May 1989
15 pages
ABSTRACT: The main problem tackled in this paper is that of
finding each set in a given collection that has no proper sub-
set in the collection. Starting with a solution that uses a
quadratic (in the size of the collection) number of subset
tests, solutions are developed which are opportunistic in the
sense of running significantly faster for certain classes of
input (such as when most sets are small). They are based on an
opportunistic algorithm for the fundamental problem of finding
an element common to two ordered sequences. Methodological
issues are emphasized throughout.
Keywords: Opportunistic algorithms, covering with subsets, con-
junctive normal form, Welfare Crook problem, programming metho-
dology.
TR-89-13 GENERATING DOMAIN MODELS FOR PROGRAM SPECIFICATION AND GEN-
ERATION
Neil Iscoe, J. C. Browne, and John Werth
May 1989
24 pages
ABSTRACT: This paper describes a formalized domain modeling
technique which we have designed to represent relevant portions
of the domain knowledge required to specify and implement
application program generators. Successful application genera-
tors are always domain specific. Software engineering of appli-
cation generators and meta-generators must be based on a char-
acterization of domain knowledge which captures the relevant
application domain knowledge necessary for the paradigm. The
operational goal is to allow designers, who are neither com-
puter programmers nor domain experts, to construct application
programs by declaratively describing and refining specifica-
tions for the programs that they wish to construct. The focus
is on a representation technique to support the meta-level
aspects of such a system - a generator for narrow domain appli-
cation program generators. A domain model generated using this
technique is based on classes that are composed of attributes
defined in formal terms that characterize an application
domain. Unique to this technique is the integration of
domain-specific properties such as units, quantities, granular-
ity, qualitative scales, population parameters into a coherent
system of reusable attributes and classes. A system prototype,
Ozym, has been developed to experiment with domain model gen-
eration.
Keywords: Software Engineering, Domain Modeling, Program Gen-
eration, Reuse, Object-Oriented, Requirements Elicitation,
Specification Techniques.
TR-89-14 THE ELUSIVE ATOMIC REGISTER (UPDATED VERSION)
Ambuj K. Singh, James H. Anderson, and Mohamed G. Gouda
May 1989
28 pages
ABSTRACT: We present two constructions of a multiple-reader
atomic register from single-reader atomic registers. The first
is a recursive construction; a two-reader construction defines
the base step, and a scheme to construct an M-reader register
from (M-1)-reader registers defines the induction step. This
construction, although simple to understand and verify, has
exponential complexity. Our second construction is also an
extension of the above two-reader construction. This construc-
tion, while more complicated, has optimal complexity; it
requires O(M2+MN) atomic single-reader bits for an N-bit regis-
ter.
Keywords: atomicity, atomic register, interleaving semantics,
shared variable.
CR Categories: D.4.1, D.4.2, F.3.1.
TR-89-15 RANKERS: A PANACEA FOR SYNCHRONIZATION
Ambuj K. Singh and Mohamed Gouda
May 1989
25 pages
ABSTRACT: The variety of synchronization problems in the com-
puting science is immense: dining philosophers, FCFS doorway,
producer-consumer, mutual exclusion, atomic register construc-
tion etc. We develop the abstraction of rankers in order to
compare the synchronization requirements of these problems and
solve them modularly. Rankers have two mandatory properties -
responsiveness and precedence and three optional ones - acycli-
city, comparability, and stability. Adding the three optional
properties one after another we obtain a chain of four rankers.
Each ranker in this chain is best suited to solve a particular
class of synchronization problems and together, the four rank-
ers are sufficient to solve most synchronization problems in
the literature. We devise a general strategy to solve synchron-
ization problems using rankers and illustrate this strategy by
solving some of these problems. In each solution, we only use
the properties of the particular ranker chosen and not to how
the ranker is implemented, thus separating the two concerns of
what a ranker's properties are and how these properties are
achieved. Finally, we present implementations for the four
rankers mentioned above.
Keywords: concurrency, modular design, mutual exclusion, rank,
ranker, specification, synchronization, verification.
TR-89-16 LONG-DURATION TRANSACTIONS IN SOFTWARE DESIGN PROJECTS
Henry F. Korth and Gregory D. Speegle
June 1989
21 pages
ABSTRACT: Computer-assisted design applications pose many prob-
lems for database systems. Standard notions of correctness are
insufficient, but some notion of correctness is still required.
Formal transaction models have been proposed for such applica-
tions. However, the practicality of such models has not been
clearly established. In this paper, we consider an example of a
software development application and apply the NT/PV model to
show how this example could be represented as a set of database
transactions. We show that although the standard notion of
correctness (serializability) is too strict, the notion of
correctness in the NT/PV model allows sufficient concurrency
with acceptable overhead. We extrapolate from this example to
draw some conclusions regarding the potential usefulness of a
formal approach to the management of long-duration design tran-
sactions.
Keywords: Long-duration transactions, Software engineering,
Concurrency control.
TR-89-17 SCALABILITY OF PARALLEL JOINS ON HIGH PERFORMANCE MULTICOMPUT-
ERS
A. G. Dale, F. F. Haddix, R. M. Jenevein, and C. B. Walton
June 1989
39 pages
ABSTRACT: This paper focuses on parallel joins computed on a
mesh-connected multicomputer. We propose a cost-effective sort
engine and a novel algorithm that combines hashing and semi-
joins. An analytic model is used to select hardware configura-
tions for detailed evaluation and to suggest refinements to the
algorithm. Simulation of our model confirmed the analytic
results. Results indicate that parallel joins scale very well.
In some cases, synergistic effects lead to better than linear
speedup.
Keywords: scalability, parallelism, interconnection networks,
wormhole routing, hashing, semijoins, relational databases.
TR-89-18 ON THE SAFE TERMINATION OF PROLOG PROGRAMS
Krzysztof R. Apt, Roland N. Bol, and Jan Willem Klop
June 1989
16 pages
ABSTRACT: We systematically 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 a natural class of PROLOG programs for
which they are complete. In this class a limited form of recur-
sion is allowed. As a by-product we obtain an implementation of
the closed world assumption of Reiter [R] and a query evalua-
tion algorithm for a class of logic programs without function
symbols.
Keywords: deductive databases, logic programming, termination
loop checking, PROLOG interpreter.
TR-89-19 DATA-VALUE PARTITIONING AND VIRTUAL MESSAGES
Nandit Soparkar and Abraham Silberschatz
July 1989
22 pages
ABSTRACT: Network Partition failures in traditional Distributed
Databases cause severe problems for transaction processing. In
this paper, we observe that the only way to overcome the prob-
lems of `blocking' behavior for transaction processing in the
event of such failures is, effectively, to execute them at
single sites. A new approach to data representation and distri-
bution is proposed and it is shown to be suitable for failure
prone environments. We propose techniques for transaction pro-
cessing, concurrency control and recovery for the new represen-
tation. Several properties that arise as a result of these
methods, such as non-blocking behavior, independent recovery
and high availability, suggest that they could be profitably
implemented in a distributed environment.
Keywords: Distributed Databases, Transaction Processing, Fault
Tolerance, Concurrency Control.
TR-89-20 ARITHMETIC CLASSIFICATION OF PERFECT MODELS OF STRATIFIED PRO-
GRAMS
Krzysztof R. Apt and Howard A. Blair
August 1989
17 pages
ABSTRACT: We study here the recursion theoretic complexity of
the perfect (Herbrand) models of stratified logic programs. We
show that these models lie arbitrarily high in the arithmetic
hierarchy. As a byproduct we obtain a similar characterization
of the recursion theoretic complexity of the set of conse-
quences in a number of formalisms for non-monotonic reasoning.
We show that under some circumstances this complexity can be
brought down to recursiveness and recursive enumerability. To
this purpose we study a class of recursion-free programs.
Keywords: stratification, arithmetical hierarchy, recursion-
free programs, non-monotonic reasoning.
TR-89-21 MECHANICAL FORMULA DERIVATION IN ELEMENTARY GEOMETRIES
Shang-Ching Chou and Xiao-Shan Gao
August 1989
20 pages
ABSTRACT: A precise formulation for the relations among certain
variables under a set of polynomial equations and a set of
polynomial inequations (to exclude certain special cases which
cannot be excluded by the selection of parameters alone) is
given. Several methods are presented to find such relations.
The methods have been implemented and used to find geometry
formulas, to discover geometry theorems, and to find geometry
loci equations. About 120 non-trivial problems have been
solved using the methods.
Keywords: Elementary geometry, formula derivation, Grobner
bases, Ritt-Wu's method, Heron's formula, Brahmagupta's For-
mula, locus equations, Peaucellier's linkage.
TR-89-22 A COLLECTION OF 120 COMPUTER SOLVED GEOMETRY PROBLEMS IN
MECHANICAL FORMULA DERIVATION
Shang-Ching Chou and Xiao-Shan Gao
August 1989
63 pages
ABSTRACT: This is a collection of 120 geometric problems
mechanically solved by a program based on the methods intro-
duced by us. Researchers can use this collection to experiment
with their methods/programs similar to ours. It consists of two
parts: the exact specification of the input to our program and
a collection of 120 examples. A typical example consists of an
informal description of the geometric problem, the input to the
program which is the exact specification of the problem, the
result of the problem, and a diagram.
Keywords: Elementary geometry, formula derivation, Grobner
bases, Ritt-Wu's method, Heron's formula, Brahmagupta's For-
mula, locus equations, Peaucellier's linkage.
TR-89-23 FORMAL METHODS FOR PROTOCOL CONVERSION
Kenneth L. Calvert and Simon S. Lam
August 1989
44 pages
ABSTRACT: We consider ways of overcoming a protocol mismatch
using protocol conversion. Three different methods for finding
a protocol converter are described. Two of these are ``bottom-
up'' in nature, and involve relating the conversion system to
existing protocols. The third approach, which is new, is
``top-down:'' the desired global properties of the conversion
system are used in deriving the converter. An example is used
to illustrate each method. We discuss more general forms of the
abstract problem in the context of layered network architec-
tures.
Keywords: internetworking, communication protocols, protocol
mismatch, protocol converter, specification, verification, quo-
tient problem.