A Unified Memory Model for Pointers

Harvey Tuch and Gerwin Klein

Abstract

One of the challenges in verifying systems level code is the low-level, untyped view of the machine state that operating systems have. We describe a way to faithfully formalise this view while at the same time providing an easy-to-use, abstract and typed view of memory where possible. We have used this formal memory model to verify parts of the virtual memory subsystem of the L4 high-performance microkernel. All formalisations and proofs have been carried out in the theorem prover Isabelle and the verified code has been integrated into the current implementation of L4.

Online Copy

Available as [PDF]

Bibtex entry

@inproceedings{TuchK-05,
  author =       {Harvey Tuch and Gerwin Klein},
  title =        {A Unified Memory Model for Pointers},
  booktitle =    {12th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR-12)},
  year =      {2005},
  editor =    {Geoff Sutcliffe and Andrei Voronkov},
  address =   {Jamaica},
  month =     Dec,
  pages =     {474--488},
  series =    {Lecture Notes in Computer Science},
  volume =    {3835},
}
Gerwin Klein
2006-01-31 16:40:37