PSP Group at UT Austin

This is the home page for the PSP group in the Department of Computer Sciences at The University of Texas at Austin. PSP stands for Programs, Specifications and Proofs. The emphasis of the work of our group is to derive parallel and distributed programs in a rigorous manner. The group is supervised by Jayadev Misra, who developed the theories we work on. The research areas are: UNITY, Powerlists and Seuss.

Current and former members of the group include:

Publications

Below we summarize the areas we work in; wherever possible we give links to papers that are available electronically.

UNITY

UNITY is a programming notation and a logic to reason about parallel and distributed programs. UNITY is presented in the book: J. Misra and K. M. Chandy, Parallel Program Design: A Foundation, Addison-Wesley, 1988.

The notes on UNITY is a series of papers presenting various results about UNITY and its applications. The notes assumes a basic understanding of the UNITY theory as presented in Chandy and Misra's book.

Since the publication of the book several improvements have been made in the theory, some of which are reflected in the notes on UNITY, Jayadev Misra has written a manuscript for a book that presents the New UNITY, this includes the introduction of a new temporal operator co for specifying safety.

 See further UNITY references for references to other papers and implementations.

 Markus Kaltenbach has written a symbolic model checker for finite state UNITY programs, called the UNITY Verifier (UV). He also extended the UNITY theory in such a way that design knowledge can be used to speed up mechanical proofs of progress properties. For more details see his dissertation

Al Carruth has extended the UNITY logic to include real time aspects of computing and hybrid systems.

Powerlists

Powerlists is a notation for describing synchronous parallel programs and circuits. The data structure is a list of length equal to a power of two, with two different operations for balanced divisions of lists. Many parallel algorithms have a succinct presentation and simple proofs in the powerlist notation. Jayadev Misra's paper Powerlists: A Structure for Parallel Recursion presents the notation and gives numerous examples of algorithms and proofs of their correctness, including the Fast Fourier Transform and Batcher's sorting network.

 Will Adams has studied how different arithmetic circuits, such as adders and multipliers, can be specified and proved correct in the powerlist notation. His paper Verifying adder circuits using powerlists is available.

 Jacob Kornerup has studied how powerlist programs can be mapped efficiently to different parallel architectures, specially hypercubes. He has also studied different sorting algorithms and extended the theory to lists of arbitrary (positive) length lists, called Parlists. See his List of papers for details about this research.

Seuss

Seuss is an offspring of the work on UNITY. It addresses the issue of program composition, by restricting how program components interact with each other. For an introduction to Seuss, read Overview of Seuss. The book A Discipline of Multiprogramming by Jayadev Misra (Springer-Verlag, 2001) treats the topics in detail. A few chapters from the book are here. A compiler for Seuss that generates C++ code and PVM calls for message communicating networks is described in Ingolf Krüger's M.S. thesis An experiment in compiler design for a concurrent object-based programming language. Recent implementation work has focused on implementing Seuss using the Java virtual machine.  This work involved adapting the Seuss notation for Java programmers; a description of the resulting language, called Seuss for Java, is available. Most of this language was implemented by Raymond Tse; details of his implementation are also available.
 
It is currently maintained by Rajeev Joshi.