Write a Blog >>
PPoPP 2021
Sat 27 February - Wed 3 March 2021
Tue 2 Mar 2021 12:42 - 12:48 - Session 6. Posters 1 Chair(s): Adam Morrison

Deductive verification of concurrent programs under weak memory has thus far been limited to simple programs over a monolithic state space. For scalabiility, we also require modular techniques with verifiable library abstractions. We address this challenge in the context of RC11 RAR, a subset of the C11 memory model that admits relaxed and release-acquire accesses, but disallows, so-called, load-buffering cycles. We develop a simple framework for specifying abstract objects that precisely characterises the observability guarantees of abstract method calls. Our framework is integrated with an operational semantics that enables verification of client programs that execute abstract method calls from a library it uses. We implement such abstractions in RC11 RAR by developing a (contextual) refinement framework for abstract objects. Our framework has been mechanised in Isabelle/HOL.

Tue 2 Mar

Displayed time zone: Eastern Time (US & Canada) change

12:30 - 13:18
Session 6. Posters 1Main Conference
Chair(s): Adam Morrison Tel Aviv University
12:30
6m
Talk
POSTER: On Group Mutual Exclusion for Dynamic Systems
Main Conference
Shreyas Gokhale The University of Texas at Dallas, Sahil Dhoked The University of Texas at Dallas, Neeraj Mittal The University of Texas at Dallas
Link to publication
12:36
6m
Talk
POSTER: Bundled References: An Abstraction for Highly-Concurrent Linearizable Range Queries
Main Conference
Jacob Nelson Lehigh University, Ahmed Hassan Lehigh University, Roberto Palmieri Lehigh University
Link to publication
12:42
6m
Talk
POSTER: Verifying C11-Style Weak Memory Libraries
Main Conference
Sadegh Dalvandi University of Surrey, Brijesh Dongol University of Surrey
Link to publication
12:48
6m
Talk
POSTER: A Lock-free Relaxed Concurrent Queue for Fast Work Distribution
Main Conference
Giorgos Kappes University of Ioannina, Stergios V. Anastasiadis University of Ioannina
Link to publication
12:54
6m
Talk
POSTER: A more Pragmatic Implementation of the Lock-free, Ordered, Linked List
Main Conference
Jesper Träff TU Wien, Austria, Manuel Pöter TU Wien, Austria
Link to publication
13:00
6m
Talk
POSTER: Extending MapReduce Framework with Locality Keys
Main Conference
Yifeng Cheng Peiking University, China, Bei Wang Peking University, China, Xiaolin Wang Peking University, China
Link to publication
13:06
6m
Talk
POSTER: On the Parallel I/O Optimality of Linear Algebra Kernels: Near-Optimal LU Factorization
Main Conference
Grzegorz Kwasniewski ETH Zurich, Tal Ben-Nun Department of Computer Science, ETH Zurich, Alexandros Nikolaos Ziogas ETH Zurich, Timo Schneider ETH Zurich, Maciej Besta ETH Zurich, Torsten Hoefler ETH Zurich
Link to publication
13:12
6m
Talk
POSTER: Asynchrony versus Bulk-Synchrony for a Generalized N-body Problem from Genomics
Main Conference
Marquita Ellis University of California at Berkeley & Lawrence Berkeley National Lab, Aydın Buluç University of California at Berkeley & Lawrence Berkeley National Lab, Katherine Yelick University of California at Berkeley & Lawrence Berkeley National Lab
Link to publication