Discamus continentiam augere, luxuriam coercere
Home -> Publications
Home
  Publications
    
all years
    2018
    2017
    2016
    2015
    2014
    2013
    2012
    2011
    2010
    2009
    2008
    2007
    2006
    2005
    2004
    theses
    techreports
    presentations
    edited volumes
    conferences
  Awards
  Research
  Teaching
  BLOG
  Miscellaneous
  Full CV [pdf]






  Events








  Past Events





Publications of Torsten Hoefler
Copyright Notice:

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.

Cedric Baumann, Andrei Marian Dan, Yuri Meshman, Torsten Hoefler, Martin 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={Feb.},
  publisher={Springer International Publishing},
  source={http://www.unixer.de/~htor/publications/},
}

serving: 54.196.42.8:36288© Torsten Hoefler