← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2000/manolios/pipeline/trivial/README

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2000/manolios/pipeline/trivial/README
 
1
This directory contains a proof that the Burch and Dill notion of
 
2
correctness used by Sawada is satisfied by a trivial machine. Sawada's
 
3
original proof is in the directory sawada-model, which you can use to
 
4
compare with the files in this directory.
 
5
 
 
6
Below is the README file that comes with Sawada's proof script.  To
 
7
Sawada's instructions on how to certify the books (which apply to both
 
8
this and the sawada-model directory) we add:
 
9
 
 
10
1.  In the makefile set the variable ACL2 correctly (i.e., so that it
 
11
    points to you local copy of ACL2).
 
12
 
 
13
2.  In ihs.lisp, basic-def.lisp, trivia.lisp, and utils.lisp fix the
 
14
    include book commands so that they point to the appropriate local
 
15
    copy of the ACL2 books.
 
16
 
 
17
 
 
18
We have gone about defining the trivial machine in a way that
 
19
minimizes the differences between our files and those of Sawada.
 
20
Therefore, the only files that have been modified are model.lisp and
 
21
proof.lisp.  In addition, any modifications are preceded by a comment
 
22
of the form:
 
23
 
 
24
; *******************CHANGE********************
 
25
; ...
 
26
; *******************CHANGE********************
 
27
 
 
28
An overview of what we have done is:
 
29
 
 
30
1. We changed the definition of MA, i.e., we have defined another
 
31
   pipelined machine.  This is in model.lisp
 
32
 
 
33
2. We have proven the same final theorem as Sawada, i.e., we have
 
34
   prove the new MA correct (with respect to the Burch and Dill
 
35
   variant of correctness used by Sawada, which includes a "liveness"
 
36
   property). This is in proof.lisp
 
37
 
 
38
3. We then prove about the new MA (in proof.lisp):
 
39
 
 
40
  (defthm ma-is-bad
 
41
    (implies (ma-state-p ma)
 
42
             (and (equal (ma-pc (ma-stepn ma x n))
 
43
                         (ma-pc ma))
 
44
                  (equal (ma-regs (ma-stepn ma x n))
 
45
                         (ma-regs ma))
 
46
                  (equal (ma-mem (ma-stepn ma x n))
 
47
                         (ma-mem ma)))))
 
48
 
 
49
  i.e., MA is a machine that never changes the programmer visible
 
50
  components of the machine.  Clearly, this should not be considered
 
51
  correct, hence, we saw that the Burch and Dill notion of correctness
 
52
  is flawed.
 
53
 
 
54
-----------------------------------------------
 
55
The Verification Proof Script for the Three-Stage Pipelined Machine
 
56
 
 
57
Author: Jun Sawada (sawada@cs.utexas.edu)
 
58
 
 
59
1. Files in this Directory
 
60
 
 
61
This directory contains the ACL2 books that define and verify the
 
62
three-stage pipelined machine discussed in the book.
 
63
There are three types of files: a makefile, files with the ".lisp"
 
64
extension, and files with the ".acl2" extension.  The makefile is used 
 
65
for the Unix make command.  The files with ".lisp" extension are ACL2
 
66
books which includes the ACL2 functions and theorems.  The files with
 
67
".acl2" extension are used during the certification process.
 
68
 
 
69
 
 
70
Following is the list of files with the ".lisp" extension: 
 
71
 
 
72
b-ops-aux-def.lisp:    Auxiliary definitions to the IHS library. 
 
73
b-ops-aux.lisp:        Auxiliary theorems to the IHS library.
 
74
basic-def.lisp:        The definitions of basic machine components.
 
75
basic-lemmas.lisp:     Basic theorems about the pipelined machine.
 
76
define-u-package.lisp: Book used to define package "u".
 
77
ihs.lisp:              Loads the IHS library and set the proper theory.
 
78
model.lisp:            The definition of the three-stage pipelined machine.
 
79
proof.lisp:            Proof of the commutative diagram. 
 
80
table-def.lisp:        The definition of the intermediate abstraction MAETT.
 
81
trivia.lisp:           Some trivial lemmas.
 
82
utils.lisp:            Definitions of utility functions.
 
83
 
 
84
 
 
85
How to re-certify the ACL2 book:
 
86
 
 
87
1.  You may have to modify the paths to the ACL2 public libraries. At
 
88
this moment, the ACL2 does not provide a uniform method to load ACL2
 
89
public libraries whose absolute path names may vary.  For example, the
 
90
IHS libraries are typically found in the "ihs" directory of the "book"
 
91
directory of the root directory for the ACL2 source code, but the ACL2
 
92
root directory is decided when it is installed.  If the load path to
 
93
the public libraries are not set properly, the certification process
 
94
fails.  You may have to change all the paths one-by-one.
 
95
 
 
96
 
 
97
2 Run "make".