CATS/Pal

1. Name:
   CATS/Pal. (The tool is called CATS, its input language is called PAL.)

2. Source:
   Purdue University

3. Brief description:
   CATS/Pal is a tool for statically analyzing concurrent programs. It is a prototype of task parcelling and composition techniques based on process algebra that will later be incorporated into the CATS tool suite. It includes:
   • An Ada-like design language (PAL)
   • An analysis tool (Pal) that
     1. translates specifications written in PAL into process graphs, and constructs a hierarchical analysis plan based on scope structure and task communication structures.
     2. performs reachability analysis and verifies correct implementations based on various notions of ``implements'' relations (bisimulations and preorders).
     3. applies abstraction and reductions automatically or under user direction during hierarchical composition of analysis results to control growth of the state-space.
     4. uses user-supplied context assumptions to further prune the state-space, as well as verifying the validity of those assumptions.
     5. can be configured as a single client/server pair (the default configuration) or as multiple servers analyzing sub-problems in parallel on a network of workstations.

4. Evaluation against applicable general dimensions:
   1. Availability: commercial/licensed/public domain
      Cost-free license. Full sources are available by anonymous ftp to
      phosphor.cs.purdue.edu, directory pub/arcadia/PAL.

   2. Cost:
      Free if obtained over the internet.

   3. Degree of support/maturity/testing/usage:
      Limited support. CATS/Pal was developed by a single graduate student, Wei Jen Yeh. The PAL language, translator, and back-end analysis engine are now fairly stable, but Pal is not a commercial-quality tool. Documentation is sparse, and the user interface is primitive. It has been successfully tested on many examples, including standard ``white rat'' problems from the literature (100 dining philosophers, Milner's scheduler, gas station, etc.) and a smaller number of more realistic problems including a model of PAL itself (in a multiple-server configuration) and portions of the Chiron user interface development system.

   4. Speed:
      An individual process composition operation is at least one order of magnitude slower in Pal than in simpler brute-force reachability analysis tools, and its capacity is similarly limited. However, analysis of much larger systems is possible when the reductions are successfully applied to limit growth of the state space. For instance, Pal requires more time to analyze 3 dining philosophers than CATS (the Ada implementation) requires for 7; but Pal analyzes 100 dining philosophers in less time (and less memory) than CATS takes to analyze 9 dining philosophers. Pal is competitive with non-enumerative analysis tools like constrained expression analysis for highly structured problems (faster on some, slower on others).

      Analysis of more realistic system designs is typically achievable if the system has a cleanly layered design; otherwise reorganization of the design (introduction of layering in the design, even if it is absent in the implementation) is necessary to achieve satisfactory results. Experience so far suggests that the structure required to make analysis feasible is also useful for understandability.

   5. Computing platforms:
      Developed and maintained on Sun Sparcstations under Sun OS 4.x with Austin/Kyoto Common Lisp version 615. Pal has been ported to System V R4 and SVR3 environments running on 80486 PC's, as well as Lucid Common Lisp version 4.0 under Sun OS. Should port to other Unix systems with Common Lisp and sockets; porting to a new operating system or Lisp compiler requires modification of a small number of interface modules for inter-process communication and invocation of system services. Performance is best with at least 24M of main memory; more is desirable.

   6. Language compatibilities:
      PAL language is based on Ada and supports most tasking constructs of Ada. Also supports modeling of data values through limited symbolic evaluation (also known as ``value flattening''). Does not support many Ada features unrelated to tasking; in particular, the 'package' construct is not supported.

   7. Footprint:
      1. Source distribution 400 kB (compressed)
      2. Full sources, binaries, and examples 48 MB

      Sources are exclusive of the Lisp compiler.

   8. Openness/integrability/source availability:
      Source code (Common Lisp and C) is provided.

   9. Extensibility:
      This experimental prototype is not designed for extension by end users, although there are reasonably clean interfaces for extension or integration by developers.

   10. Pedigree: ARPA developed?
       Developed under NSF and ARPA sponsorship, including a subcontract to the ARPA Arcadia program.

5. Contact person(s)

   Michal Young
   Department of Computer Sciences
   Purdue University
   West Lafayette, IN 47907
   young@cs.purdue.edu
   yeh@cs.purdue.edu
   (317) 494-6023
   (317) 494-0739 - fax

6. Pointers to literature, demos, etc.:
   All papers are available by anonymous ftp to phosphor.cs.purdue.edu,
   directory pub/arcadia/papers. See manifest for contents.
   • Wei Jen Yeh and Michal Young. Compositional reachability analysis of Ada programs using process algebra. Preliminary version appeared in Proceedings of the Fourth ACM Symposium on Software Testing, Analysis, and Verification (TAV4), Victoria, BC, October 1991; the ftp-able version is greatly revised and expanded (July 1993) and has been submitted for journal publication.

   • Wei Jen Yeh and Michal Young, Redesigning Ada tasking programs for analysis, SERC technical report TR-148-P, December 1993, submitted for publication.

   • Wei Jen Yeh, Controlling State Explosion in Reachability Analysis, SERC technical report TR-147-P, August 1993 (Ph.D. Dissertation).

   • Demonstrations on request.