Abstract
Embedded systems often come with constrained memory footprints. It is therefore essential to ensure that software running on such platforms fulfils memory usage specifications at compile-time, to prevent memory-related software failure after deployment. Previous proposals on memory usage verification are not satisfactory as they usually can only handle restricted subsets of programs, especially when shared mutable data structures are involved. In this paper, we propose a simple but novel solution. We instrument programs with explicit memory operations so that memory usage verification can be done along with the verification of other properties, using an automated verification system Hip/Sleek developed recently by Chin et al.[10,19]. The instrumentation can be done automatically and is proven sound with respect to an underlying semantics. One immediate benefit is that we do not need to develop from scratch a specific system for memory usage verification. Another benefit is that we can verify more programs, especially those involving shared mutable data structures, which previous systems failed to handle, as evidenced by our experimental results.
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.
Similar content being viewed by others
References
Amadio, R.M., Coupet-Grimal, S., Dal Zilio, S., Jakubiec, L.: A Functional Scenario for Bytecode Verification of Resource Bounds. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, pp. 265–279. Springer, Heidelberg (2004)
Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 1–26. Springer, Heidelberg (2005)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006)
Berdine, J., Cook, B., Distefano, D., O’Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386–400. Springer, Heidelberg (2006)
Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic certification of heap consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 347–362. Springer, Heidelberg (2005)
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: ACM POPL, pp. 289–300 (2009)
Campbell, B.: Amortised memory analysis using the depth of data structures. In: ESOP. LNCS, vol. 5502, pp. 190–204. Springer, Heidelberg (2009)
Carlisle, M.C., Rogers, A.: Software caching and computation migration in Olden. ACM SIGPLAN Notices 30(8), 29–38 (1995)
Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Enhancing modular oo verification with separation logic. In: ACM POPL, pp. 87–99 (2008)
Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Under Consideration by Science of Computer Programming (2009), http://www.dur.ac.uk/shengchao.qin/papers/SCP-draft.pdf
Chin, W.-N., Nguyen, H.H., Popeea, C., Qin, S.: Analysing memory resource bounds for low-level programs. In: International Symposium on Memory Management (ISMM), pp. 151–160. ACM Press, New York (2008)
Chin, W.-N., Nguyen, H.H., Qin, S., Rinard, M.: Memory usage verification for oo Programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 70–86. Springer, Heidelberg (2005)
Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)
Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: ACM OOPSLA, pp. 213–226 (2008)
Hofmann, M., Jost, S.: Static prediction of heap space usage for first order functional programs. In: ACM POPL, January 2003, pp. 185–197 (2003)
Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 22–37. Springer, Heidelberg (2006)
Ishtiaq, S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM POPL, January 2001, pp. 14–26 (2001)
Nguyen, H.H., Chin, W.-N.: Enhancing program verification with lemmas. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 355–369. Springer, Heidelberg (2008)
Nguyen, H.H., David, C., Qin, S., Chin, W.-N.: Automated verification of shape and size properties via separation logic. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 251–266. Springer, Heidelberg (2007)
Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: ACM POPL, pp. 75–86 (2008)
Reeves, G., Neilson, T., Litwin, T.: Mars exploration rover spirit vehicle anomaly report. Jet Propulsion Laboratory Document No. D-22919 (July 2004)
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: IEEE LICS, July 2002, pp. 55–74 (2002)
Xi, H.: Imperative programming with dependent types. In: IEEE LICS, June 2000, pp. 375–387 (2000)
Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
He, G., Qin, S., Luo, C., Chin, WN. (2009). Memory Usage Verification Using Hip/Sleek. In: Liu, Z., Ravn, A.P. (eds) Automated Technology for Verification and Analysis. ATVA 2009. Lecture Notes in Computer Science, vol 5799. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04761-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-04761-9_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04760-2
Online ISBN: 978-3-642-04761-9
eBook Packages: Computer ScienceComputer Science (R0)