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