[llvm-commits] CVS: llvm-www/pubs/2009-01-VMCAI-ScalableMemoryModel.html 2009-01-VMCAI-ScalableMemoryModel.pdf pubs.js

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',




