Theses & Reports

---

Instructions for submitting a technical report or thesis.

You can find technical reports published prior to 1990 archived here.

• Ph.D. Thesis 1982 Decision Algorithms for a Class of Set-Theoretic Formulae Involving One Occurrence of the Union-Set Operator Breban, Michael Abstract | PDF

  Title: Decision Algorithms for a Class of Set-Theoretic Formulae Involving One Occurrence of the Union-Set Operator

  Candidate: Breban, Michael

  Advisor(s): Schwartz, Jacob T.

  Abstract:

  We consider the first order language allowing the operators = (equality), (epsilon) (membership), (UNION) (binary union), (INTERSECT) (binary intersection), (FDIAG) (set difference), { } (singleton former) and one occurrence of Un (unary union). We show that unquantified formulae of this language are decidable. As a preparatory result we show that unquantified formulae of the above mentioned language not involving the singleton former are decidable.

• Ph.D. Thesis 1982 The Role of the High Level Specification in Programming by Transformation: Specification and Transformation by Parts Merritt, Susan Mary Abstract | PDF

  Title: The Role of the High Level Specification in Programming by Transformation: Specification and Transformation by Parts

  Candidate: Merritt, Susan Mary

  Abstract:

  Specification by parts is a technique for constructing a very high level specification of a problem. The specification is then the target of transformation by parts, a global transformation strategy, which yields a family of high level algorithms which are correct and which solve the problem. The specifications are easy to construct, to understand and to modify. The key to the specification by parts technique is the use of weak parts. Output conditions are factored into conjunctions of weaker conditions, called weak parts, each of which is easier to satisfy than the original condition. In the transformation by parts, an initial guess is made for the output object. The guess satisfies some subset of the weak parts; the conditions in this subset are called the invariant conditions. A general iterative structure is built, which incrementally changes the initial guess, keeping the invariant conditions true, and converging to the remaining conditions. The methodology demonstrates the relationship between invariance and convergence in algorithm construction. In particular it demonstrates that algorithms for the same problem are often the result of different choices of invariant and convergent conditions. The methods are illustrated in three case studies and in three supplementary examples (which are smaller in scope than the case studies), all of which are fundamental computer science problems. These applications demonstrate the flexibility and ease with which the high level specifications can be constructed and transformed. They also demonstrate the potential which this methodology offers for the discovery of new algorithms, the illustration of connections among known algorithms, and the possible semi-automation or automation of algorithm construction.

• Ph.D. Thesis 1982 Software Structures for Ultraparallel Computing Rudolph, Lawrence S. Abstract | PDF

  Title: Software Structures for Ultraparallel Computing

  Candidate: Rudolph, Lawrence S.

  Advisor(s): Gottlieb, Allan; Schwartz, Jacob T.

  Abstract:

  In this thesis we implement several basic parallel processing primitives by using a replace-add operation, which can supersede the standard test and set, and which appears to be a universal primitive for efficiently coordinating large numbers of independently acting sequential processors. The replace-add is essentially an indivisible add-to-memory operation although concurrent replace-adds can all be processed in the same one cycle. In particular, we use the replace-add to develop routines for concurrent access to a queue and show how they can be used to devise many highly parallel algorithms as well as a distributed, concurrent task scheduler. The paracomputer forms our underlying theoretical model of parallel computation although we also consider a realistic architecture approximating this model. We justify our use of the replace-add operation by presenting a hardware implementation that permits multiple replace-adds to be processed nearly as efficiently as loads and stores. Moreover, the crucial special case of concurrent replace-adds updating the same variable is handled particularly well: If every PE simultaneously addresses a replace-add at the same variable, all these requests are satisfied in the time required to process just one request.