Advertisement

Abstract

We present Mapped Separation Logic, an instance of Separation Logic for reasoning about virtual memory. Our logic is formalised in the Isabelle/HOL theorem prover and it allows reasoning on properties about page tables, direct physical memory access, virtual memory access, and shared memory. Mapped Separation Logic fully supports all rules of abstract Separation Logic, including the frame rule.

Keywords

Address Space Physical Memory Assignment Rule Virtual Memory Proof Rule 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Affeldt, R., Marti, N.: Separation logic in Coq (2008), http://savannah.nongnu.org/projects/seplog
  2. 2.
    Bornat, R., Calcagno, C., O’Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL 2005: Proc3̇2nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 259–270. ACM, New York (2005)CrossRefGoogle Scholar
  3. 3.
    Alkassar, E., Schirmer, N., Starostin, A.: Formal pervasive verification of a paging mechanism. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963. Springer, Heidelberg (to appear, 2008)CrossRefGoogle Scholar
  4. 4.
    Calcagno, C., O’Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS 2007: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pp. 366–378. IEEE Computer Society Press, Los Alamitos (2007)CrossRefGoogle Scholar
  5. 5.
    Dalinger, I., Hillebrand, M.A., Paul, W.J.: On the verification of memory management mechanisms. In: Borrione, D., Paul, W.J. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 301–316. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Derrin, P., Elphinstone, K., Klein, G., Cock, D., Chakravarty, M.M.T.: Running the manual: An approach to high-assurance microkernel development. In: Proc. ACM SIGPLAN Haskell WS, Portland, OR, USA (September 2006)Google Scholar
  7. 7.
    Elphinstone, K., Klein, G., Derrin, P., Roscoe, T., Heiser, G.: Towards a practical, verified kernel. In: Proc. 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, p. 6 ( May 2007)Google Scholar
  8. 8.
    Hillebrand, M.: Address Spaces and Virtual Memory: Specification, Implementation, and Correctness. PhD thesis, Saarland University, Saarbrücken (2005)Google Scholar
  9. 9.
    Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL 2001: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 14–26. ACM, New York (2001)CrossRefGoogle Scholar
  10. 10.
    Klein, G., Tuch, H.: Towards verified virtual memory in L4. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223. Springer, Heidelberg (2004)Google Scholar
  11. 11.
    Kolanski, R.: A logic for virtual memory. In: Huuck, R., Klein, G., Schlich, B. (eds.) Proc. 3rd Int’l Workshop on Systems Software Verification (SSV 2008). ENTCS, pp. 55–70. Elsevier, Amsterdam (to appear, 2008)Google Scholar
  12. 12.
    Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)zbMATHGoogle Scholar
  13. 13.
    O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004: Proc. 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 268–280. ACM, New York (2004)CrossRefGoogle Scholar
  14. 14.
    Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL 2005: Proc. 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 247–258. ACM, New York (2005)CrossRefGoogle Scholar
  15. 15.
    Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. 17th IEEE Symposium on Logic in Computer Science, pp. 55–74 (2002)Google Scholar
  16. 16.
    Tews, H.: Formal methods in the Robin project: Specification and verification of the Nova microhypervisor. In: C/C++ Verification Workshop, Technical Report ICIS-R07015, pp. 59–68, Oxford, UK. Radboud University Nijmegen (July 2007)Google Scholar
  17. 17.
    Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) POPL 2007, pp. 97–108. ACM, New York (2007)CrossRefGoogle Scholar
  18. 18.
    Weber, T.: Towards mechanized program verification with separation logic. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210. pp. 250–264. Springer, Heidelberg (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Rafal Kolanski
    • 1
    • 2
  • Gerwin Klein
    • 1
    • 2
  1. 1.Sydney Research Lab.NICTAAustralia
  2. 2.School of Computer Science and EngineeringUNSWSydneyAustralia

Personalised recommendations