Keynote talk : How to structure your concurrent program and its verification

Paul Attie American University in Beirut (Lebanon)

ABSTRACT: I present some local methods for both *writing* and verifying large concurrent programs: pairwise normal form, dynamic addition of pairwise interactions, and deadlock-freedom via subsystem checking. In pairwise normal form, a process P_i is a set of actions, where each action is a « conjunction » of smaller pairwise-actions, over the neighbors of P_i (the processes that P_i interacts directly with). Variables are shared among pairs. This provides for locality and modifiability in program design, and for tractability in verification. Mutex among n processes can be expressed as 2-process mutex among every pair. If 2-process mutex is enforced among some pairs only, we obtain generalized dining philosophers. If some

2-process mutexes are replaced by a version which gives priority to one process, we obtain readers-writers. Verification of pairwise safety and liveness can be carried out by model-checking each pair in isolation, thereby avoiding state-explosion.

Pairs can be added dynamically, at run time. This enables an infinite-state system to be expressed as a countably infinite number of finite-state processes. I introduce the first sound and complete characterization of deadlock for concurrent programs. Most approaches to deadlock observe that a wait-for cycle is necessary for deadlock. However, a cycle is not *sufficient* for deadlock, since a process in the wait-for cycle can choose to interact with a process outside the cycle. This leads to high degree of « incompleteness » in such methods. My approach analyzes the AND-OR generalization of a wait-for cycle, which is necessary and sufficient for a deadlock. I then impose local conditions (over small subsystems) which prevent the creation of such AND-OR wait-for cycles. My methods have been implemented in the Eshmun tool.

BIOGRAPHY: Paul Attie (http://www.cs.aub.edu.lb/pa07/) is a Professor of Computer Science at the American University of Beirut. He received a Ph.D. in Computer Science from the University of Texas at Austin in 1995. Paul’s research is in software engineering, formal methods, and distributed computing. He works on devising efficient methods for specifying, designing, and reasoning about the behavior of large distributed software systems. In particular, he showed that the safety, liveness, and deadlock-freedom of large concurrent programs can be established by reasoning about small sets (2 or 3) of component processes at a time, thereby avoiding state-explosion. Together with his students, Paul has designed and implemented the Eshmun tool, which can model check and repair concurrent programs.

Paul has held faculty positions at Florida International University and Northeastern University, and Visiting Scientist and Research Affiliate positions at the MIT Computer Science and Artificial Intelligence Laboratory (CSAIL). He will join the School of Computer and Cyber Sciences at Augusta University in August 2019.