Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 Virtual Conference

This program is tentative and subject to change.

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.

This program is tentative and subject to change.

Conference Day
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 LiangNanjing University, Xinyu FengNanjing University
DOI
09:05
5m
Talk
Modular Data-Race-Freedom Guarantees in the Promising Semantics
PLDI
Minki ChoSeoul National University, Sung-Hwan LeeSeoul National University, Chung-Kil HurSeoul National University, Ori LahavTel Aviv University
DOI
09:10
5m
Talk
Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs
PLDI
Coşku AcayCornell University, Rolph RectoCornell University, Joshua GancherCornell University, Andrew C. MyersCornell University, Elaine ShiCornell University
DOI Pre-print
09:15
5m
Talk
Canary: Practical Static Detection of Inter-thread Value-Flow Bugs
PLDI
Yuandao CaiHong Kong University of Science and Technology, Peisen YaoHong Kong University of Science and Technology, Charles ZhangHong Kong University of Science and Technology
DOI
09:20
5m
Talk
Practical Smart Contract Sharding with Ownership and Commutativity Analysis
PLDI
George PîrleaNational University of Singapore, Amrit KumarZilliqa Research, Ilya SergeyYale-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 NikolaevVirginia Tech, Binoy RavindranVirginia Tech
DOI
09:30
5m
Talk
Concurrent Deferred Reference Counting with Constant-Time Overhead
PLDI
Daniel AndersonCarnegie Mellon University, Guy E. BlellochCarnegie Mellon University, Yuanhao WeiCarnegie 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 LiangNanjing University, Xinyu FengNanjing University
DOI
21:05
5m
Talk
Modular Data-Race-Freedom Guarantees in the Promising Semantics
PLDI
Minki ChoSeoul National University, Sung-Hwan LeeSeoul National University, Chung-Kil HurSeoul National University, Ori LahavTel Aviv University
DOI
21:10
5m
Talk
Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs
PLDI
Coşku AcayCornell University, Rolph RectoCornell University, Joshua GancherCornell University, Andrew C. MyersCornell University, Elaine ShiCornell University
DOI Pre-print
21:15
5m
Talk
Canary: Practical Static Detection of Inter-thread Value-Flow Bugs
PLDI
Yuandao CaiHong Kong University of Science and Technology, Peisen YaoHong Kong University of Science and Technology, Charles ZhangHong Kong University of Science and Technology
DOI
21:20
5m
Talk
Practical Smart Contract Sharding with Ownership and Commutativity Analysis
PLDI
George PîrleaNational University of Singapore, Amrit KumarZilliqa Research, Ilya SergeyYale-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 NikolaevVirginia Tech, Binoy RavindranVirginia Tech
DOI
21:30
5m
Talk
Concurrent Deferred Reference Counting with Constant-Time Overhead
PLDI
Daniel AndersonCarnegie Mellon University, Guy E. BlellochCarnegie Mellon University, Yuanhao WeiCarnegie Mellon University
DOI