Provisional-certification
Certify a book in stages for improved book-level parallelism
Provisional certification is a process that can increase
parallelism when certifying books in parallel, typically using `make', when
certifying a collection of books. We got this idea from Jared Davis,
who developed rudimentary provisional certification schemes first at Rockwell
Collins and later for his `Milawa' project. Our design has also benefited
from conversations with Sol Swords.
Warning: as of November 2014, enabling provision certification via the
ACL2_PCERT flag can not be reliably enabled at the Makefile level (as is
shown below). See Github
Issue 255 for more information.
To invoke provisional certification, see books-certification. For
example, you could issue the following command.
cert.pl --pcert-all -j 4 `find . -name '*.lisp'`
Alternatively, see books-certification-classic for a discussion of
classic ACL2 `make'-based certification (which may disappear in a future ACL2
release); here we extend those instructions to show how to use provisional
certification. (Also, you may wish to look at community books file
books/system/pcert/Makefile for an example.) We begin by describing a
few ways to do that. A simple way is to add the line `ACL2_PCERT=t' to a
`make' command that you use for book certification, for example as
follows.
make -j 4 ACL2_PCERT=t
The following works too, in a bash shell.
(export ACL2_PCERT=t ; time make -j 4)
Alternatively, add the line
ACL2_PCERT ?= t
to the Makefile residing in the directory, placed above the line that
specifies the `include' of file Makefile-generic. A successful
`make' will result in creating the desired certificate (.cert)
files.
Warning: If you put the line ``ACL2_PCERT ?= t'' below the include of
Makefile-generic, it might have no effect. For example, try editing
community books file books/system/pcert/Makefile by moving the line
``ACL2_PCERT ?= t'' to the bottom of the file, and watch ``make
top.cert'' fail to invoke provisional certification.
The description above may be sufficient for you to use provisional
certification. We provide additional documentation below for the reader who
wants to understand more about this process, for example when not using
`make'. Below we assume prior familiarity with books, in particular
certify-book and include-book. The remainder of this documentation topic is divided into sections: Summary, Correctness Claim and
Issues, Combining Pcertify and Convert into Pcertify+, and Further
Information.
Summary
Recall that certification of a book, bk, produces a certificate
file bk.cert. The provisional certification process produces this file
as well, but as the last of the following three steps. All of these steps are
carried out by calls of certify-book using its :pcert keyword
argument. We typically call these steps ``procedures'', to distinguish them
from the steps of an individual call of certify-book.
- The ``Pcertify'' procedure (sometimes called the ``Create''
procedure) is invoked by calling certify-book with keyword argument
:pcert :create. It produces a file bk.pcert0, sometimes called the
``.pcert0'' file (pronounced ``dot pee cert zero''). Proofs are skipped
during this procedure, which can be viewed as an elaborate syntax check,
augmented by compilation if specified (as it is by default).
- The ``Convert'' procedure is invoked by calling certify-book with
keyword argument :pcert :convert. It creates file bk.pcert1 from
bk.pcert0, by doing proofs for all events in bk.lisp. Note that the
third argument (the `compile-flg' argument) is ignored by such a call of
certify-book unless its value is :all (either explicitly or by way
of environment variable ACL2_COMPILE_FLG). A subtlety is that if there
is a compiled file at least as recent as the corresponding .pcert0 file,
then that compiled file's write date will be updated to the current time at
the end of this procedure. The usual local-incompatibility check at
the end of certify-book is omitted for the Convert procedure, since it
was performed towards the end of the Create procedure.
- The ``Complete'' procedure is invoked by calling certify-book
with keyword argument :pcert :complete. It checks that every included
book (including every one that is locally included) has a .cert
file that is at least as recent as the corresponding book. The effect is to
move bk.pcert1 to bk.cert. Note that all arguments of
certify-book other than the :pcert argument are ignored for this
procedure, other than for some trivial argument checking.
You can combine the Pcertify and Convert procedures into a single
procedure, Pcertify+, which may be useful for books that contain expensive
include-book events but do few proofs. We defer discussion of
that feature to the section below, ``Combining Pcertify and Convert into
Pcertify+''.
The main idea of provisional certification is to break sequential
dependencies caused by include-book, that is, so that a book's proofs
are carried out even when it includes books (sometimes called ``sub-books'')
that have not themselves been fully certified. For example, suppose that a
proof development consists of books A.lisp, B.lisp, and C.lisp,
where file A.lisp contains the form (include-book "B") and file
B.lisp contains the form (include-book "C"). Normally one would
first certify C, then B, and finally, A. However, the
provisional certification process can speed up the process on a multi-core
machine, as follows: the Pcertify (pronounced ``pee certify'') procedure
respects this order but (one hopes) is fast since proofs are skipped; the
Convert procedure essentially completes the certification in parallel by doing
proofs and creating .pcert1 files based on .pcert0 files; and the
Complete procedure respects book order when quickly renaming .pcert1
files to .cert files. In our example, the steps would be as follows, but
note that we need not finish all Pcertify steps before starting some Convert
steps, nor need we finish all Convert steps before starting some Complete
steps, as explained further below.
- Pcertify books "C", "B",and then "A", sequentially,
skipping proofs but doing compilation.
- Do proofs in parallel for the books using the Convert procedure, where
each book relies on the existence of its own .pcert0 file as well as a
.cert, .pcert0, or .pcert1 file for each of its included
sub-books. Write out a .pcert1 file for the book when the proof
succeeds.
- Rename the .pcert1 file to a corresponding .cert file when a
.cert file exists and is up-to-date for each included
book.
The Convert step can begin for bk.lisp any time after bk.pcert0
is built. The Complete step can begin for this book any time after
bk.pcert1 and every sub-bk.cert are built, for sub-bk a
sub-book of bk.
The new procedures — Pcertify, Convert, and Complete — are
invoked by supplying a value for the keyword argument :pcert of certify-book, namely :create, :convert, or :complete,
respectively. Typically, and by default, the compile-flg argument of
certify-book is t for the Pcertify procedure, so that compilation can take full advantage of parallelism. This argument is treated
as nil for the other procedures except when its value is :all in the
Convert procedure, as mentioned above.
For those who use make-event, we note that expansion is done in the
Pcertify procedure; the later steps use the expansion resulting from that
procedure. The reason is that although a call of make-event is
similar to a macro call, a difference is that the expansion of a
make-event form can depend on the state. Therefore, we insist on
doing such an expansion only once, so that all books involved agree on the
expansion. We say more about make-event below.
Correctness Claim and Issues
The Basic Claim for certification is the same whether or not the
provisional certification process is employed: all books should be certified
from scratch, with no files written to the directories of the books except by
ACL2. Moreover, no trust tags should be used (see defttag), or else it
is the responsibility of the user to investigate every occurrence of ``TTAG
NOTE'' that is printed to standard output.
But common practice is to certify a set of books in stages: certify a few
books, fix some books, re-certify changed books, certify some more books, and
so on. In practice, we expect this process to be sound even though it does
not meet the preconditions for the Basic Claim above. In particular, we
expect that the use of book-hash values in certificates will
make it exceedingly unlikely that a book is still treated as certified after
any events in the book or any sub-book, or any portcullis commands of the book or any sub-book, have been modified.
Provisional certification makes it a bit easier for a determined user to
subvert correctness. For example, the Complete procedure only checks write
dates to ensure that each sub-book's .cert file is no older than the
corresponding .lisp file, but it does not look inside .cert files of
sub-books; in particular it does not look at their book-hash
information. Of course, the automatic dependency analysis provided by classic
ACL2 `make'-based certification avoids accidental problems of this sort. And,
book-hash information will indeed be applied at include-book time, at
least for sub-books included non-locally.
In short: while we believe that the provisional certification process can
be trusted, we suggest that for maximum trust, it is best for all books in a
project to be certified from scratch without the provisional certification
process.
Combining Pcertify and Convert into Pcertify+
You can combine the Pcertify and Convert procedure into a single procedure,
Pcertify+, which may be useful for books that contain expensive include-book events but do few proofs. If you are using `make' to do
provisional certification as described above, just set `make' variable
ACL2_BOOKS_PCERT_ARG_T to the list of books for which you want the
Pcertify+ procedure performed instead of separate Pcertify and Convert
procedures. Either of two common methods may be used to set this variable, as
illustrated below for the case that books sub.lisp and mid.lisp are
the ones on which you want Pcertify+ performed. One method is to add the
following to your directory's Makefile, above the include of
Makefile-generic.
ACL2_BOOKS_PCERT_ARG_T = sub mid
Alternatively, you can specify the desired books on the command line, for
example as follows.
make -j 4 ACL2_BOOKS_PCERT_ARG_T='sub mid'
Note that the books are given without their .lisp extensions.
At the ACL2 level, the Pcertify+ procedure is performed when the value
t is supplied to the :pcert keyword argument of certify-book. Thus, :pcert t can be thought of as a combination of
:pcert :create and :pcert :convert. However, what ACL2 actually
does is to perform the Pcertify step without skipping proofs, and at the end
of the certify-book run, it writes out both the .pcert0 and
.pcert1 file, with essentially the same contents. (We say
``essentially'' because the implementation writes :PCERT-INFO :PROVED to
the end of the .pcert0 file, but not to the .pcert1 file.)
Further Information
Some errors during provisional certification cannot be readily solved. For
example, if there are circular directory dependencies (for example, some book
in directory D1 includes some book in directory D2 and vice-versa), then
classic ACL2 `make'-based certification will quite possibly fail. For another
example, perhaps your directory's Makefile is awkward to convert to one with
suitable dependencies. When no fix is at hand, it might be best simply to
avoid provisional certification. If you are using classic ACL2 `make'-based
certification, you can simply add the following line to your directory's
Makefile, or use ``ACL2_PCERT= '' on the `make' command line, to
avoid provisional certification.
override ACL2_PCERT =
We invite anyone who has troubleshooting tips to contact the ACL2
developers with suggestions for adding such tips to this section.
Our next remark is relevant only to users of make-event, and
concerns the interaction of that utility with state global ld-skip-proofsp. Normally, the global value of ld-skip-proofsp is
unchanged during make-event expansion, except that it is bound to
nil when the make-event form has a non-nil
:check-expansion argument. But during the Pcertify procedure (not the
Pcertify+ procedure), ld-skip-proofsp is always bound to nil at
the start of make-event expansion. To see why, consider for example the
community book books/make-event/proof-by-arith.lisp. This book
introduces a macro, proof-by-arith, that expands to a call of make-event. This make-event form expands by trying to prove a given
theorem using a succession of included arithmetic books, until the proof
succeeds. Now proofs are skipped during the Pcertify procedure, and if proofs
were also skipped during make-event expansion within that procedure, the
first arithmetic book's include-book form would always be saved
because the theorem's proof ``succeeded'' (as it was skipped!). Of course,
the theorem's proof could then easily fail during the Convert step. If you
really want to inhibit proofs during make-event expansion in the Pcertify
step, consider using a form such as the following: (state-global-let*
((ld-skip-proofsp nil)) ...).
Finally, we describe what it means for there to be a valid certificate file for including a certified book. Normally, this is a file
with extension .cert. However, if that .cert file does not exist,
then ACL2 looks for a .pcert0 file instead; and if that also does not
exist, it looks for a .pcert1 file. (To see why does the .pcert0
file take priority over the .pcert1 file, note that the Convert procedure
copies a .pcert0 file to a .pcert1 file, so both might exist —
but the .pcert1 file might be incomplete if copying is in progress.)
Once the candidate certificate file is thus selected, it must be valid in
order for the book to be considered certified (see certificate). For
the certificate file as chosen above, then in order for a compiled file to be
loaded, it must be at least as recent as that certificate file.
Again, as discussed above, a .pcert0 or .pcert1 file may serve as
a valid certificate file when the .cert file is missing. But when that
happens, a warning may be printed that a ``provisionally certified'' book has
been included. No such warning occurs if environment variable ACL2_PCERT
has a non-empty value, or if that warning is explicitly inhibited (see set-inhibit-warnings and see set-inhibit-output-lst).
