PROVISIONAL-CERTIFICATION

Major Section:  BOOKS

Provisional certification is a process that can increase parallelism at the system level, 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.

Perhaps the easiest way to invoke provisional certification is with the `make' approach supported by the ACL2 system; see book-makefiles. 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

(export ACL2_PCERT=t ; time make -j 4)

ACL2_PCERT = t

A successful `make' will result in creati See community books file books/system/pcert/Makefile for an example.

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.

o 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).

o 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.

o 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.

o Pcertify books "C", "B",and then "A", sequentially, skipping proofs but doing compilation.

o 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.

o 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 checksums 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 checksum information. Of course, the automatic dependency analysis provided by `make' avoids accidental problems of this sort. And, checksum 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 the ACL2 `make' approach to do provisional certification, 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

make -j 4 ACL2_BOOKS_PCERT_ARG_T='sub mid'

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 the standard ACL2 `make'-based provisional 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 the standard ACL2 `make'-based approach, 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).