Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI
Wed 23 Jun 2021 09:00 - 09:05 at PLDI-A - Talks 1A: Concurrent and Distributed Programming
Wed 23 Jun 2021 21:00 - 21:05 at PLDI-A - Talks 1A: Concurrent and Distributed Programming

Strong eventual consistency (SEC) has been used as a classic notion of correctness for Conflict-Free Replicated Data Types (CRDTs). However, it does not give proper abstractions of functionality, thus is not helpful for modular verification of client programs using CRDTs. We propose a new correctness formulation for CRDTs, called Abstract Converging Consistency (ACC), to specify both data consistency and functional correctness. ACC gives abstract atomic specifications (as an abstraction) to CRDT operations, and establishes consistency between the concrete execution traces and the execution using the abstract atomic operations. The abstraction allows us to verify the CRDT implementation and its client programs separately, resulting in more modular and elegant proofs than monolithic approaches for whole program verification. We give a generic proof method to verify ACC of CRDT implementations, and a rely-guarantee style program logic to verify client programs. Our Abstraction theorem shows that ACC is equivalent to contextual refinement, linking the verification of CRDT implementations and clients together to derive functional correctness of whole programs.

Wed 23 Jun

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

09:00 - 09:35
Talks 1A: Concurrent and Distributed ProgrammingPLDI at PLDI-A +12h
09:00
5m
Talk
Abstraction for Conflict-Free Replicated Data Types
PLDI
Hongjin Liang Nanjing University, Xinyu Feng Nanjing University
DOI
09:05
5m
Talk
Modular Data-Race-Freedom Guarantees in the Promising Semantics
PLDI
Minki Cho Seoul National University, Sung-Hwan Lee Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav Tel Aviv University
DOI
09:10
5m
Talk
Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs
PLDI
Coşku Acay Cornell University, Rolph Recto Cornell University, Joshua Gancher Cornell University, Andrew C. Myers Cornell University, Elaine Shi Cornell University
DOI Pre-print
09:15
5m
Talk
Canary: Practical Static Detection of Inter-thread Value-Flow Bugs
PLDI
Yuandao Cai Hong Kong University of Science and Technology, Peisen Yao Hong Kong University of Science and Technology, Charles Zhang Hong Kong University of Science and Technology
DOI
09:20
5m
Talk
Practical Smart Contract Sharding with Ownership and Commutativity Analysis
PLDI
George Pîrlea National University of Singapore, Amrit Kumar Zilliqa Research, Ilya Sergey Yale-NUS College; National University of Singapore
DOI
09:25
5m
Talk
Snapshot-Free, Transparent, and Robust Memory Reclamation for Lock-Free Data Structures
PLDI
Ruslan Nikolaev Virginia Tech, Binoy Ravindran Virginia Tech
DOI
09:30
5m
Talk
Concurrent Deferred Reference Counting with Constant-Time Overhead
PLDI
Daniel Anderson Carnegie Mellon University, Guy E. Blelloch Carnegie Mellon University, Yuanhao Wei Carnegie Mellon University
DOI
21:00 - 21:35
Talks 1A: Concurrent and Distributed ProgrammingPLDI at PLDI-A
21:00
5m
Talk
Abstraction for Conflict-Free Replicated Data Types
PLDI
Hongjin Liang Nanjing University, Xinyu Feng Nanjing University
DOI
21:05
5m
Talk
Modular Data-Race-Freedom Guarantees in the Promising Semantics
PLDI
Minki Cho Seoul National University, Sung-Hwan Lee Seoul National University, Chung-Kil Hur Seoul National University, Ori Lahav Tel Aviv University
DOI
21:10
5m
Talk
Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs
PLDI
Coşku Acay Cornell University, Rolph Recto Cornell University, Joshua Gancher Cornell University, Andrew C. Myers Cornell University, Elaine Shi Cornell University
DOI Pre-print
21:15
5m
Talk
Canary: Practical Static Detection of Inter-thread Value-Flow Bugs
PLDI
Yuandao Cai Hong Kong University of Science and Technology, Peisen Yao Hong Kong University of Science and Technology, Charles Zhang Hong Kong University of Science and Technology
DOI
21:20
5m
Talk
Practical Smart Contract Sharding with Ownership and Commutativity Analysis
PLDI
George Pîrlea National University of Singapore, Amrit Kumar Zilliqa Research, Ilya Sergey Yale-NUS College; National University of Singapore
DOI
21:25
5m
Talk
Snapshot-Free, Transparent, and Robust Memory Reclamation for Lock-Free Data Structures
PLDI
Ruslan Nikolaev Virginia Tech, Binoy Ravindran Virginia Tech
DOI
21:30
5m
Talk
Concurrent Deferred Reference Counting with Constant-Time Overhead
PLDI
Daniel Anderson Carnegie Mellon University, Guy E. Blelloch Carnegie Mellon University, Yuanhao Wei Carnegie Mellon University
DOI