With increasing levels of parallelism in all computers since the end of Dennard Scaling in 2005, all software is now becoming parallel or concurrent by default. It is increasingly important to examine the foundations of parallelism underlying current software from the verification perspective. In many cases, this foundation is based on “unstructured parallelism”, as exemplified by the use of threads and locks.

In this talk, we summarize experiences gained in the Habanero Extreme Scale Software Research Laboratory (first at Rice University, and now at Georgia Tech) in developing a foundation for parallel and concurrent software based on a collection of structured parallel execution model primitives that enable enhanced verification relative to unstructured parallelism. We show how this execution model can enable verification of entire classes of programs that use well defined subsets of parallel primitives (e.g., deadlock freedom, determinism), verification of specific programs that use less constrained primitives (e.g., permissions, determinism), and verification of program-input pairs with even fewer constraints (e.g., datarace freedom, determinism, deadlock avoidance).

Vivek Sarkar is Professor of Computer Science and the E.D. Butcher Chair in Engineering at Rice University. He conducts research in multiple aspects of parallel software including programming languages, program analysis, compiler optimizations and runtimes systems for diverse parallel platforms. He currently leads the Habanero Extreme Scale Software Research Laboratory at Rice University, and is PI of the DARPA-funded Pliny project on “big code” analytics. Prior to joining Rice in July 2007, Vivek was Senior Manager of Programming Technologies at IBM Research. His responsibilities at IBM included leading IBM’s research efforts in programming model, tools, and productivity in the PERCS project during 2002- 2007 as part of the DARPA High Productivity Computing System program. His prior research projects include the X10 programming language, the Jikes Research Virtual Machine for the Java language, the ASTI optimizer used in IBM’s XL Fortran product compilers, the PTRAN automatic parallelization system, and profile-directed partitioning and scheduling of Sisal programs. In 1997, he was on sabbatical as a visiting associate professor at MIT, where he was a founding member of the MIT Raw multicore project. Vivek became a member of the IBM Academy of Technology in 1995, and was inducted as an ACM Fellow in 2008. He holds a B.Tech. degree from the Indian Institute of Technology, Kanpur, an M.S. degree from University of Wisconsin-Madison, and a Ph.D. from Stanford University. Vivek has been serving as a member of the US Department of Energy’s Advanced Scientific Computing Advisory Committee (ASCAC) since 2009, and on CRA’s Board of Directors since 2015.