Write a Blog >>
ASE 2020
Mon 21 - Fri 25 September 2020 Melbourne, Australia
Tue 22 Sep 2020 02:40 - 03:00 at Koala - Formal Methods (1) Chair(s): Nazareno Aguirre

A common problem in MPI programs is deadlock: when two or more processes are blocked indefinitely due to a circular communication dependency. Automatically detecting deadlock is difficult due to its schedule-dependent nature. This paper presents a predictive analysis for single-path MPI programs that observes a single program execution and then determines whether any other feasible schedule of the program can lead to a deadlock. The analysis works by identifying problematic communication patterns in a dependency graph to form a set of deadlock candidates. The deadlock candidates are filtered by an abstract machine and ultimately tested for reachability by an SMT solver with an efficient encoding for deadlock. This approach quickly yields a set of high probability deadlock candidates useful for reasoning about complex codes and yields higher performance overall in many cases compared to other state-of-the-art analyses. The analysis is sound and complete for single-path MPI programs on a given input.

Tue 22 Sep

Displayed time zone: (UTC) Coordinated Universal Time change

02:20 - 03:20
Formal Methods (1)NIER track / Research Papers at Koala
Chair(s): Nazareno Aguirre Dept. of Computer Science FCEFQyN, University of Rio Cuarto
02:20
20m
Talk
Accelerating All-SAT Computation with Short Blocking Clauses
Research Papers
Yueling Zhang Singapore Management University, Geguang Pu East China Normal University, Jun Sun Singapore Management University
02:40
20m
Talk
A Predictive Analysis for Detecting Deadlock in MPI Programs
Research Papers
Yu Huang Southwestern University of Finance and Economics, Benjamin Ogles Brigham Young University, Eric Mercer Brigham Young University
Pre-print
03:00
10m
Talk
Proving Termination by k-Induction
NIER track
Jianhui Chen Tsinghua University, Fei He Tsinghua University, China