• Home
• People
• Jobs
• Visit
• Thesis Topics
• Publications
• Conference Rankings
• Research
• Bcast
• Teaching
• Contact

SPONSORS

COLLABORATIONS

The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

Publications of SPCL

C. Baumann, A. Marian Dan, Y. Meshman, T. Hoefler, M. Vechev:
	Automatic Verification of RMA Programs via Abstraction Extrapolation (Springer International Publishing, Feb. 2018, ) Abstract Remote Memory Access (RMA) networks are emerging as a promising basis for building performant large-scale systems such as MapReduce, scientific computing applications, and others. To achieve this performance, RMA networks exhibit relaxed memory consistency. This means the developer now must manually ensure that the additional relaxed behaviors are not harmful to their application -- a task known to be difficult and error-prone. In this paper, we present a method and a system that can automatically address this task. Our approach consists of two ingredients: (i) a reduction where we reduce the task of verifying program P running on RMA to the problem of verifying a program {$}{$}{\backslash}overline{\{}P{\}}{$}{$} on sequential consistency (where {$}{$}{\backslash}overline{\{}P{\}}{$}{$} captures the required RMA behaviors), and (ii) abstraction extrapolation: a new method to automatically discover both, predicates (via predicate extrapolation) and abstract transformers (via boolean program extrapolation) for {$}{$}{\backslash}overline{\{}P{\}}{$}{$} . This enables us to automatically extrapolate the proof of P under sequential consistency (SC) to a proof of P under RMA. We implemented our method and showed it to be effective in automatically verifying, for the first time, several challenging concurrent algorithms under RMA. Documents download article:
	BibTeX
@proceedings{,   author={Cedric Baumann and Andrei Marian Dan and Yuri Meshman and Torsten Hoefler and Martin Vechev},   title={{Automatic Verification of RMA Programs via Abstraction Extrapolation}},   year={2018},   month={02},   publisher={Springer International Publishing},   note={}, }