Simplifying Bug Finding in Concurrent Programs
T
r
u
c
L
.
N
g
u
y
e
n
1
,
P
e
t
e
r
S
c
h
r
a
m
m
e
l
2
,
B
e
r
n
d
F
i
s
c
h
e
r
3
,
S
a
l
v
a
t
o
r
e
L
a
T
o
r
r
e
4
,
G
e
n
n
a
r
o
P
a
r
l
a
t
o
1
1
University of Southampton, United Kingdom
2
University of Sussex, United Kingdom
3
Stellenbosch University, South Africa
4
Universita degli Studi di Salerno, Italy
P
a
r
a
l
l
e
l
B
u
g
-
f
i
n
d
i
n
g
i
n
C
o
n
c
u
r
r
e
n
t
P
r
o
g
r
a
m
s
v
i
a
R
e
d
u
c
e
d
I
n
t
e
r
l
e
a
v
i
n
g
I
n
s
t
a
n
c
e
s
C
o
n
c
u
r
r
e
n
c
y
m
a
k
e
s
b
u
g
f
i
n
d
i
n
g
h
a
r
d
e
r
.
S
t
a
t
e
s
p
a
c
e
e
x
p
l
o
s
i
o
n
(
i
.
e
.
,
l
a
r
g
e
n
u
m
b
e
r
o
f
i
n
t
e
r
l
e
a
v
i
n
g
s
)
:
(… and many more)
Problem: modern hardware means concurrency is everywhere
software is increasingly concurrent
x = *;
y = 0;
if(x != y)
x = x-y;
x = x + 1;
z = x * y;
y = *;
x = 0;
if(x != y)
y = y-x;
y = y + 1;
z = x * y;
C
o
n
c
u
r
r
e
n
c
y
m
a
k
e
s
b
u
g
f
i
n
d
i
n
g
e
a
s
i
e
r
.
C
o
n
c
u
r
r
e
n
t
h
a
r
d
w
a
r
e
a
l
l
o
w
s
u
s
t
o
r
u
n
m
a
n
y
(
s
m
a
l
l
e
r
)
a
n
a
l
y
s
i
s
t
a
s
k
s
i
n
p
a
r
a
l
l
e
l
:
C
o
n
c
u
r
r
e
n
c
y
m
a
k
e
s
b
u
g
f
i
n
d
i
n
g
e
a
s
i
e
r
.
C
o
n
c
u
r
r
e
n
t
h
a
r
d
w
a
r
e
a
l
l
o
w
s
u
s
t
o
r
u
n
m
a
n
y
(
s
m
a
l
l
e
r
)
a
n
a
l
y
s
i
s
t
a
s
k
s
i
n
p
a
r
a
l
l
e
l
:
H
o
w
c
a
n
w
e
p
a
r
t
i
t
i
o
n
a
t
a
s
k
i
n
t
o
i
n
d
e
p
e
n
d
e
n
t
s
m
a
l
l
e
r
t
a
s
k
s
?
?
?
?
?
?
?
?
?
?
?
?
?
?
?
?
?
?
?
S
t
r
a
t
e
g
y
c
o
m
p
e
t
i
t
i
o
n
v
s
.
t
a
s
k
c
o
m
p
e
t
i
t
i
o
n
S
t
r
a
t
e
g
y
c
o
m
p
e
t
i
t
i
o
n
:
r
u
n
d
i
f
f
e
r
e
n
t
s
e
t
t
i
n
g
s
o
n
s
a
m
e
t
a
s
k
(
f
i
r
s
t
c
o
u
n
t
e
r
e
x
a
m
p
l
e
“
w
i
n
s
”
a
n
d
a
b
o
r
t
s
o
t
h
e
r
t
a
s
k
s
)
T
h
i
s
w
o
r
k
:
T
a
s
k
c
o
m
p
e
t
i
t
i
o
n
:
r
u
n
s
a
m
e
p
r
o
v
e
r
(
s
e
t
t
i
n
g
)
o
n
d
i
f
f
e
r
e
n
t
t
a
s
k
s
H
o
w
c
a
n
w
e
p
a
r
t
i
t
i
o
n
a
t
a
s
k
i
n
t
o
i
n
d
e
p
e
n
d
e
n
t
s
m
a
l
l
e
r
t
a
s
k
s
?
“anticipate the appearance of systems with large numbers of CPU
cores, but without matching increases in clockspeeds… describe a
model checking strategy that leverages this trend”
R
e
d
u
c
e
d
i
n
t
e
r
l
e
a
v
i
n
g
i
n
s
t
a
n
c
e
s
O
u
r
g
o
a
l
:
O
u
r
s
o
l
u
t
i
o
n
:
S
p
l
i
t
s
e
t
o
f
i
n
t
e
r
l
e
a
v
i
n
g
s
I
k
(
P
)
i
n
t
o
s
u
b
s
e
t
s
t
h
a
t
c
a
n
b
e
a
n
a
l
y
z
e
d
s
y
m
b
o
l
i
c
a
l
l
y
a
n
d
i
n
d
e
p
e
n
d
e
n
t
l
y
.
…
D
e
r
i
v
e
p
r
o
g
r
a
m
v
a
r
i
a
n
t
s
P
ϑ
t
h
a
t
a
l
l
o
w
c
o
n
t
e
x
t
s
w
i
t
c
h
e
s
o
n
l
y
i
n
s
u
b
s
e
t
s
o
f
s
t
a
t
e
m
e
n
t
s
(
t
i
l
e
s
)
s
.
t
.
I
k
(
P
)
=
U
ϑ
I
k
(
P
ϑ
)
.
R
e
d
u
c
e
d
i
n
t
e
r
l
e
a
v
i
n
g
i
n
s
t
a
n
c
e
s
O
u
r
g
o
a
l
:
O
u
r
s
o
l
u
t
i
o
n
:
S
p
l
i
t
s
e
t
o
f
i
n
t
e
r
l
e
a
v
i
n
g
s
I
k
(
P
)
i
n
t
o
s
u
b
s
e
t
s
t
h
a
t
c
a
n
b
e
a
n
a
l
y
z
e
d
s
y
m
b
o
l
i
c
a
l
l
y
a
n
d
i
n
d
e
p
e
n
d
e
n
t
l
y
.
D
e
r
i
v
e
p
r
o
g
r
a
m
v
a
r
i
a
n
t
s
P
ϑ
t
h
a
t
a
l
l
o
w
c
o
n
t
e
x
t
s
w
i
t
c
h
e
s
o
n
l
y
i
n
s
u
b
s
e
t
s
o
f
s
t
a
t
e
m
e
n
t
s
(
t
i
l
e
s
)
s
.
t
.
I
k
(
P
)
=
U
ϑ
I
k
(
P
ϑ
)
.
…
T
i
l
i
n
g
T
h
r
e
a
d
s
T
i
l
i
n
g
t
h
r
e
a
d
s
A
s
s
u
m
p
t
i
o
n
:
b
o
u
n
d
e
d
c
o
n
c
u
r
r
e
n
t
p
r
o
g
r
a
m
s
•
finite #threads, fixed (but arbitrary) schedule
–
captures all bounded round-robin computations for given bound
•
bugs manifest within very few rounds
[Musuvathi, Qadeer, PLDI’07]
T
i
l
i
n
g
t
h
r
e
a
d
s
A
s
s
u
m
p
t
i
o
n
:
b
o
u
n
d
e
d
c
o
n
c
u
r
r
e
n
t
p
r
o
g
r
a
m
s
•
finite #stmts
•
control can only go forward
–
simplifies analysis and tiling
T
i
l
i
n
g
t
h
r
e
a
d
s
T
i
l
e
s
:
•
t
i
l
e
:
(
c
o
n
t
i
g
u
o
u
s
)
s
u
b
s
e
t
o
f
v
i
s
i
b
l
e
s
t
a
t
e
m
e
n
t
s
–
other tile types possible: random subsets, data-flow driven, …
•
t
i
l
i
n
g
:
p
a
r
t
i
t
i
o
n
o
f
p
r
o
g
r
a
m
i
n
t
o
t
i
l
e
s
•
u
n
i
f
o
r
m
w
i
n
d
o
w
t
i
l
i
n
g
:
a
l
l
t
i
l
e
s
h
a
v
e
s
a
m
e
s
i
z
e
–
number of visible statements
T
0
T
N
T
N-1
T
1
…
stmt
1
;
stmt
2
;
...
stmt
t-1
;
stmt
t
;
stmt
1
;
stmt
2
;
...
stmt
u-1
;
stmt
u
;
stmt
1
;
stmt
2
;
...
stmt
v-1
;
stmt
v
;
stmt
1
;
stmt
2
;
...
stmt
s-1
;
stmt
s
;
T
i
l
i
n
g
t
h
r
e
a
d
s
T
i
l
e
s
e
l
e
c
t
i
o
n
:
•
z
-
s
e
l
e
c
t
i
o
n
:
s
u
b
s
e
t
o
f
z
t
i
l
e
s
f
o
r
e
a
c
h
t
h
r
e
a
d
–
c
o
n
t
e
x
t
s
w
i
t
c
h
e
s
a
r
e
o
n
l
y
a
l
l
o
w
e
d
f
r
o
m
s
e
l
e
c
t
e
d
t
i
l
e
s
context switches can only go into other selected tiles
(or first thread statement)
•
e
a
c
h
z
-
s
e
l
e
c
t
i
o
n
s
p
e
c
i
f
i
e
s
a
r
e
d
u
c
e
d
i
n
t
e
r
l
e
a
v
i
n
g
i
n
s
t
a
n
c
e
T
0
T
N
T
N-1
T
1
…
stmt
1
;
stmt
2
;
...
stmt
t-1
;
stmt
t
;
stmt
1
;
stmt
2
;
...
stmt
u-1
;
stmt
u
;
stmt
1
;
stmt
2
;
...
stmt
v-1
;
stmt
v
;
stmt
1
;
stmt
2
;
...
stmt
s-1
;
stmt
s
;
…
T
i
l
i
n
g
t
h
r
e
a
d
s
C
o
m
p
l
e
t
e
n
e
s
s
o
f
s
e
l
e
c
t
i
o
n
s
:
•
each interleaving with
k
context switches can be covered
by a ⌈
k
/2⌉-selection
ϑ
ϵ
Θ
P
–
each thread can only switch out at most
⌈
k
/2⌉
times
set of all
⌈
k
/2⌉-selections together covers all interleavings
with
k
context switches:
I
k
(
P
) = U
ϑ
I
k
(
P
ϑ
)
T
0
T
N
T
N-1
T
1
…
stmt
1
;
stmt
2
;
...
stmt
t-1
;
stmt
t
;
stmt
1
;
stmt
2
;
...
stmt
u-1
;
stmt
u
;
stmt
1
;
stmt
2
;
...
stmt
v-1
;
stmt
v
;
stmt
1
;
stmt
2
;
...
stmt
s-1
;
stmt
s
;
…
T
i
l
i
n
g
t
h
r
e
a
d
s
C
o
m
p
l
e
t
e
n
e
s
s
o
f
s
e
l
e
c
t
i
o
n
s
:
•
number of selections grows exponentially
sampling
T
0
T
N
T
N-1
T
1
…
stmt
1
;
stmt
2
;
...
stmt
t-1
;
stmt
t
;
stmt
1
;
stmt
2
;
...
stmt
u-1
;
stmt
u
;
stmt
1
;
stmt
2
;
...
stmt
v-1
;
stmt
v
;
stmt
1
;
stmt
2
;
...
stmt
s-1
;
stmt
s
;
…
V
E
R
I
S
M
A
R
T
(
V
e
r
i
f
i
c
a
t
i
o
n
S
m
a
r
t
)
V
E
R
I
S
M
A
R
T
i
m
p
l
e
m
e
n
t
s
s
w
a
r
m
v
e
r
i
f
i
c
a
t
i
o
n
b
y
t
a
s
k
c
o
m
p
e
t
i
t
i
o
n
f
o
r
m
u
l
t
i
-
t
h
r
e
a
d
e
d
C
.
Target:
•
C
p
r
o
g
r
a
m
s
w
i
t
h
“
r
a
r
e
”
c
o
n
c
u
r
r
e
n
c
y
b
u
g
s
,
i
.
e
.
,
–
“
l
a
r
g
e
”
n
u
m
b
e
r
o
f
i
n
t
e
r
l
e
a
v
i
n
g
s
–
“
f
e
w
”
i
n
t
e
r
l
e
a
v
i
n
g
s
l
e
a
d
t
o
a
b
u
g
•
a
u
t
o
m
a
t
i
c
b
u
g
-
f
i
n
d
i
n
g
(
b
o
u
n
d
e
d
a
n
a
l
y
s
i
s
,
n
o
t
c
o
m
p
l
e
t
e
)
•
r
e
a
c
h
a
b
i
l
i
t
y
–
assertion failure
–
out-of-bound array, division-by-zero, …
–
linearizability → reachability
[Bouajjani et al., POPL’15, ICALP’15]
Approach:
•
source-to-source translation to generate instances (for tiling)
–
instances are bounded concurrent programs
•
use cluster to run Lazy-CSeq over instances
[Inverso et al., CAV’14]
V
E
R
I
S
M
A
R
T
a
r
c
h
i
t
e
c
t
u
r
e
•
I
n
l
i
n
e
/
u
n
w
i
n
d
m
o
d
u
l
e
:
–
concurrent program
⟶
bounded concurrent program
•
N
u
m
e
r
i
c
a
l
l
a
b
e
l
s
m
o
d
u
l
e
:
–
inject numerical labels at each visible statement
•
I
n
s
t
r
u
m
e
n
t
m
o
d
u
l
e
:
–
instrument the code with guarded commands (
yield
) that can
enable/disable context switch points at numerical labels
•
S
p
l
i
t
m
o
d
u
l
e
:
–
generate variants with configuration from tiling and #tiles
–
randomize number of generated variants when #variants is large
W
h
y
d
o
e
s
t
h
i
s
w
o
r
k
?
Remember:
Each
P
ϑ
allows only a (small) subset of P’s interleavings
We assume bugs are rare,
•
so for most
ϑ
,
P
ϑ
does not exhibit the bug…
•
… and the analysis will run out of time
•
but if
P
ϑ
does exhibit the bug…
•
… the analysis will find it quick(er)
Hence,
•
overall CPU time consumption goes (way) up…
•
… but with enough cores CPU time is free and…
•
mean wall clock time to find failure goes down
E
x
p
e
r
i
m
e
n
t
a
l
E
v
a
l
u
a
t
i
o
n
E
x
p
e
r
i
m
e
n
t
s
o
n
l
o
c
k
-
f
r
e
e
d
a
t
a
s
t
r
u
c
t
u
r
e
s
eliminationstack
:
•
ABA problem: requires 7 threads for exposure
•
L
a
z
y
-
C
S
e
q
c
a
n
f
i
n
d
b
u
g
i
n
~
1
3
h
a
n
d
4
G
B
–
#unwind=1, #rounds=2, #threads=8,
size=52 visible stmts
•
all other tools fail
safestack
:
•
ABA problem:
requires context bound of 5
•
L
a
z
y
-
C
S
e
q
c
a
n
f
i
n
d
b
u
g
i
n
~
7
h
a
n
d
6
.
5
G
B
–
#unwind=3, #rounds=4, #threads=4, size=152 visible stmts
•
all other tools fail
e
l
i
m
i
n
a
t
i
o
n
s
t
a
c
k
:
R
e
s
u
l
t
s
•
Lazy-CSeq: 46764 sec, 4.2 GB
•
CBMC (sequential): 80.8 sec, 0.7 GB
–
average over 3000 interleavings, bug not found
fastest instances
very fast – 1000x
average still very
fast – 40x
some slowdown for
larger tile sizes – 10x
reduced memory
consumption – 4x
high fraction of bug-
exposing instances
e
l
i
m
i
n
a
t
i
o
n
s
t
a
c
k
:
E
x
p
e
c
t
e
d
b
u
g
f
i
n
d
i
n
g
t
i
m
e
bug found with
99% probability,
5 cores, < 500sec
1
0
0
x
s
p
e
e
d
-
u
p
!
s
a
f
e
s
t
a
c
k
(
S
C
)
:
R
e
s
u
l
t
s
•
Lazy-CSeq: 24139 sec, 6.6 GB
•
CBMC (sequential): 55.4 sec, 0.7 GB
–
average over 3000 interleavings, bug not found
similar picture, but less advantage for V
ERI
S
MART
lower fraction of bug-
exposing instances
than eliminationstack
…but boosted with
larger tile sizes
s
a
f
e
s
t
a
c
k
(
S
C
)
:
E
x
p
e
c
t
e
d
b
u
g
f
i
n
d
i
n
g
t
i
m
e
bug found with 95%
probability,
~32 cores, ~1300sec
smaller tiles
take longer
2
5
x
s
p
e
e
d
-
u
p
!
s
a
f
e
s
t
a
c
k
(
P
S
O
)
:
E
x
p
e
c
t
e
d
b
u
g
f
i
n
d
i
n
g
t
i
m
e
get some speed-up (2x), even
though average time per instance
is higher than full analysis time
PSO easier than SC
C
o
n
c
l
u
s
i
o
n
s
•
first task-competitive swarm verification approach
•
exploits availability of many cores to reduce
mean wall clock
time to find failure
–
allows us to handle very hard problems
–
high speed-ups already for 5-50 cores
•
reduced interleaving instances boost bug-finding capabilities
F
u
t
u
r
e
W
o
r
k
•
production-quality implementation based on LLVM
•
other backends (testing)
•
other tiling styles
•
fast over-approximations to filter out safe instances
Joint work with…
Handling concurrency in software development poses challenges due to state space explosion. This work discusses how reduced interleaving instances and concurrent hardware can make bug finding easier by analyzing smaller independent tasks in parallel. Strategies for task competition and model checking are also explored.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Parallel Bug-finding in Concurrent Programs via Reduced Interleaving Instances Truc L. Nguyen1, Peter Schrammel2, Bernd Fischer3, Salvatore La Torre4, Gennaro Parlato1 1 University of Southampton, United Kingdom 2 University of Sussex, United Kingdom 3 Stellenbosch University, South Africa 4 Universita degli Studi di Salerno, Italy
Concurrency makes bug finding harder. State space explosion (i.e., large number of interleavings): x = *; y = *; y = 0; x = 0; if(x != y) if(x != y) x = x-y; y = y-x; x = x + 1; y = y + 1; z = x * y; z = x * y; ( and many more) Problem: modern hardware means concurrency is everywhere software is increasingly concurrent
Concurrency makes bug finding easier. Concurrent hardware allows us to run many (smaller) analysis tasks in parallel: SMALLER TASK SMALLER TASK SMALLER TASK SMALLER TASK ANALYSIS TASK SMALLER TASK SMALLER TASK
Concurrency makes bug finding easier. Concurrent hardware allows us to run many (smaller) analysis tasks in parallel: ??? ??? ??? ??? ??? ??? How can we partition a task into independent smaller tasks?
Strategycompetitionvs.task competition Strategy competition: run different settings on same task (first counterexample wins and aborts other tasks) anticipate the appearance of systems with large numbers of CPU cores, but without matching increases in clockspeeds describe a model checking strategy that leverages this trend This work: Task competition: run same prover (setting) on different tasks How can we partition a task into independent smaller tasks?
Reduced interleaving instances Our goal: Split set of interleavings Ik(P) into subsets that can be analyzed symbolically and independently. Our solution: Derive program variantsP that allow context switches only in subsets of statements (tiles) s.t. Ik(P) = U Ik(P ).
Reduced interleaving instances Our goal: Split set of interleavings Ik(P) into subsets that can be analyzed symbolically and independently. Our solution: Derive program variantsP that allow context switches only in subsets of statements (tiles) s.t. Ik(P) = U Ik(P ).
Tiling threads Assumption: bounded concurrent programs round 1 round 2 round 3 main() T0 T1 TN TN-1 round k finite #threads, fixed (but arbitrary) schedule captures all bounded round-robin computations for given bound bugs manifest within very few rounds [Musuvathi, Qadeer, PLDI 07]
Tiling threads Assumption: bounded concurrent programs TN TN-1 T0 T1 stmt1; stmt1; stmt1; stmt1; stmt2; stmt2; stmt2; stmt2; ... ... ... ... stmts-1; stmtt-1; stmtu-1; stmtv-1; stmts; stmtt; stmtu; stmtv; finite #stmts control can only go forward simplifies analysis and tiling
Tiling threads Tiles: TN TN-1 T0 T1 stmt1; stmt1; stmt1; stmt1; stmt2; stmt2; stmt2; stmt2; ... ... ... ... stmts-1; stmtt-1; stmtu-1; stmtv-1; stmts; stmtt; stmtu; stmtv; tile: (contiguous) subset of visible statements other tile types possible: random subsets, data-flow driven, tiling: partition of program into tiles uniform window tiling: all tiles have same size number of visible statements
Tiling threads Tile selection: TN TN-1 T0 T1 stmt1; stmt1; stmt1; stmt1; stmt2; stmt2; stmt2; stmt2; ... ... ... ... stmts-1; stmtt-1; stmtu-1; stmtv-1; stmts; stmtt; stmtu; stmtv; z-selection: subset of z tiles for each thread context switches are only allowed from selected tiles context switches can only go into other selected tiles (or first thread statement) each z-selection specifies a reduced interleaving instance
Tiling threads Completeness of selections: TN TN-1 T0 T1 stmt1; stmt1; stmt1; stmt1; stmt2; stmt2; stmt2; stmt2; ... ... ... ... stmts-1; stmtt-1; stmtu-1; stmtv-1; stmts; stmtt; stmtu; stmtv; each interleaving with k context switches can be covered by a k/2 -selection P each thread can only switch out at most k/2 times set of all k/2 -selections together covers all interleavings with k context switches: Ik(P) = U Ik(P )
Tiling threads Completeness of selections: TN TN-1 T0 T1 stmt1; stmt1; stmt1; stmt1; stmt2; stmt2; stmt2; stmt2; ... ... ... ... stmts-1; stmtt-1; stmtu-1; stmtv-1; stmts; stmtt; stmtu; stmtv; number of selections grows exponentially sampling
VERISMART (Verification Smart)
VERISMART implements swarm verification by task competition for multi-threaded C. Target: C programs with rare concurrency bugs, i.e., large number of interleavings few interleavings lead to a bug automatic bug-finding (bounded analysis, not complete) reachability assertion failure out-of-bound array, division-by-zero, linearizability reachability [Bouajjani et al., POPL 15, ICALP 15] Approach: source-to-source translation to generate instances (for tiling) instances are bounded concurrent programs use cluster to run Lazy-CSeq over instances [Inverso et al., CAV 14]
VERISMART architecture Inline/unwind module: concurrent program bounded concurrent program Numerical labels module: inject numerical labels at each visible statement Instrument module: instrument the code with guarded commands (yield) that can enable/disable context switch points at numerical labels Split module: generate variants with configuration from tiling and #tiles randomize number of generated variants when #variants is large
Why does this work? Remember: Each P allows only a (small) subset of P s interleavings We assume bugs are rare, so for most , P does not exhibit the bug and the analysis will run out of time but if P does exhibit the bug the analysis will find it quick(er) Hence, overall CPU time consumption goes (way) up but with enough cores CPU time is free and mean wall clock time to find failure goes down
Experimental Evaluation
Experiments on lock-free data structures eliminationstack: ABA problem: requires 7 threads for exposure Lazy-CSeq can find bug in ~13h and 4GB #unwind=1, #rounds=2, #threads=8, size=52 visible stmts all other tools fail safestack: ABA problem: requires context bound of 5 Lazy-CSeq can find bug in ~7h and 6.5GB #unwind=3, #rounds=4, #threads=4, size=152 visible stmts all other tools fail
eliminationstack: Results Lazy-CSeq: 46764 sec, 4.2 GB CBMC (sequential): 80.8 sec, 0.7 GB average over 3000 interleavings, bug not found fastest instances very fast 1000x reduced memory consumption 4x average still very fast 40x some slowdown for larger tile sizes 10x high fraction of bug- exposing instances
eliminationstack: Expected bug finding time 100x speed-up! bug found with 99% probability, 5 cores, < 500sec
safestack (SC): Results Lazy-CSeq: 24139 sec, 6.6 GB CBMC (sequential): 55.4 sec, 0.7 GB average over 3000 interleavings, bug not found lower fraction of bug- exposing instances than eliminationstack but boosted with larger tile sizes similar picture, but less advantage for VERISMART
safestack (SC): Expected bug finding time bug found with 95% probability, ~32 cores, ~1300sec 25x speed-up! smaller tiles take longer
safestack (PSO): Expected bug finding time PSO easier than SC get some speed-up (2x), even though average time per instance is higher than full analysis time
Conclusions first task-competitive swarm verification approach exploits availability of many cores to reduce mean wall clock time to find failure allows us to handle very hard problems high speed-ups already for 5-50 cores reduced interleaving instances boost bug-finding capabilities Future Work production-quality implementation based on LLVM other backends (testing) other tiling styles fast over-approximations to filter out safe instances
