Implementing and evaluating candidate-based invariant generation
File(s)
Accepted version
Author(s)
Betts, A
Chong, N
Deligiannis, P
Donaldson, AF
Ketema, J
Type
Journal Article
Abstract
The discovery of inductive invariants lies at the heart of static program verification. Presently, many automatic solutions to
inductive invariant generation are inflexible, only applicable to certain classes of programs, or unpredictable. An automatic technique
that circumvents these deficiencies to some extent is
candidate-based invariant generation
, whereby a large number of candidate
invariants are guessed and then proven to be inductive or rejected using a sound program analyser. This paper describes our efforts to
apply candidate-based invariant generation in GPUVerify, a static checker of programs that run on GPUs. We study a set of
383
GPU
programs that contain loops, drawn from a number of open source suites and vendor SDKs. Among this set,
253
benchmarks require
provision of loop invariants for verification to succeed.
We describe the methodology we used to incrementally improve the invariant generation capabilities of GPUVerify to handle these
benchmarks, through
candidate-based invariant generation
, whereby potential program invariants are speculated using cheap static
analysis and subsequently either refuted or proven. We also describe a set of experiments that we used to examine the effectiveness of
our rules for candidate generation, assessing rules based on their
generality
(the extent to which they generate candidate invariants),
hit
rate
(the extent to which the generated candidates hold),
effectiveness
(the extent to which provable candidates actually help in allowing
verification to succeed), and
influence
(the extent to which the success of one generation rule depends on candidates generated by
another rule). We believe that our methodology for devising and evaluation candidate generation rules may serve as a useful framework
for other researchers interested in candidate-based invariant generation.
The candidates produced by GPUVerify help to verify
231
of these
253
programs. An increase in precision, however, has created
sluggishness in GPUVerify because more candidates are generated and hence more time is spent on computing those which are
inductive invariants. To speed up this process, we have investigated four under-approximating program analyses that aim to reject false
candidates quickly and a framework whereby these analyses can run in sequence or in parallel. Across two platforms, running Windows
and Linux, our results show that the best combination of these techniques running
sequentially
speeds up invariant generation across
our benchmarks by
1
.
17
×
(Windows) and
1
.
01
×
(Linux), with per-benchmark best speedups of
93
.
58
×
(Windows) and
48
.
34
×
(Linux),
and worst slowdowns of
10
.
24
×
(Windows) and
43
.
31
×
(Linux). We find that
parallelising
the strategies marginally improves overall
invariant generation speedups to
1
.
27
×
(Windows) and
1
.
11
×
(Linux), maintains good best-case speedups of
91
.
18
×
(Windows) and
44
.
60
×
(Linux), and, importantly, dramatically reduces worst-case slowdowns to
3
.
15
×
(Windows) and
3
.
17
×
(Linux).
inductive invariant generation are inflexible, only applicable to certain classes of programs, or unpredictable. An automatic technique
that circumvents these deficiencies to some extent is
candidate-based invariant generation
, whereby a large number of candidate
invariants are guessed and then proven to be inductive or rejected using a sound program analyser. This paper describes our efforts to
apply candidate-based invariant generation in GPUVerify, a static checker of programs that run on GPUs. We study a set of
383
GPU
programs that contain loops, drawn from a number of open source suites and vendor SDKs. Among this set,
253
benchmarks require
provision of loop invariants for verification to succeed.
We describe the methodology we used to incrementally improve the invariant generation capabilities of GPUVerify to handle these
benchmarks, through
candidate-based invariant generation
, whereby potential program invariants are speculated using cheap static
analysis and subsequently either refuted or proven. We also describe a set of experiments that we used to examine the effectiveness of
our rules for candidate generation, assessing rules based on their
generality
(the extent to which they generate candidate invariants),
hit
rate
(the extent to which the generated candidates hold),
effectiveness
(the extent to which provable candidates actually help in allowing
verification to succeed), and
influence
(the extent to which the success of one generation rule depends on candidates generated by
another rule). We believe that our methodology for devising and evaluation candidate generation rules may serve as a useful framework
for other researchers interested in candidate-based invariant generation.
The candidates produced by GPUVerify help to verify
231
of these
253
programs. An increase in precision, however, has created
sluggishness in GPUVerify because more candidates are generated and hence more time is spent on computing those which are
inductive invariants. To speed up this process, we have investigated four under-approximating program analyses that aim to reject false
candidates quickly and a framework whereby these analyses can run in sequence or in parallel. Across two platforms, running Windows
and Linux, our results show that the best combination of these techniques running
sequentially
speeds up invariant generation across
our benchmarks by
1
.
17
×
(Windows) and
1
.
01
×
(Linux), with per-benchmark best speedups of
93
.
58
×
(Windows) and
48
.
34
×
(Linux),
and worst slowdowns of
10
.
24
×
(Windows) and
43
.
31
×
(Linux). We find that
parallelising
the strategies marginally improves overall
invariant generation speedups to
1
.
27
×
(Windows) and
1
.
11
×
(Linux), maintains good best-case speedups of
91
.
18
×
(Windows) and
44
.
60
×
(Linux), and, importantly, dramatically reduces worst-case slowdowns to
3
.
15
×
(Windows) and
3
.
17
×
(Linux).
Date Issued
2018-07-01
Date Acceptance
2017-04-05
Citation
IEEE Transactions on Software Engineering, 44 (7), pp.631-650
ISSN
1939-3520
Publisher
IEEE
Start Page
631
End Page
650
Journal / Book Title
IEEE Transactions on Software Engineering
Volume
44
Issue
7
Copyright Statement
© 20xx IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Sponsor
Commission of the European Communities
Engineering & Physical Science Research Council (E
Grant Number
287767
EP/K503733/1
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Engineering, Electrical & Electronic
Computer Science
Engineering
Formal verification
GPUs
invariant generation
GPU KERNELS
VERIFICATION
INFERENCE
0803 Computer Software
0806 Information Systems
Software Engineering
Publication Status
Published
Date Publish Online
2017-06-22