Abstract
In this paper, we propose a type system to analyze the time consumed by multi-threaded imperative programs with a shared global memory, which delineates a class of safe multi-threaded programs. We demonstrate that a safe multi-threaded program runs in polynomial time if (i) it is strongly terminating wrt a non-deterministic scheduling policy or (ii) it terminates wrt a deterministic and quiet scheduling policy. As a consequence, we also characterize the set of polynomial time functions. The type system presented is based on the fundamental notion of data tiering, which is central in implicit computational complexity. It regulates the information flow in a computation. This aspect is interesting in that the type system bears a resemblance to typed based information flow analysis and notions of non-interference. As far as we know, this is the first characterization by a type system of polynomial time multi-threaded programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Amadio, R.M., Dabrowski, F.: Feasible reactivity in a synchronous pi-calculus. In: PPDP, pp. 221–230 (2007)
Amadio, R.M., Dal Zilio, S.: Resource control for synchronous cooperative threads. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 68–82. Springer, Heidelberg (2004)
Baillot, P., Terui, K.: Light types for polynomial time computation in lambda-calculus. In: LICS, pp. 266–275. IEEE Computer Society Press (2004)
Bell, D.E., La Padula, L.J.: Secure computer system: unified exposition and multics interpretation. Technical report, Mitre corp Rep. (1976)
Bellantoni, S., Cook, S.: A new recursion-theoretic characterization of the poly-time functions. Computational Complexity 2, 97–110 (1992)
Biba, K.: Integrity considerations for secure computer systems. Technical report, Mitre corp. Rep. (1977)
Bonfante, G., Marion, J.Y., Moyen, J.Y.: Quasi-interpretations a way to control resources. Theo. Comput. Sci. (2011)
Boudol, G., Castellani, I.: Noninterference for concurrent programs. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 382–395. Springer, Heidelberg (2001)
Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. In: PLDI, pp. 320–330 (2007)
Girard, J.-Y.: Light linear logic. Inf. Comput. 143(2), 175–204 (1998)
Hainry, E., Marion, J.-Y., Péchoux, R.: Type-based complexity analysis for fork processes. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol. 7794, pp. 305–320. Springer, Heidelberg (2013)
Hofmann, M.: Linear types and non-size-increasing polynomial time computation. Inf. Comput. 183(1), 57–85 (2003)
Jones, N.: The expressive power of higher-order types or, life without cons. J. Funct. Program. 11(1), 5–94 (2001)
Jones, N., Kristiansen, L.: A flow calculus of wp-bounds for complexity analysis. ACM Trans. Comput. Log. 10(4) (2009)
Jones, N.D.: Computability and complexity, from a programming perspective. MIT Press (1997)
Leivant, D.: A foundational delineation of poly-time. Inf. Comput. 110(2), 391–420 (1994)
Leivant, D.: Predicative recurrence and computational complexity i: Word recurrence and poly-time. In: Clote, P., Remmel, J. (eds.) Feasible Mathematrics II (1994)
Leivant, D., Marion, J.-Y.: Evolving graph-structures and their implicit computational complexity. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 349–360. Springer, Heidelberg (2013)
Madet, A., Amadio, R.M.: An elementary affine λ-calculus with multithreading and side effects. In: Ong, L. (ed.) TLCA 2011. LNCS, vol. 6690, pp. 138–152. Springer, Heidelberg (2011)
Marion, J.-Y.: A type system for complexity flow analysis. In: LICS, pp. 123–132 (2011)
Marion, J.Y., Péchoux, R.: Sup-interpretations, a semantic method for static analysis of program resources. ACM TOCL 10(4), 27 (2009)
Niggl, K.-H., Wunderlich, H.: Certifying polynomial time and linear/polynomial space for imperative programs. SIAM J. Comput. 35(5), 1122–1147 (2006)
Nowak, D., Zhang, Y.: A calculus for game-based security proofs. IACR Cryptology ePrint Archive, 2010:230 (2010)
Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications 21(1), 5–19 (2003)
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
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Marion, JY., Péchoux, R. (2014). Complexity Information Flow in a Multi-threaded Imperative Language. In: Gopal, T.V., Agrawal, M., Li, A., Cooper, S.B. (eds) Theory and Applications of Models of Computation. TAMC 2014. Lecture Notes in Computer Science, vol 8402. Springer, Cham. https://doi.org/10.1007/978-3-319-06089-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-06089-7_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06088-0
Online ISBN: 978-3-319-06089-7
eBook Packages: Computer ScienceComputer Science (R0)