Abstract
We propose a type system for lock-freedom in the π-calculus, which guarantees that certain communications will eventually succeed. Distinguishing features of our type system are: it can verify lock-freedom of concurrent programs that have sophisticated recursive communication structures; it can be fully automated; it is hybrid, in that it combines a type system for lock-freedom with local reasoning about deadlock-freedom, termination, and confluence analyses. Moreover, the type system is parameterized by deadlock-freedom/termination/confluence analyses, so that any methods (e.g. type systems and model checking) can be used for those analyses. A lock-freedom analysis tool has been implemented based on the proposed type system, and tested for non-trivial programs.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Acciai, L., Boreale, M.: Responsiveness in process calculi. In: Proc. of 11th Annual Asian Computing Science Conference (ASIAN 2006). LNCS, vol. 4435, pp. 136–150. Springer, Heidelberg (2006)
Ben-Amram, A.M., Lee, C.S.: Program termination analysis in polynomial time. ACM Trans. Prog. Lang. Syst. 29(1 (Article 5)) (2007)
Bidinger, P., Compagnoni, A.B.: Pict correctness revisited. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 206–220. Springer, Heidelberg (2007)
Brinksma, E., Rensink, A., Volger, W.: Fair testing. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 313–327. Springer, Heidelberg (1995)
Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: Proc. of POPL, pp. 265–276 (2007)
Demangeon, R., Hirschkoff, D., Kobayashi, N., Sangiorgi, D.: On the complexity of termination inference for processes. In: Barthe, G., Fournet, C. (eds.) Proceedings of TGC 2007. LNCS, vol. 4912, pp. 140–155. Springer, Heidelberg (2008)
Deng, Y., Sangiorgi, D.: Ensuring termination by typability. Info. Comput. 204(7), 1045–1082 (2006)
Kobayashi, N.: A type system for lock-free processes. Info. Comput. 177, 122–159 (2002)
Kobayashi, N.: Type-based information flow analysis for the pi-calculus. Acta Informatica 42(4-5), 291–347 (2005)
Kobayashi, N.: TyPiCal: A type-based static analyzer for the pi-calculus, http://www.kb.ecei.tohoku.ac.jp/~koba/typical/
Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 233–247. Springer, Heidelberg (2006)
Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Prog. Lang. Syst. 21(5), 914–947 (1999)
Kobayashi, N., Sangiorgi, D.: A hybrid type system for lock-freedom of mobile processes. An extended version (2008), http://www.kb.ecei.tohoku.ac.jp/~koba/papers/hybrid.pdf
Leroy, X.: A modular module system. J. Funct. Program. 10(3), 269–303 (2000)
Pierce, B.C., Turner, D.N.: Pict: A programming language based on the pi-calculus. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner, pp. 455–494. MIT Press, Cambridge (2000)
Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Sangiorgi, D.: Termination of processes. Math. Struct. Comput. Sci. 16(1), 1–39 (2006)
Terauchi, T., Aiken, A.: A Capability Calculus for Concurrency and Determinism. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 218–232. Springer, Heidelberg (2006)
Sangiorgi, D.: The name discipline of uniform receptiveness. Theor. Comput. Sci. 221(1-2), 457–493 (1999)
Yoshida, N.: Type-based liveness guarantee in the presence of nontermination and nondeterminism. Technical Report 2002-20, MSC Technical Report, University of Leicester (April 2002)
Yoshida, N., Berger, M., Honda, K.: Strong normalisation in the pi-calculus. Info. Comput. 191(2), 145–202 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kobayashi, N., Sangiorgi, D. (2008). A Hybrid Type System for Lock-Freedom of Mobile Processes. In: Gupta, A., Malik, S. (eds) Computer Aided Verification. CAV 2008. Lecture Notes in Computer Science, vol 5123. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70545-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-70545-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70543-7
Online ISBN: 978-3-540-70545-1
eBook Packages: Computer ScienceComputer Science (R0)