Satis ability solvers can be embedded in applications to perform speci c formal reasoning tasks. CBMC, for example, is a bounded model checker for C and C++ that embeds SMT and SAT solvers to check internally generated formulae. Such solvers will be solely used to evaluate the class of formulae generated by the embedding application and therefore may bene t from domain-speci c parameter tuning. We propose the use of Bayesian optimisation for this purpose, which o ers a principled approach to black-box optimisation within limited resources. We demonstrate its use for optimisation of the solver embedded in CBMC speci cally for a collection of test harnesses in active industrial use, for which we have achieved a signi cant improvement over the default parameters.
al. [
In the following sections, we describe the relevant aspects of CBMC and Bayesian optimisation in detail, and our experiments. 2
CBMC is a bounded model checker for C and C++. CBMC performs code analysis using symbolic simulation, that is, it compiles code into logical formulae which are then sent to a solver for veri cation. With this method, assertions in the code can be veri ed statically. CBMC can also automatically generate assertions to check for common errors, such as bu er over ows, unsafe pointer access, memory leaks and arithmetic faults.
Test harness. Any project utilising CBMC will typically de ne a suite of test harnesses: carefully written C functions that act as entry-points for CBMC, along with speci cations for loop unrolling, function pointer destinations, variables that should be treated as non-deterministic and other optimisations. Each test harness should aim to formally verify some aspect of the code. Test harnesses may be viewed as static analysis unit tests. aws-c-common. aws-c-common is an open source library of commonly used datastructures and algorithms written in the C programming language, developed for use in the Amazon Web Services Software Development Kit and utilised by multiple projects. Given the central role of this library, the developers have committed considerable resources towards its formal veri cation using CBMC. At the time of writing, the library contains 166 CBMC test harnesses.
An example test harness from aws-c-common is shown in listing 1. This harness was designed to verify certain properties of aws_string_eq_ignore_case(): a function exported by the library. Of note, is the use of nondet_bool() to specify a non-deterministic value to CBMC. Non-deterministic values are also available for other datatypes, such as nondet_ushortint() for unsigned short integers. Such values represent input read from the environment and thus CBMC analyses the test harness for any possible choice of those values. void aws_string_eq_ignore_case_harness() { struct aws_string *str_a = nondet_bool() ? ,! ensure_string_is_allocated_bounded_length(MAX_STRING_LEN) : NULL; struct aws_string *str_b = nondet_bool() ? (nondet_bool() ? str_a : NULL) : ,! ensure_string_is_allocated_bounded_length(MAX_STRING_LEN); if (aws_string_eq_ignore_case(str_a, str_b) && str_a && str_b) { assert(aws_string_is_valid(str_a)); assert(aws_string_is_valid(str_b)); assert(str_a->len == str_b->len); } }
Listing 1: An example CBMC test harness from the aws-c-common library. aws_string_eq_ignore_case_harness struct aws_string *str_a; _Bool return_value_nondet_bool; return_value_nondet_bool = NONDET(__CPROVER_bool); struct aws_string *tmp_if_expr; IF !(return_value_nondet_bool != FALSE) THEN GOTO 1 struct aws_string *return_value_ensure_string_is_allocated_bounded_length; ensure_string_is_allocated_bounded_length((size_t)16); return_value_ensure_string_is_allocated_bounded_length = ,! ensure_string_is_allocated_bounded_length#return_value; dead ensure_string_is_allocated_bounded_length#return_value; tmp_if_expr = return_value_ensure_string_is_allocated_bounded_length;
GOTO 2 1: tmp_if_expr = (struct aws_string *)(void *)0; 2: str_a = tmp_if_expr;
...
Listing 2: A snippet from the goto le generated for the test harness shown in listing 1 from the aws-c-common library.
Goto les. CBMC uses a modi ed C compiler to compile source code down to a simpli ed format that is more amenable to further conversion into logical formulae. One such simpli cation, for example, is the unrolling of every loop to a speci ed number of iterations. The output les are called goto les in CBMC parlance. Formal veri cation of each test harness can be viewed as a two-stage process. First the test harness is compiled down to a goto le, and in the next stage the goto le is formally veri ed by conversion into logical formulae and checked by a solver. This project focuses on optimisation of the solver, and therefore we only need to generate the goto les for every test harness once. Only the second stage needs to be re-executed on any changes to the solver.
The goto les are binaries but a human readable text representation can be generated using CBMC. The text version of the goto le generated from the test harness shown in listing 1 spans 6231 lines. The large size is in part due to inclusion of other code from the library relevant to the harness in the goto le. A snippet of that text is shown in listing 2, which shows the rst few lines of the code generated for the test harness function.
1337 lines if the generated comments are excluded aws-batch-cbmc. Formal veri cation using CBMC is a computationally intensive task, but each test harness can be veri ed independently and in parallel. The developers of aws-c-common run their suite of CBMC tests for their continuous integration process and therefore require a fast turnaround from them. Their solution is to run each test harness as an independent batch process on a public cloud service, using the system from another open source project called aws-batch-cbmc.
MiniSat. CBMC can use multiple external SMT and SAT solvers to check internally generated
formulae, but its default solver is MiniSat | an open source SAT solver by Een et al. [
Bayesian Optimisation (BO) is a model-based black-box optimisation method, suitable for
optimising targets that are expensive to evaluate and lack an analytical form, as is the case
with typical SMT solvers. The optimisation target is modelled as an objective function, which
maps from the parameters of the target system to a performance metric. In this work, we will
often refer to the target system being optimised as the objective, with the target system being
MiniSat by default. Since the objective is a black-box, the shape of the objective function is
modelled using Gaussian Process (GP) regression [
Since Bayesian optimisation uses a machine learning model of the objective function, training data must be produced by testing the objective, initially at random. Subsequently, the optimisation process cycles between prediction, testing and training. Using the predictions from the latest model, a point of interest in the parameter space is chosen for testing, based on a criterion explained later in this section. The point is then evaluated on the objective. The result is a new item of data for the GP model to learn from, re ning its estimate of the objective. This process is repeated until a pre-de ned resource budget is consumed. The resource budget may be, for example, a xed number of iterations or wall-clock time. The persistent goal throughout the process is to intelligently search for better performing parameters.
Suppose the noisy black-box objective we wish to optimise using Bayesian optimisation is f , such that
y = f (x) + : Our goal, therefore, is to nd the point x that minimises f (x), where x is vector valued. In our setting, x is a vector of MiniSat parameter values, f measures the time spent in MiniSat, and the noise is due to the inherent non-determinism in the underlying system which in uences that measure. After some initial evaluations of f , Bayesian optimisation progresses in the following steps.
1. We treat all previous evaluations of f as training data and use a machine learning algorithm to build a predictive distribution of the values of y for any given x: p(yjx). With the use of a GP model, this distribution is Gaussian:
p(yjx) = N (yj (x); 2(x)): We build this distribution instead of a point estimate because many di erent estimates of f will be able to interpolate the points we have evaluated thus far. Two additional observations reinforce the need for this design: our measurements of the objective may be noisy; and the objective may be expensive to evaluate. When the objective is expensive to evaluate, as is the case with the work presented here, models of the objective will be derived from only a limited number of previous evaluations, and so we must account for the wider distribution of functions that could interpolate them. This is achieved by estimating the variance in addition to the mean. 2. We then use this distribution to build an acquisition function :
(x) = Ep(yjx)[U (yjx)] where U is the utility function, discussed in further detail below. The acquisition function is an inexpensive function that measures the expected utility of collecting data about any point x. The point x0 that maximises (x) is therefore the point to evaluate next. 3. We evaluate the objective at point x0, which adds to our training dataset, and we return to step 1. However, if the pre-allocated resources for the optimisation process are exhausted, we terminate the optimisation process. The minimum is extracted from the collection of points evaluated so far.
Utility function. Given a model of the objective function, consider the utility of evaluating points in the parameter space. The expectation as well as the uncertainty of the performance of any point in the parameter space as predicted by the model will vary. Some regions of the parameter space may be predicted with high expectation and low variance, wherein it may be useful to exploit the knowledge in the model in search of an optimal point. Alternatively, it may be bene cial to explore the parameter space in regions of high uncertainty in the model, to reduce the uncertainty in the model and to reveal potentially hidden optimal points. Exploration and exploitation are trade-o s within the pre-determined resource budget allocated for the optimisation process and must be carefully balanced. The choice of the point of interest during Bayesian optimisation at any stage is the point that maximises the acquisition function, which in turn uses the utility function. This acquisition function maps the model of the objective, which is a distribution over functions, to a single function which measures the expected utility of any point in the parameter space. The utility function is user-speci ed and can be used to control the balance between exploration and exploitation. A commonly used utility function is expected improvement. As explained before, we model our objective using GP regression and thereby obtain a distribution over functions f : where (x) is the mean function and K(x; x0) is the kernel covariance function. Suppose the minimum value of the objective that we have observed so far is v. The expected improvement utility function is then de ned as:
p(f ) = GP(f ; ; K)
U (x) = max(0; v
f (x)):
In e ect, this function rewards improvements proportionally, but does not reward degradations.
Discrete parameters. The Bayesian optimisation framework presented thus far is de ned for
continuous arguments to f . SMT solvers however often have discrete parameters. One solution
is to map the discrete parameters to integers, and yet model them in the GP regression as any
other real-valued parameter. When the objective needs to be evaluated, values supplied for the
discrete parameters can be rounded to integers. Rounding is a common workaround for integer
parameters in BO, but it can lead to problems, since the points that are actually evaluated are
di erent from the points that are modelled in the GP, as shown in work by Garrido-Merchan et
al. [
K0(xi; xj ) = K(T (xi); T (xj )); where T (x) rounds all integer-valued variables to the closest integer. Kernel covariance functions are discussed further in appendix A. In this work, we have used a commercially available BO framework described below, which provides built-in facilities for integer parameters. 4
In this work, we derive a parameter con guration for MiniSat that is optimised for a subset of the test harnesses in aws-c-common.
Goto les. Using aws-batch-cbmc, we completed one batch of the CBMC tests for aws-ccommon. This generated goto les for each of the test harnesses, which we used subsequently for all our tests. The system also reported time spent by the tests in the solver. The 166 tests spend a total of 4252 seconds in the solver, with a median of 1.2 seconds; of these, 159 tests spend less than 100 seconds, and another 4 spend less than 200 seconds. The remaining three tests are notably slower, taking up 488, 687 and 1005 seconds respectively in the solver. Tests and parameters. Given the resources available to us, we limited our sample of test harnesses to the 125 tests that spend the least amount of time in MiniSat. They represent 254 seconds of total time in the solver before optimisation. CBMC uses the SimpSolver in MiniSat, the parameters of which are shown in Table 1. We decided to limit our optimisation task to the SimpSolver speci c parameters, leaving the remaining MiniSat parameters at their defaults. Early experiments revealed that any search for more optimal parameters would maintain the three Boolean parameters asymm, rcheck and elim at their default settings of false, false and true respectively. Therefore, we decided to x these Boolean parameters to their default values and attempted to optimise only the remaining four parameters.
Objective function. Our goal was to nd a single parameter con guration for the whole set of test harnesses that could reduce the total time spent in evaluating the entire set. In more detail, suppose there are N test harnesses, and functions ti map from the parameters to the evaluation time of the test harness indexed by i, such that
ti : (g; c; s; r) 7! where g, c, s and r are the MiniSat parameters grow, cl-lim, sub-lim and simp-gc-frac respectively, and is the time spent in MiniSat when that test harness is evaluated. For any xed parameter con guration tuple (g0; c0; s0; r0), the objective function can simply be P ti(g0; c0; s0; r0). However, it is necessary to adjust the objective function with a timeout, since some parameter
Parameter
asymm rcheck elim grow con gurations will lead to a prohibitively long evaluation time. Therefore, when the objective begins to exceed the pre-de ned timeout, we take note and terminate it.
Implementation. Our implementation of the Bayesian optimisation process for this task
is in Matlab [
In the Matlab implementation of Bayesian optimisation, the objective function may return with NaN (not a number) to signify an error. Matlab builds an error model to accommodate errors in the objective, and this model can accommodate non-deterministic errors. We chose to model timeouts in our objective function as errors. Modelling timeouts as errors allows the Bayesian optimisation framework to avoid parameter spaces that frequently cause timeouts. In this scenario, the choice of the timeout value has trade-o s that must be considered. A short timeout will be resource e cient, reducing the time spent in parameter spaces that perform worse than the original ones. However, poor performing parameters are also informative of the shape of the objective function, but when they are modelled as errors due to the timeout, the GP model has less data to learn from. Based on the practical resources available to us, we speci ed a large timeout of 1200 seconds, more than four times the time taken by MiniSat in the original con guration.
Acquisition function & GP kernel. We used the expected improvement plus acquisition function from the framework in Matlab. This is similar to the expected improvement function described above, with a modi cation to avoid excessively exploiting an area. We used the default exploration ratio of 0:5. To obtain the maximum control over the Bayesian optimisation process in Matlab, we used the bayesopt function. However, the kernel covariance function used by this is xed to the Matern 5=2 kernel, which is brie y discussed in appendix A. The kernel hyperparameters are optimised internally by Matlab, and options to in uence them are unavailable. 5
It is necessary to specify bounds on the parameter space for the optimisation process. Our speci ed bounds are shown in Table 2. These bounds were chosen to be su ciently large, again based on preliminary experiments. In the case of cl-lim and sub-lim, it is possible to set both parameters to 1 in MiniSat, which then removes the clause limit and subsumption limit entirely, and we included that option in our parameter search space.
) 210 s d n o c e s ( e v i t c e jb 200 O d e v r e s b O m ium190 n i M 0 50 150
200 100
Iterations
After running the optimisation for a total of 210 iterations, which completed in thirty-four hours, the best discovered parameters are shown in Table 3. In comparison to the original parameters, these parameters reduce the time spent in the solver from 254 seconds to 184 seconds. Figure 1 plots the minimum objective that is observed until each iteration during Bayesian optimisation. The times presented here are a measure of the times spent in MiniSat. Each invocation of CBMC to evaluate a goto le will require relatively expensive additional steps such as the preparation of formulae, which are una ected by changes in MiniSat parameters.
We have optimised a collection of test harnesses all together to nd a single parameter con guration that, applied to all the tests, reduces the total time spent in the solver. An alternative is to optimise each test harness individually, and save the discovered parameters along with the test harness. When the suite of test harnesses is evaluated, each test harness can then be evaluated with individualised solver parameters. The trade-o between this approach and our presented approach depends on the resources available and the nature of the test harnesses. For a basic comparison, we optimised two randomly selected tests harnesses individually for the same number of iterations. The results, shown in Table 4, show that the optimised parameters discovered for the two are very di erent, and further improvement is achieved. aws_byte_buf_cat aws_hash_table_put 6
We have focussed on optimisation of the SimpSolver speci c parameters in this work. However, another eleven parameters are available in MiniSat, and tuning all parameters together may yield improved results.
We have shown that the use of Bayesian optimisation to tune parameters of the default solver in CBMC is e ective, and leads to a signi cant improvement in our experiments. Bayesian optimisation has shown to be successful in a variety of optimisation tasks, and our results show it can be e ectively used to tune parameters of satis ability solvers.
This work was developed during an internship at the Automated Reasoning Group of Amazon Web Services, supervised by John Harrison. Subsequent research was supported by the Engineering and Physical Sciences Research Council Doctoral Training studentship [reference number 1788755].
Test harness such that A
A kernel function is a real-valued function of two vector-valued arguments, for x; x0 2 where is some abstract space. Kernels may be viewed as a measure of similarity between the two arguments when the function is symmetric and non-negative. For example, the following kernel measures cosine similarity:
:
: 7! RD
k(x; x0) = (x)T (x0):
Kernel functions used as covariance functions in Gaussian processes must be positive de nite.
Such a kernel is called a Mercer kernel. Mercer's theorem (Minh et al. [
D X (xd However, this may lead to sample functions in the GP that are unrealistically smooth for practical optimisation problems. Instead, Snoek et al. recommend the use of the Matern 5/2 kernel: kM52(x; x0) = 0 1 + p5r2(x; x0) + 5 r2(x; x0) ef 3 p5r2(x;x0)g: