← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/concurrent-programs/german-protocol/Readme.lsp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/concurrent-programs/german-protocol/Readme.lsp
 
1
;; Readme.lsp file for the contribution books/concurrent-programs/german-protocol/
 
2
 
 
3
(
 
4
 (:files
 
5
 "
 
6
.:
 
7
  Makefile  
 
8
  Readme.lsp  
 
9
  ccp.m  
 
10
  german.lisp
 
11
"
 
12
 )
 
13
 (:TITLE "An ACL2 Proof of Coherence of the German Protocol")
 
14
 (:AUTHOR/S "Sandip Ray")
 
15
 (:Keywords "concurrent programs"
 
16
            "inductive invariant"
 
17
            "iterative strengthening"
 
18
            "directory-based cache system"
 
19
            )
 
20
 (:ABSTRACT
 
21
 
 
22
"This set of books definea an invariant that is strong enbough to verify the
 
23
coherence of the German Cache Protocol.  The proof shows how to come up with a
 
24
sufficient inductive invariant by iterative strengthening starting from the
 
25
desired base property.  The proof also demonstrates how to define invariant
 
26
predicates for multiprocess systems both using quantification over process
 
27
indices and recursive functions, thus providing a tutorial demonstration of how
 
28
to reason about concurrent protoicols."  
 
29
)
 
30
 (:PERMISSION
 
31
 
 
32
"An ACL2 Proof of Coherence of the German Protocol
 
33
Copyright (C) 2006 Sandip Ray
 
34
 
 
35
This program is free software; you can redistribute it and/ormodify it under
 
36
the terms of the GNU General Public Licenseas published by the Free Software
 
37
Foundation; either version 2 of the License, or (at your option) any later
 
38
version. This program is distributed in the hope that it will be useful, but
 
39
WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
 
40
FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for more
 
41
details.You should have received a copy of the GNU General Public License along
 
42
with this program; if not, write to the Free Software Foundation, Inc., 51
 
43
Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA."
 
44
))
 
45
 
 
46
This set of books prvides an ACL2 proof of the German cache protocol.  The
 
47
protocol is translated directly into ACL2 from the murphy code provided in
 
48
ccp.m.  The proof involves formalizing coherence and strengthening the property
 
49
into an inductive invariant.
 
50
 
 
51
Background and Description
 
52
---------------------------
 
53
 
 
54
Anna Slobodova gave this problem to the author when she was looking for doing
 
55
cache protocol proofs with ACL2.  The key is that some predicates involved,
 
56
especially the key coherence property, could be naturally stated as quantified
 
57
formulas, and the question was how we could use the standard quantification
 
58
approaches together with (possibly) recursive functions to derive a proof in
 
59
the way the human would do.
 
60
 
 
61
I looked at the protocol and decided to do a proof on my own of the protocol in
 
62
ACL2.  Previously a similar proof ws done in ACL2 via predicate abstraction,
 
63
and this proof was primarily intended to show how predicate abstraction could
 
64
save labor over a standard ACL2 proof.  However, the ACL2 proof itself was not
 
65
devoid of interest, since it showed how one typically iterates over a partial
 
66
invariant to define a concrete inductive invariant for a protocol-level
 
67
system.  The proof did spring some surprises, for instance as documented in the
 
68
definition of some fragments of the invariant required in the proof.
 
69
 
 
70
However, the chief contribution of the proof is to provide a tutorial
 
71
introduction to coming up with an inductive invarriant for a complicated
 
72
multiprocess protocol.  Towards this end, substantial on-the-fly commentary of
 
73
the proof is provided in the form of comments, documenting the thought process
 
74
involved in the proof.  
 
75
 
 
76
For questions and concerns about these books, contact sandip@cs.utexas.edu.
 
 
b'\\ No newline at end of file'