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
Times are displayed in time zone: (UTC) Coordinated Universal Time

02:20 - 03:20: Formal Methods (1)Research Papers / NIER track at Koala
Chair(s): Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto
02:20 - 02:40
Accelerating All-SAT Computation with Short Blocking Clauses
Research Papers
Yueling ZhangSingapore Management University, Geguang PuEast China Normal University, Jun SunSingapore Management University
02:40 - 03:00
A Predictive Analysis for Detecting Deadlock in MPI Programs
Research Papers
Yu HuangSouthwestern University of Finance and Economics, Benjamin OglesBrigham Young University, Eric MercerBrigham Young University
03:00 - 03:10
Proving Termination by k-Induction
NIER track
Jianhui ChenTsinghua University, Fei HeTsinghua University, China