		Search-engine friendly clone of the ACL2 documentation.

Cert.pl

Distributed-builds

(Advanced) how to distribute ACL2 book building over a cluster of machines.

Warning: getting a cluster set up and running smoothly is a significant undertaking. Aside from hardware costs, it may take significant energy to install and administer the system, and you will need to learn how to effectively use the queuing system. You'll probably also need to be ready to do some scripting to work around dumb problems. Think of this topic as: some hints that may help you, not a usable guide to setting up a cluster.

At Centaur, cert.pl is successfully used within a rocks cluster environment, using the open-source queuing system torque and the maui scheduler. This clustering software allows for the submission of PBS scripts as jobs. To support this cluster, cert.pl has certain features.

Support for PBS directives

For one, cert.pl writes out a PBS script for each book it is going to certify. These scripts look like ordinary shell scripts (so they work fine for use in non-cluster environments), but they contain special comments that the clustering software understands.

These comments allow you to say, e.g., how much memory a job is going to take, so that if a job takes more than its allotted memory, the clustering software may choose to kill it. The clustering software also uses this memory limit to ensure that when it allocates a job to a machine, the machine will have enough physical machine to run the job.

This is really very useful. If you let a machine start swapping into the gigabytes, at worst you will need to physically reset it, because it dies a special kind of horrible death where its load average is 50 and you can't even "kill" anything. In a slightly better case, you may run into the Linux overcommit and OOM killer features, which are also really awful. My favorite article on the topic, from back before we had the cluster and were running into this frequently, is here.

At any rate, when cert.pl writes out the scripts to certify books, it includes some PBS commands that say how much memory the book is expected to take. This is done by a stupid heuristic: we search for set-max-mem lines; if no such line is found we say the book will take 4 GB, and otherwise we reserve I think 2-3 GB more than the set-max-mem line calls for. This extra padding is because set-max-mem only affects the heap, and doesn't account for the stacks, and we typically build a CCL image with large stacks, as explained in centaur/ccl-config.lsp, and also because set-max-mem is sort of best thought of as a soft cap, anyway.

Support for a Queuing System

Besides this support for PBS directives, cert.pl also consults an environment variable $STARTJOB. If this variable isn't set, we default it to your current $SHELL. When we run ACL2 jobs, we basically use:

$STARTJOB -c "acl2 < certify-commands &> foo.cert.out"

So, given a suitable startjob command, cert.pl can automatically distribute the jobs to your cluster. A suitable command is one that:

Accepts the -c syntax or (without -c) accepts a script.
Waits for the job to finish.
Exits "transparently", i.e., with the exit code of the job.

A suitable startjob command does not need to support any input/output redirection; we embed that into the command itself.

Setting environment variables visible to the queuing system

The build system scans books for lines containing the pattern

; cert-env: (varname1=value1, varname2, ...)

Each of these varname/value pairs are set in the environment before calling STARTJOB to build the book; these can therefore be set in such a way as to give information to the queuing system about how the book needs to be built. If a varname is included without a corresponding value, the value defaults to 1.

The build system also scan for some particular patterns to help define how much memory and time the book should need to be allocated. The following kinds of set-max-mem forms are recognized and used to generate the environment variable CERT_MAX_MEM:

(set-max-mem (expt 2 k))
(set-max-mem (* n (expt 2 30))) ;; N gigabytes
(set-max-mem (* (expt 2 30) n))

Additionally, the following pattern is scanned to set the environment variable CERT_MAX_TIME. Note this isn't a real ACL2 event, so it should occur in a comment:

; (set-max-time N)

Support for NFS Lag

We originally found that our builds would often "fail" due to the following scenario:

Head node: Makefile submits book A to the queue.
Compute node: Certifies book A successfully.
Head node: startjob returns control to the Makefile.
Head node: Makefile runs ls A.cert to check success.
Head node: ls fails because NFS isn't up to date.
Make thinks there's been a problem and dies.
Moments later A.cert shows up.

To avoid this, cert.pl now has special support for NFS lag. We now use exit codes instead of files to determine success. In cases where the exit code says the job completed successfully, we wait until A.cert becomes visible to the head node before returning control to the Makefile.