[llvm-commits] CVS: llvm-www/pubs/2009-01-VMCAI-ScalableMemoryModel.html 2009-01-VMCAI-ScalableMemoryModel.pdf pubs.js
Chris Lattner
sabre at nondot.org
Tue Mar 24 22:58:18 PDT 2009
Changes in directory llvm-www/pubs:
2009-01-VMCAI-ScalableMemoryModel.html added (r1.1)
2009-01-VMCAI-ScalableMemoryModel.pdf added (r1.1)
pubs.js updated: 1.11 -> 1.12
---
Log message:
add another paper.
---
Diffs of the changes: (+58 -0)
2009-01-VMCAI-ScalableMemoryModel.html | 50 +++++++++++++++++++++++++++++++++
2009-01-VMCAI-ScalableMemoryModel.pdf | 0
pubs.js | 8 +++++
3 files changed, 58 insertions(+)
Index: llvm-www/pubs/2009-01-VMCAI-ScalableMemoryModel.html
diff -c /dev/null llvm-www/pubs/2009-01-VMCAI-ScalableMemoryModel.html:1.1
*** /dev/null Wed Mar 25 00:58:02 2009
--- llvm-www/pubs/2009-01-VMCAI-ScalableMemoryModel.html Wed Mar 25 00:57:51 2009
***************
*** 0 ****
--- 1,50 ----
+ <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+ <html>
+ <head>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
+ <link rel="stylesheet" href="http://llvm.org/llvm.css" type="text/css" media="screen" />
+ <title>A Scalable Memory Model for Low-Level Code</title>
+ </head>
+ <body>
+
+ <div class="pub_title">
+ A Scalable Memory Model for Low-Level Code
+ </div>
+ <div class="pub_author">
+ Zvonimir Rakamaric and Alan J. Hu
+ </div>
+
+ <h2>Abstract:</h2>
+ <blockquote>
+ Because of its critical importance underlying all other software, low-level
+ system software is among the most important targets for formal verification.
+ Low-level systems software must sometimes make type-unsafe memory accesses,
+ but because of the vast size of available heap memory in today's computer systems,
+ faithfully representing each memory allocation and access does not scale
+ when analyzing large programs. Instead, verification tools rely on abstract memory
+ models to represent the program heap. This paper reports on two related
+ investigations to develop an accurate (i.e., providing a useful level of soundness
+ and precision) and scalable memory model: First, we compare a recently introduced
+ memory model, specifically designed to more accurately model low-level
+ memory accesses in systems code, to an older, widely adopted memory model.
+ Unfortunately, we find that the newer memory model scales poorly compared to
+ the earlier, less accurate model. Next, we investigate how to improve the
+ soundness of the less accurate model. A direct approach is to add assertions to the code
+ that each memory access does not break the assumptions of the memory model,
+ but this causes verification complexity to blow-up. Instead, we develop a novel,
+ extremely lightweight static analysis that quickly and conservatively guarantees
+ that most memory accesses safely respect the assumptions of the memory model,
+ thereby eliminating almost all of these extra type-checking assertions. Furthermore,
+ this analysis allows us to create automatically memory models that flexibly
+ use the more scalable memory model for most of memory, but resorting to a more
+ accurate model for memory accesses that might need it.
+ </blockquote>
+
+ <h2>Download:</h2>
+ <ul>
+ <li><a href="2009-01-VMCAI-ScalableMemoryModel.pdf">A
+ Scalable Memory Model for Low-Level Code</a> (PDF)</li>
+ </ul>
+
+ </body>
+ </html>
Index: llvm-www/pubs/2009-01-VMCAI-ScalableMemoryModel.pdf
Index: llvm-www/pubs/pubs.js
diff -u llvm-www/pubs/pubs.js:1.11 llvm-www/pubs/pubs.js:1.12
--- llvm-www/pubs/pubs.js:1.11 Wed Mar 25 00:49:31 2009
+++ llvm-www/pubs/pubs.js Wed Mar 25 00:57:52 2009
@@ -14,6 +14,14 @@
month: 3,
year: 2009},
+ {url: '2009-01-VMCAI-ScalableMemoryModel.html',
+ title: 'A Scalable Memory Model for Low-Level Code',
+ author: 'Zvonimir Rakamaric and Alan J. Hu',
+ published: 'Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2009)',
+ location: 'Savannah, GA, USA',
+ month: 1,
+ year: 2009},
+
{url: '2009-01-ASP-DAC-Automatic_Instrumentation.html',
title: 'Automatic Instrumentation of Embedded Software for High Level Hardware/Software Co-Simulation',
author: 'Aimen Bouchhima, Patrice Gerin, Frederic Petrot',
More information about the llvm-commits
mailing list