Automating deductive verification for weak-memory programs (extended version)
- PDF / 1,954,603 Bytes
- 20 Pages / 595.276 x 790.866 pts Page_size
- 53 Downloads / 234 Views
STTT Special Issue TACAS 2018
Automating deductive verification for weak-memory programs (extended version) Alexander J. Summers1 · Peter Müller1
© Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract Writing correct programs for weak-memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of such programs have recently been proposed, but their usage has been limited thus far to manual proofs. Automating proofs in these logics via first-order solvers is non-trivial, due to features such as higher-order assertions, modalities and rich permission resources. In this paper, we provide the first encoding of a weak-memory program logic using existing deductive verification tools. Our work enables, for the first time, the (unbounded) verification of C11 programs at the level of abstraction provided by the program logics; the only necessary user interaction is in the form of specifications written in the program logic and, in rare cases, ghost operations. We tackle three recent program logics: Relaxed Separation Logic and two forms of Fenced Separation Logic, and show how these can be encoded using the Viper verification infrastructure. In doing so, we illustrate several novel encoding techniques which could be employed for other logics. Our work is implemented, and has been evaluated on examples from existing papers as well as the Facebook open-source Folly library. Keywords Relaxed separation logic (RSL) · Fenced separation logic (FSL) · Viper encoding · Weak memory · Program verification
1 Introduction Reasoning about programs running on weak memory is challenging, because weak-memory models admit executions that are not sequentially consistent, that is, cannot be explained by a sequential interleaving of concurrent threads. Moreover, weak-memory programs employ a range of operations to access memory, which require dedicated reasoning techniques. These operations include fences as well as read and write accesses with varying degrees of synchronisation. The complexity of the underlying memory model and the non-existence (in general) of a single ordering of events consistent with the observations of all program threads makes
B
Peter Müller [email protected] Alexander J. Summers [email protected]
1
Department of Computer Science, ETH Zurich, Universitätstrasse 6, 8092 Zurich, Switzerland
writing and reasoning about code combining these primitives extremely difficult.1 Some of these challenges are addressed by the first program logics for weak-memory programs, in particular, Relaxed Separation Logic (RSL) [43], GPS [41], Fenced Separation Logic (FSL) [13], and FSL++ [14]. These logics apply to interesting classes of C11 programs, but their tool support has been limited to embeddings in Coq. Verification based on these embeddings requires substantial user interaction, which is an obstacle to applying and evaluating these logics. In this paper, we present a novel approach
Data Loading...
