SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Wed 2 Nov 2016 11:45 - 12:10 at Matterhorn 2 - Semantics and Verification Chair(s): Jonathan Aldrich

Recent advances in networking hardware have led to a new generation of Remote Memory Access (RMA) networks in which processors from different machines can communicate directly, bypassing the operating system and allowing higher performance. Researchers and practitioners have proposed libraries and programming models for RMA to enable the development of applications running on these networks,

However, the memory models implied by these RMA libraries and languages are often loosely specified, poorly understood, and differ depending on the underlying network architecture and other factors. Hence, it is difficult to precisely reason about the semantics of RMA programs or how changes in the network architecture affect them.

We address this problem with the following contributions: (i) a \emph{coreRMA} language which serves as a common foundation, formalizing the essential characteristics of RMA programming; (ii) complete axiomatic semantics for that language;
(iii) integration of our semantics with an existing constraint solver, enabling us to exhaustively generate \emph{coreRMA} programs (litmus tests) up to a specified bound and check whether the tests satisfy their specification; and (iv) extensive validation of our semantics on real-world RMA systems.
We generated and ran $7441$ litmus tests using each of the low-level RMA network APIs: DMAPP, VPI Verbs, and Portals 4. Our results confirmed that our model successfully captures behaviors exhibited by these networks. Moreover, we found RMA programs that behave inconsistently with existing documentation, confirmed by network experts.

Our work provides an important step towards understanding existing RMA networks, thus influencing the design of future RMA interfaces and hardware.

#### Wed 2 NovDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

 10:30 - 12:10 Semantics and VerificationOOPSLA at Matterhorn 2 Chair(s): Jonathan Aldrich Carnegie Mellon University 10:3025mTalk Semantics-Based Program Verifiers for All LanguagesOOPSLAAndrei Stefanescu University of Illinois at Urbana-Champaign, Daejun Park University of Illinois at Urbana-Champaign, Shijiao Yuwen University of Illinois at Urbana-Champaign, Yilong Li Runtime Verification, Inc., Grigore Roşu University of Illinois at Urbana-Champaign DOI Media Attached 10:5525mTalk Hoare-Style Specifications as Correctness Conditions for Non-linearizable Concurrent ObjectsOOPSLAIlya Sergey University College London, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute, Germán Andrés Delbianco IMDEA Software Institute DOI Pre-print Media Attached File Attached 11:2025mTalk An Operational Semantics for C/C++11 ConcurrencyOOPSLAKyndylan Nienhuis University of Cambridge, Kayvan Memarian University of Cambridge, Peter Sewell University of Cambridge DOI 11:4525mTalk Modeling and Analysis of Remote Memory Access ProgrammingOOPSLAAndrei Marian Dan ETH Zurich, Patrick Lam University of Waterloo, Canada, Torsten Hoefler ETH Zurich, Martin Vechev ETH Zurich DOI Pre-print Media Attached