Write a Blog >>
ICSE 2023
Sun 14 - Sat 20 May 2023 Melbourne, Australia
Thu 18 May 2023 11:45 - 12:00 at Meeting Room 106 - Software verification Chair(s): Youcheng Sun

Data races seriously threaten the correctness of concurrent programs. Earlier works can report false positives. Recently, trace-based predictive analysis has achieved sound results by inferring feasible traces based on sound partial orders or constraint solvers. However, they hold the same assumption: any read event may affect the control-flow. Thus, being control-flow sensitive, they have to enforce that any read event (in an inferred trace) should read the same value or a value from the same event as that in the original trace, albeit some slightly relax this. This (even with relaxation) severely limits their predictive ability and many true data races can be missed. To overcome this limitation, we introduce the concept of Fix-Point Event and propose a new partial order model. This allows us to not only predict races with witness traces (like existing works with no control-flow changes) but also soundly infer existences of witness traces with potential control-flow changes. Thus, we can achieve a higher concurrency coverage and detect more data races soundly. We have implemented above as a tool ToccRace and conducted a set of experiments on a benchmark of seven real-world programs and a large-scale software MySQL, where MySQL produced 427 traces with a total size of 3.4TB. Compared with the state-of-the-art sound data race detector SeqC, ToccRace is significantly more effective by detecting 84.4%/200% more unique/dynamic races on the benchmark programs and 52.22%/49.8% more unique/dynamic races on MySQL, incurring reasonable time and memory costs (about 1.1x/43.5x on the benchmark programs and 10x/1.03x on MySQL). Furthermore, ToccRace is sound and is complete on two threads.

Thu 18 May

Displayed time zone: Hobart change

11:00 - 12:30
11:00
15m
Talk
Data-driven Recurrent Set Learning For Non-termination Analysis
Technical Track
Zhilei Han Tsinghua University, Fei He Tsinghua University
11:15
15m
Talk
Compiling Parallel Symbolic Execution with Continuations
Technical Track
Guannan Wei Purdue University, Songlin Jia Purdue University, Ruiqi Gao Purdue University, Haotian Deng Purdue University, Shangyin Tan UC Berkeley, Oliver Bračevac Purdue University, Tiark Rompf Purdue University
Pre-print
11:30
15m
Talk
Verifying Data Constraint Equivalence in FinTech Systems
Technical Track
Chengpeng Wang Hong Kong University of Science and Technology, Gang Fan Ant Group, Peisen Yao Zhejing University, Fuxiong Pan Ant Group, Charles Zhang Hong Kong University of Science and Technology
Pre-print
11:45
15m
Talk
Tolerate Control-Flow Changes for Sound Data Race Prediction
Technical Track
Shihao Zhu State Key Laboratory of Computer Science,Institute of Software,Chinese Academy of Sciences,China, Yuqi Guo Institute of Software, Chinese Academy of Sciences, Beijing, China, Long Zhang Institute of Software, Chinese Academy of Sciences, Yan Cai Institute of Software at Chinese Academy of Sciences
12:00
7m
Talk
TSVD4J: Thread-Safety Violation Detection for Java
DEMO - Demonstrations
Shanto Rahman University of Texas at Austin, Chengpeng Li University of Texas at Austin, August Shi University of Texas at Austin
12:07
7m
Talk
What Petri Nets Oblige Us to Say Comparing Approaches for Behavior Composition
Journal-First Papers
Achiya Elyasaf Ben-Gurion University of the Negev, Tom Yaacov Ben-Gurion University of the Negev, Gera Weiss Ben-Gurion University of the Negev
Link to publication DOI
12:15
7m
Talk
A Novel and Pragmatic Scenario Modeling Framework with Verification-in-the-loop for Autonomous Driving Systems
NIER - New Ideas and Emerging Results
Dehui Du East China Normal University, Bo Li East China Normal University, Chenghang Zheng East China Normal University