Write a Blog >>
ESEC/FSE 2021
Thu 19 - Sat 28 August 2021 Clowdr Platform
Wed 25 Aug 2021 11:20 - 11:30 - Analysis—Model Checking Chair(s): Domenico Bianculli
Wed 25 Aug 2021 23:20 - 23:30 - Analysis—Model Checking Chair(s): Matthew B Dwyer

Atomicity is a correctness criterion to reason about isolated code regions in a multithreaded program when they are executed concurrently. However, dynamic instances of these code regions, called transactions, may fail to behave atomically, resulting in transactional atomicity violations. Existing dynamic online atomicity checkers incur either false positives or false negatives in detecting transactions experiencing transactional atomicity violations. This paper proposes RegionTrack. RegionTrack tracks cross-thread dependences at the event, dynamic subregion, and transaction levels. It maintains both dynamic subregions within selected transactions and transactional happens-before relations through its novel timestamp propagation approach. We prove that RegionTrack is sound and complete in detecting both transactional atomicity violations and non-serializable traces. To the best of our knowledge, it is the first online technique that precisely captures the transitively closed set of happens-before relations over all conflicting events with respect to every running transaction for the above two kinds of issues. We have evaluated RegionTrack on 19 subjects of the DaCapo and the Java Grande Forum benchmarks. The empirical results confirm that RegionTrack precisely detected all those transactions which experienced transactional atomicity violations and identified all non-serializable traces. The overall results also show that RegionTrack incurred 1.10x and 1.08x lower memory and runtime overheads than Velodrome and 2.10x and 1.21x lower than Aerodrome, respectively. Moreover, it incurred 2.89x lower memory overhead than DoubleChecker. On average, Velodrome detected about 55% fewer violations than RegionTrack, which in turn reported about 3%-70% fewer violations than DoubleChecker.

Wed 25 Aug

Displayed time zone: Athens change

11:00 - 12:00
Analysis—Model CheckingJournal First / Research Papers +12h
Chair(s): Domenico Bianculli University of Luxembourg
11:00
10m
Paper
Checking LTL[F,G,X] on Compressed Traces in Polynomial TimeArtifacts AvailableArtifacts Reusable
Research Papers
Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign
DOI
11:10
10m
Paper
Conditional Interpolation: Making Concurrent Program Verification More Effective
Research Papers
Jie Su Xidian University, Cong Tian Xidian University, Zhenhua Duan Xidian University
DOI
11:20
10m
Paper
RegionTrack: A Trace-based Sound and Complete Checker to Debug Transactional Atomicity Violations and Non-Serializable Traces
Journal First
Xiaoxue Ma City University of Hong Kong, Shangru WU City University of Hong Kong, Ernest Pobee City University of Hong Kong, Xiupei Mei City University of Hong Kong, Hao Zhang City University of Hong Kong, Bo Jiang Beihang University, Wing-Kwong Chan City University of Hong Kong, Hong Kong
11:30
30m
Live Q&A
Q&A (Analysis—Model Checking)
Research Papers

23:00 - 00:00
Analysis—Model CheckingResearch Papers / Journal First
Chair(s): Matthew B Dwyer University of Virginia
23:00
10m
Paper
Checking LTL[F,G,X] on Compressed Traces in Polynomial TimeArtifacts AvailableArtifacts Reusable
Research Papers
Minjian Zhang University of Illinois at Urbana-Champaign, Umang Mathur University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign
DOI
23:10
10m
Paper
Conditional Interpolation: Making Concurrent Program Verification More Effective
Research Papers
Jie Su Xidian University, Cong Tian Xidian University, Zhenhua Duan Xidian University
DOI
23:20
10m
Paper
RegionTrack: A Trace-based Sound and Complete Checker to Debug Transactional Atomicity Violations and Non-Serializable Traces
Journal First
Xiaoxue Ma City University of Hong Kong, Shangru WU City University of Hong Kong, Ernest Pobee City University of Hong Kong, Xiupei Mei City University of Hong Kong, Hao Zhang City University of Hong Kong, Bo Jiang Beihang University, Wing-Kwong Chan City University of Hong Kong, Hong Kong
23:30
30m
Live Q&A
Q&A (Analysis—Model Checking)
Research Papers