With classification and regression learning, we employ ranking approaches for the constraint solving backends of the ProB model checker to assess the most suited backend to use for a given constraint. In case the top ranked backend fails to solve the constraint, the predicted ranking yields a clear order of which backend to utilise in a second attempt. Our trained predictors achieve an overall runtime overhead of only 7 % while a static order of backends results in an overhead of 8.5 %. Thus, we are confident in our approach as it is more dynamic and ofers potential to increase performance in the future.
predicted backend fails to satisfy or invalidate the constraint, a ranking clearly defines which backend to use for solving the constraint next.
In the following, we briefly discuss related work in Section 2. Our training data, used machine learning algorithms, and experimental results are summarised in Sections 3 and 4. The paper concludes in Section 5. The code for our experiments and our full results are available on Github: https://github.com/jdnklau/ranked-runtime-predictions-for-probs-backends.
Previous work investigated classification approaches [
We utilise the set of 597,134 training constraints collected over the ProB public examples1 by
Dunkelau et al. [
Given a possible backend response ∈ {valid, invalid, unknown, timeout, error} and a
measured runtime over each backend with a timeout of (in our application 25 s), each constraint
was labelled with one cost value per backend given by the cost function by Healy et al. [
+ ⎪⎩ + 2 if ∈ {valid, invalid} if = unknown if ∈ {timeout, error} (1)
As we want to favour faster backends over slower backends yet also definitive responses over unknown, timeout, or error responses in our ranking, we utilise the cost function from Equation (1). This reduces our goal to predicting the backends in ascending order of their costs. We can make use of three diferent approaches.
Multi-output regression is the approach followed by Healy et al. [
In separate single-output regression only one independent regressor is trained per backend. This allows for easier maintenance in the long run as optimizing performance for a single backend does not impact the other regressors. Adding a new backend into the portfolio also only consists of adding a new, optimised regressor instead of retraining the singular regressor over all backends.
A non-regression approach is ranking classification. Each possible ranking is defined as its own class, leading to 6 classes in total. This however is even less extendable than the multioutput regression as adding a new backend not only leads to retraining of the whole classifier but also increases the amount of classes by a factorial factor, losing feasibility by increasing number of backends. We also lose the information of predicted runtime cost per backend.
We compared the performances of multiple machine learning algorithms, employing a total of six
diferent algorithms: linear regression (LR) [
To quantify the performance of our ranking predictors we utilise the following two metrics. The
ifrst is the double normalised discounted cumulative gain (dnDCG) [
DCG = ∑︁ 2rel − 1 , =1 log2( + 1)
DCG DCG* nDCG = dnDCG = nDCG − nDCG 1 − nDCG (2) for a ranking of length , where rel is the relevance of the th backend, DCG* is the DCG value for the ideal ranking, and nDCG is the nDCG value for the worst ranking. The second metric is the usage duration comparison value (UDC) which we defined ourselves to assess the runtime overhead introduced by predicting a non-ideal ranking. This is motivated by observing that, e.g., picking the second best backend first might only add a couple nano seconds to the final runtime and thus introduces no significant overhead. If the firstly ranked backend fails to return a definite answer we would query the remaining backends in order of their ranking, until either (3) one gives a definite answer or we run out of backends. Let the time used up by this query be ˆ for a constraint . Let the query time over the ideal ranking be * . We define the UDC as ∑︀=1
ˆ
UDC = ∑︀=1 * ∈ [1, ∞) .
Table 1 shows the best performing models per approach. While we investigated multiple
machine learning algorithms, it stands out that random forests took part in all the best achieved
performances. This is inline with the results, observations, and decisions from related work [
In comparison, a static algorithm that always uses the ranking CLP(FD) ≻ Z3 ≻ Kodkod already yields a UDC of 1.085, competing with our predictors. However, our approach is more dynamic and allows for improvement due to further tuning or a more refined feature set.
We trained multiple predictors for ranking the ProB backends by ascending, weighted, expected runtime. Our results show not much of a diference between the approaches of single-output regression, multi-output regression, and ranking classification, while the single-output regression still represents the most flexible approach and should be focus of research going forward. Finally, we achieved performance values of a double normalised discounted cumulative gain of up to 0.81 and an usage diference comparison value of up to 1.07. While a dummy approach which always prefers a single, static ranking competes with our learned predictors we are confident that our method proves more valuable going forward as it allows for further tuning.
Computational support and infrastructure was provided by the “Centre for Information and Media Technology” (ZIM) at the University of Düsseldorf (Germany).