From: IN%"peter@Nexus.YorkU.CA" "Peter Roosen-Runge" 30-SEP-1989 02:03:56.52 To: cs100006@YUSol CC: Subj: Return-path: peter@Nexus.YorkU.CA Sat, 30 Sep 89 02:03 EDT Received: from YUOrion by VM1.YORKU.CA (Mailer R2.02A) with BSMTP id 0181; Sat, 30 Sep 89 02:00:46 EDT Received: from nexus.yorku.ca by Orion.YorkU.CA; Sat, 30 Sep 89 02:02 EDT Date: Sat, 30 Sep 89 01:55:16 EDT From: Peter Roosen-Runge To: cs100006@YUSol Path: yunexus!utzoo!attcan!utgpu!jarvis.csri.toronto.edu!mailrus!tut.cis.ohio-st ate.edu!ucbvax!smu.UUCP!leff From: leff@smu.UUCP (Laurence Leff) Newsgroups: comp.doc.techreports Subject: tr-input/ut88.89 Message-ID: <8909290057.AA06616@smu.edu> Date: 29 Sep 89 00:57:33 GMT Article-I.D.: smu.8909290057.AA06616 Posted: Thu Sep 28 20:57:33 1989 Sender: daemon@ucbvax.BERKELEY.EDU Organization: The Internet Lines: 333 Approved: trlist@smu.edu 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.