Abstract
In our previous papers [7,11,23], we presented advanced type systems for the π-calculus, which can guarantee deadlock-freedom in the sense that certain communications will eventually succeed unless the whole process diverges. Although such guarantee is quite useful for reasoning about the behavior of concurrent programs, there still remains a weakness that the success of a communication cannot be completely guaranteed due to the problem of divergence. For example, while a server process that has received a request message cannot discard the request, it is allowed to infinitely delegate the request to other processes, causing a livelock. In this paper, we show that we can guarantee not only deadlock-freedom but also livelock-freedom, by modifying our previous type systems for deadlock-freedom. The resulting type system guarantees that certain communications will eventually succeed under fair scheduling, no matter whether processes diverge. Moreover, it can also guarantee that some of those communications will succeed within a certain amount of time.
Chapter PDF
References
G. Boudol. Typing the use of resources in a concurrent calculus. In Proceedings of ASIAN’97, pages 239–253, 1997.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 238–252, 1977.
K. Crary and S. Weirich. Resource bound certification. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 184–198, 2000.
C. Flanagan and M. Abadi. Object types against races. In CONCUR’99, LNCS 1664, pages 288–303. Springer-Verlag, 1999.
S. J. Gay. A sort inference algorithm for the polyadic π-calculus. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 429–438, 1993.
M. Hofmann. Linear types and non-size-increasing polynomial time computation. In Proceedings of IEEE Symposium on Logic in Computer Science, pages 464–473, 1999.
N. Kobayashi. A partially deadlock-free typed process calculus. ACM Transactions on Programming Languages and Systems, 20(2):436–482, 1998. A preliminary summary appeared in Proceedings of LICS’97, pages 128–139.
N. Kobayashi. Quasi-linear types. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 29–42, 1999.
N. Kobayashi. A livelock-free typed process calculus. Technical report, Dept. Info. Sci., Univ. of Tokyo, 2000. To appear. Available at http://www.yl.is.s.utokyo.ac.jp/~koba/publications.html.
N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems, 21(5):914–947, 1999. Preliminary summary appeared in Proceedings of POPL’96, pp.358-371.
N. Kobayashi, S. Saito, and E. Sumii. An implicitly-typed deadlock-free process calculus. Technical Report TR00-01, Dept. Info. Sci., Univ. of Tokyo, January 2000. Available at http://www.yl.is.s.u-tokyo.ac.jp/~koba/publications.html. A summary will appear in Proceedings of CONCUR 2000, LNCS, Springer-Verlag.
N. Kobayashi and A. Yonezawa. Towards foundations for concurrent object-Oriented programming-types and language design. Theory and Practice of Object Systems, 1(4):243–268, 1995.
R. Milner. The polyadic π-calculus: a tutorial. In F. L. Bauer, W. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification. Springer-Verlag, 1993.
R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, I, II. Information and Computation, 100:1–77, September 1992.
U. Nestmann. What is a ‘good’ encoding of guarded choice? In EXPRESS’97, volume 7 of ENTCS. Elsevier Science Publishers, September 1997.
S. Peyton Jones. Concurrent Haskell. In Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pages 295–308, 1996.
B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. Mathematical Structures in Computer Science, 6(5):409–454, 1996.
B. C. Pierce and D. N. Turner. Concurrent objects in a process calculus. In Theory and Practice of Parallel Programming (TPPP), Sendai, Japan (Nov. 1994), LNCS 907, pages 187–215. Springer-Verlag, 1995.
F. Puntigam. Coordination requirements expressed in types for active objects. In Proceedings of ECOOP’97, LNCS 1241, pages 367–388, 1997.
F. Puntigam and C. Peter. Changeable interfaces and promised messages for concurrent components. In Proceedings of the 1999 ACM Symposium on Applied Computing, pages 141–145, 1999.
J. H. Reppy. CML: A higher-order concurrent language. In Proceedings of the ACM SIGPLAN’91 Conference on Programming Language Design and Implementation, pages 293–305, 1991.
D. Sangiorgi. The name discipline of uniform receptiveness (extended abstract). In Proceedings of ICALP’97, LNCS 1256, pages 303–313, 1997.
E. Sumii and N. Kobayashi. A generalized deadlock-free process calculus. In Proc. of Workshop on High-Level Concurrent Language (HLCL’98), volume 16(3) of ENTCS, pages 55–77, 1998.
V. T. Vasconcelos and K. Honda. Principal typing schemes in a polyadic π-calculus. In CONCUR’93, LNCS 715, pages 524–538. Springer-Verlag, 1993.
A. Yonezawa and M. Tokoro. Object-Oriented Concurrent Programming. The MIT Press, 1987.
N. Yoshida. Graph types for monadic mobile processes. In FST/TCS’16, LNCS 1180, pages 371–387. Springer-Verlag, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kobayashi, N. (2000). Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, Time-Boundedness. In: van Leeuwen, J., Watanabe, O., Hagiya, M., Mosses, P.D., Ito, T. (eds) Theoretical Computer Science: Exploring New Frontiers of Theoretical Informatics. TCS 2000. Lecture Notes in Computer Science, vol 1872. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44929-9_27
Download citation
DOI: https://doi.org/10.1007/3-540-44929-9_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67823-6
Online ISBN: 978-3-540-44929-4
eBook Packages: Springer Book Archive