Title: Effect Summaries for Thread-Modular Analysis,
Abstract: We propose a novel guess-and-check principle to increase the efficiency of
thread-modular verification of lock-free data structures. We build on a
heuristic that guesses candidates for stateless effect summaries of programs by
searching the code for instances of a copy-and-check programming idiom common
in lock-free data structures. These candidate summaries are used to compute the
interference among threads in linear time. Since a candidate summary need not
be a sound effect summary, we show how to fully automatically check whether the
precision of candidate summaries is sufficient. We can thus perform sound
verification despite relying on an unsound heuristic. We have implemented our
approach and found it up to two orders of magnitude faster than existing ones.