×

Safety guarantees from explicit resource management. (English) Zbl 1209.68119

de Boer, Frank S. (ed.) et al., Formal methods for components and objects. 6th international symposium, FMCO 2007, Amsterdam, The Netherlands, October 24–26, 2007. Revised lectures. Berlin: Springer (ISBN 978-3-540-92187-5/pbk). Lecture Notes in Computer Science 5382, 52-71 (2008).
Summary: We present a language and a program analysis that certifies the safe use of flexible resource management idioms, in particular advance reservation or “block booking” of costly resources. This builds on previous work with resource managers that carry out runtime safety checks, by showing how to assist these with compile-time checks. We give a small ANF-style language with explicit resource managers, and introduce a type and effect system that captures their runtime behaviour. In this setting, we identify a notion of dynamic safety for running code, and show that dynamically safe code may be executed without runtime checks. We show a similar static safety property for type-safe code, and prove that static safety implies dynamic safety. The consequence is that typechecked code can be executed without runtime instrumentation, and is guaranteed to make only appropriate use of resources.
For the entire collection see [Zbl 1155.68012].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Appel, A.W.: SSA is functional programming. SIGPLAN Notices 33(4), 17–20 (1998) · doi:10.1145/278283.278285
[2] Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resources. Theoret. Comput. Sci. 389(3), 411–445 (2007) · Zbl 1133.68010 · doi:10.1016/j.tcs.2007.09.003
[3] Aspinall, D., Maier, P., Stark, I.: Monitoring external resources in Java MIDP. Electron. Notes Theor. Comput. Sci. 197, 17–30 (2008) · doi:10.1016/j.entcs.2007.10.011
[4] Barrett, C., de Moura, L., Stump, A.: Design and results of the 2nd annual satisfiability modulo theories competition. Form. Meth. Syst. Des. 31(3), 221–239 (2007) · Zbl 1129.68498 · doi:10.1007/s10703-007-0038-1
[5] Barthe, G., Beringer, L., Crégut, P., Grégoire, B., Hofmann, M., Müller, P., Poll, E., Puebla, G., Stark, I., Vétillard, E.: MOBIUS: Mobility, ubiquity, security. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 10–29. Springer, Heidelberg (2007) · Zbl 05523434 · doi:10.1007/978-3-540-75336-0_2
[6] Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic certification of heap consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol. 3452, pp. 347–362. Springer, Heidelberg (2005) · Zbl 1108.68374 · doi:10.1007/978-3-540-32275-7_23
[7] Besson, F., Dufay, G., Jensen, T.P.: A formal model of access control for mobile interactive devices. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol. 4189, pp. 110–126. Springer, Heidelberg (2006) · doi:10.1007/11863908_8
[8] Binder, W., Hulaas, J., Villazón, A.: Portable resource control in Java. In: Proc. OOPSLA 2001, pp. 139–155. ACM, New York (2001) · Zbl 1052.68961
[9] Czajkowski, G., von Eicken, T.: JRes: A resource accounting interface for Java. In: Proc. OOPSLA 1998, pp. 21–35. ACM, New York (1998)
[10] Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. In: Proc. PLDI 1993, pp. 237–247. ACM, New York (1993)
[11] Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract predicates and mutable ADTs in Hoare type theory. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 189–204. Springer, Heidelberg (2007) · Zbl 1187.68158 · doi:10.1007/978-3-540-71316-6_14
[12] Unknown: Redbrowser. A, J2ME trojan. Identified in the February 2006 as Redbrowser. A (F-Secure), J2ME/Redbrowser.a (McAfee), Trojan. Redbrowser. A (Symantec), Trojan-SMS.J2ME.Redbrowser.a (Kaspersky Lab)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.