Much of the past work on dynamic data-race and determinacy-race detection algorithms for task parallelism has focused on structured parallelism with fork-join constructs and, more recently, with future constructs. This paper addresses the problem of dynamic detection of data-races and determinacy-races in task-parallel programs with promises, which are more general than fork-join constructs and futures. The motivation for our work is twofold. First, promises have now become a mainstream synchronization construct, with their inclusion in multiple languages, including C++, JavaScript, and Java. Second, past work on dynamic data-race and determinacy-race detection for task-parallel programs does not apply to programs with promises, thereby identifying a vital need for this work.

This paper makes multiple contributions. First, we introduce a featherweight programming language that captures the semantics of task-parallel programs with promises and provides a basis for formally defining determinacy using our semantics. This definition subsumes functional determinacy (same output for same input) and structural determinacy (same computation graph for same input). The main theoretical result shows that the absence of data races is sufficient to guarantee determinacy with both properties. We are unaware of any prior work that established this result for task-parallel programs with promises. Next, we introduce a new Dynamic Race Detector for Promises that we call DRDP. DRDP is the first known race detection algorithm that executes a task-parallel program sequentially without requiring the serial-projection property; this is a critical requirement since programs with promises do not satisfy the serial-projection property in general. Finally, the paper includes experimental results obtained from an implementation of DRDP. The results show that, with some important optimizations introduced in our work, the space and time overheads of DRDP are comparable to those of more restrictive race detection algorithms from past work. To the best of our knowledge, DRDP is the first determinacy race detector for task-parallel programs with promises.

Fri 21 Jul

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

10:30 - 12:00
ECOOP 7: Verification and TestingResearch Papers at Amazon Auditorium (Gates G20)
Chair(s): Wenxi Wang University of Texas at Austin
10:30
15m
Talk
On using VeriFast, VerCors, Plural, and KeY to check object usage
Research Papers
João Mota NOVA School of Science and Technology, António Ravara NOVA LINCS & FCT, NOVA University of Lisbon, Marco Giunti NOVA-LINCS, FCT NOVA / Universidade Nova de Lisboa
DOI
10:45
15m
Talk
Exact Separation Logic
Research Papers
Petar Maksimović Imperial College London, UK, Caroline Cronjäger Ruhr-Universität Bochum, Andreas Lööw Imperial College London, Julian Sutherland Imperial College London, Philippa Gardner Imperial College London
DOI Pre-print
11:00
15m
Talk
Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs
Research Papers
Ashish Mishra Purdue University, Suresh Jagannathan Purdue University
DOI
11:15
15m
Talk
Constraint Based Compiler Optimization for Energy Harvesting Applications
Research Papers
Yannan Li University of Southern California, Chao Wang University of Southern California
DOI
11:30
15m
Talk
Dynamic Determinacy Race Detection for Task-Parallel Programs with Promises
Research Papers
Feiyang Jin Georgia Institute of Technology, Lechen Yu Georgia Institute of Technology, Tiago Cogumbreiro University of Massachusetts Boston, Vivek Sarkar Georgia Institute of Technology, Jun Shirako Georgia Institute of Technology
DOI
11:45
15m
Talk
On Leveraging Tests to Infer Nullable Annotations
Research Papers
Jens Dietrich Victoria University of Wellington, David J. Pearce ConsenSys, Mahin Chandramohan Oracle Labs
DOI