Abstract
We introduce a type system for concurrent programs described as a parallel imperative language using while-loops and fork/wait instructions, in which processes do not share a global memory, in order to analyze computational complexity. The type system provides an analysis of the data-flow based both on a data ramification principle related to tiering discipline and on secure typed languages. The main result states that well-typed processes characterize exactly the set of functions computable in polynomial space under termination, confluence and lock-freedom assumptions. More precisely, each process computes in polynomial time so that the evaluation of a process may be performed in polynomial time on a parallel model of computation. Type inference of the presented analysis is decidable in linear time provided that basic operator semantics is known.
Chapter PDF
Similar content being viewed by others
References
Amadio, R.M., Dabrowski, F.: Feasible reactivity for synchronous cooperative threads. Electron. Notes Theor. Comput. Sci. 154(3), 33–43 (2006)
Amadio, R.M., Dabrowski, F.: Feasible reactivity in a synchronous pi-calculus. In: Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, PPDP 2007, pp. 221–230. ACM, New York (2007)
Biba, K.: Integrity considerations for secure computer systems. Technical report, Mitre corp Rep. (1977)
Buss, S.R.: The boolean formula value problem is in ALOGTIME. In: Proceedings of the Nineteenth Annual ACM Symposium on Theory of Computing, STOC 1987, pp. 123–131. ACM, New York (1987)
Chandra, A., Kozen, D., Stockmeyer, L.: Alternation. J. ACM 28(1), 114–133 (1981)
Cockett, R., Redmond, B.: A categorical setting for lower complexity. Electron. Notes Theor. Comput. Sci. 265, 277–300 (2010)
Gaboardi, M., Marion, J.-Y., Ronchi Della Rocca, S.: A logical account of PSPACE. In: POPL 2008, pp. 121–131. ACM (2008)
Jones, N.D.: The expressive power of higher-order types or, life without cons. J. Funct. Program. 11(1), 5–94 (2001)
Jones, N.D., Kristiansen, L.: A flow calculus of wp-bounds for complexity analysis. ACM Trans. Comput. Log. 10(4) (2009)
Ladner, R.E., Fischer, M.J.: Parallel prefix computation. J. ACM 27(4), 831–838 (1980)
Lafont, Y.: Soft linear logic and polynomial time. Theor. Comput. Sci. 318(1-2), 163–180 (2004)
Dal Lago, U., Di Giamberardino, P.: Soft session types. In: EXPRESS 2011. EPTCS, vol. 64, pp. 59–73 (2011)
Dal Lago, U., Martini, S., Sangiorgi, D.: Light logics and higher-order processes. In: EXPRESS 2010. EPTCS, vol. 41, pp. 46–60 (2010)
Leivant, D., Marion, J.-Y.: Ramified Recurrence and Computational Complexity II: Substitution and Poly-Space. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933, pp. 486–500. Springer, Heidelberg (1995)
Leivant, D., Marion, J.-Y.: Predicative Functional Recurrence and Poly-Space. In: Bidoit, M., Dauchet, M. (eds.) TAPSOFT 1997. LNCS, vol. 1214, pp. 369–380. Springer, Heidelberg (1997)
Madet, A.: A polynomial time lambda-calculus with multithreading and side effects. In: PPDP (2012)
Marion, J.-Y.: A type system for complexity flow analysis. In: LICS, pp. 123–132 (2011)
Moyen, J.-Y.: Resource control graphs. ACM Trans. Comput. Logic 10(4), 29:1–29:44 (2009)
Niggl, K.-H., Wunderlich, H.: Certifying polynomial time and linear/polynomial space for imperative programs. SIAM J. Comput. 35(5), 1122–1147 (2006)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)
Savitch, W.J.: Relationship between nondeterministic and deterministic tape classes. JCSS 4, 177–192 (1970)
Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: POPL, pp. 355–364. ACM (1998)
Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. Journal of Computer Security 4(2/3), 167–188 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hainry, E., Marion, JY., Péchoux, R. (2013). Type-Based Complexity Analysis for Fork Processes. In: Pfenning, F. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2013. Lecture Notes in Computer Science, vol 7794. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37075-5_20
Download citation
DOI: https://doi.org/10.1007/978-3-642-37075-5_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37074-8
Online ISBN: 978-3-642-37075-5
eBook Packages: Computer ScienceComputer Science (R0)