TyPiCal

TyPiCal: Type-based static analyzer for the Pi-Calculus

Table of Contents

What is TyPiCal?

TyPiCal is a type-based static analyzer for the pi-calculus. The current version of TyPiCal provides the following program analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code elimination, information flow analysis, and termination analysis. The former two analyses aim to statically analyze whether each communication succeeds or not. The lock-freedom analysis can answer, e.g., the following questions about the behavior of concurrent/distributed programs:

Useless-code elimination (UCE) optimizes a pi-calculus process by removing sub-processes that do not affect the observable behavior of the process. The result of UCE is barbed congruent to the original process, but often simpler than the original process, so that it is more efficient, and easier to verify (with other tools such as model checkers). Information flow analyzer checks whether a process leaks information about secret data to the environment. You can try web interface for TyPiCal's deadlock-freedom analysis here.

Example

Consider the following program, which consists of two dining philosophers. ('?' stands for a receive operation, '!' stands for a send operation, and '*' stands for replication.) 
   new philos in new fork1 in new fork2 in
    *philos?x.(let left=fst(x) in let right=snd(x) in 
      left?w.right?w. /*** picks the left fork and then the right fork ***/
         (left!() | right!() | eating!() | philos!(left,right))) |
    philos!(fork1,fork2) |
    philos!(fork1,fork2) | 
    fork1!() | fork2!()
The two philosophers try to pick the two forks in the same order, so that they do not get into a deadlock. The lock-freedom analyzer of TyPiCal produces the following output: 
   new philos in new fork1 in new fork2 in
    *philos??x.(let left=fst(x) in let right=snd(x) in 
      left??w.right??w. /*** picks the left fork and then the right fork ***/
         (left!!() | right!!() | eating!() | philos!!(left,right))) |
    philos!!(fork1,fork2) |
    philos!!(fork1,fork2) | 
    fork1!!() | fork2!!()
All the communications except eating1!() are marked by !! or ??, which mean that those communications eventually succeed. The above result implies that two philosophers can acquire forks infinitely often. Given the same program, the useless-code eliminator of TyPiCal produces the following output: 
   *eating!()
Since the philosophers can acquire forks infinitely often, the whole process is actually observationally equivalent to *eating!().

If the second philosopher get forks in a different order: 

   new philos in new fork1 in new fork2 in
    *philos?x.(let left=fst(x) in let right=snd(x) in 
      left?w.right?w. /*** picks the left fork and then the right fork ***/
         (left!() | right!() | eating!() | philos!(left,right))) |
    philos!(fork1,fork2) |
    philos!(fork2,fork1) | 
    fork1!() | fork2!()
then, the output of the lock-freedom analyzer is: 
   new philos in new fork1 in new fork2 in
    *philos?x.(let left=fst(x) in let right=snd(x) in 
      left?w.right?w. /*** picks the left fork and then the right fork ***/
         (left!() | right!() | eating!() | philos!!(left,right))) |
    philos!!(fork1,fork2) |
    philos!!(fork2,fork1) | 
    fork1!!() | fork2!!()
So, we know that philosophers may not be able to eat (note that left?w and right?w are not annotated with ??). The useless-code eliminator does not eliminate any sub-process in this case. Consult README file in the distribution for more details.

How does it work?

TyPiCal is a type-based analyzer. To make it possible to analyze complex properties such as lock-freedom and information flow, an ordinary type system is extended so that channel types carry precise information about how each channel is used. TyPiCal performs type inference for such an extended type system, and obtains information about the behavior of a process. See papers available here for the theoretical background of TyPiCal. The following tutorial paper is recommended for the first read: 
  Naoki Kobayashi, "Type Systems for Concurrent Programs,"
  Proceedings of UNU/IIST 10th Anniversary Colloquium
  Springer LNCS 2757, pp.439-453
The technical background of TyPiCal is described in more detail in the following paper. 
  Naoki Kobayashi, "A New Type System for Deadlock-Free Processes,"
  CONCUR 2006, Springer LNCS 4137, pp.233-247, 2006.

  Naoki Kobayashi, "Type-Based Information Flow Analysis for the Pi-Calculus,"
  Acta Informatica, 42(4-5), pp.291-347, 2005.

  Naoki Kobayashi and Davide Sangiorgi, "A Hybrid Type System for Lock-Freedom of Mobile Processes,"
  CAV 2008, Springer LNCS, 2008.

Download

TyPiCal is free software. (We adapted the GNU public license before, but due to some request, we have switched to the BSD-style license. Please see README file in the distribution for the exact terms of redistribution and use.) You can download the current version of TyPiCal (version 1.6.2) from here. The distribution contains source programs and sample pi-calculus programs. You need Objective Caml to compile them.

Change history

Please read README file in the distribution for details about installation and usage.

Contact Information

Please send any questions, comments or bug reports to Naoki Kobayashi ()