[Prev][Next][Index][Thread]
deadlock-free process calculus
We would like to announce that the following draft
paper is available as
ftp://camille.is.s.u-tokyo.ac.jp/pub/papers/deadlock.dvi.Z
We completely revised the type system in our previous paper:
"A Partially-Deadlock-free Typed Process Calculus (I)."
Any comments are welcome.
--
A Partially Deadlock-free Typed Process Calculus (II)
by
Naoki Kobayashi
Univeristy of Tokyo
Abstract
We propose a novel static type system for a process calculus, which
ensures both partial deadlock-freedom and partial confluence. The key
ideas are (1) introduction of order of channel use as type
information, and (2)classification of communication channels into
reliable and unreliable channels based on their usage, with a grantee
of the usage by the type system. We can ensure that communications on
reliable channels never cause deadlock, and also that certain reliable
channels never introduce non-determinism. With the type system, for
example, both call-by-value and call-by-name simply typed
\(\lambda\)-calculus can be encoded into the deadlock-free and
confluent fragment of our process calculus; thus, we can recover
behavior of the typed \(\lambda\)-calculus in the level of process
calculi. We also show that typical concurrent objects and call-by-need
simply typed \(\lambda\)-calculus are also encoded into the
deadlock-free fragment.
--
Naoki Kobayashi
Department of Information Science
Faculty of Science
University of Tokyo
7-3-1 Hongo, Bunkyo-ku,
Tokyo 113, Japan
e-mail:koba@is.s.u-tokyo.ac.jp