Advances in computing crucially dependent on the use of multiple processing units that are programmed using parallel programming languages. As these parallel processing systems find uses in critical applications such as national security infrastructures, medical devices, airplanes, and computing installations that predict our weather, they must be highly reliable as well as energy efficient. Unfortunately, today’s parallel programming languages as well as multi-processors are extremely difficult to reliably employ, as well as efficiently program. In addition to the generally recognized difficulty of writing parallel programs, one of the central unresolved difficulties is that of a clearly defined and well specified shared memory semantics, which dictates how the computing elements exchange data, as well as how compilers can safely optimize parallel programs.

The main contribution of this project was exploring topics related to the analysis and verification of parallel programs while taking the semantics of shared memory into account. We devised several main contributions. First, we developed a formal model for a common and widely used parallel programming paradigm called pthreads. We implemented this model as an extension of our software verifier called SMACK. Using this extension, we were able to verify numerous real-world parallel programs, and in particular we focused on Linux device drivers. In the process, our tool automatically discovered several bugs related to parallelism and shared memory. Also, we competed twice in the annual software verification competition, and won several medals both times.

As our second main thrust, we carefully studied how shared memory operates in graphics processing units (GPUs). GPUs achieve higher computational efficiency than CPUs by employing simpler cores, and hide memory latency by switching away from stalled threads. GPUs also follow a weak memory consistency model, and as such are very hard to program correctly. While CPUs also have such weak memory rules,  the rules followed by GPUs are much less well understood. As a part of this project, we subjected a number of different GPU architecture to targeted stress-testing in order to observe potentially erroneous memory behaviors. In the process, we have shown that GPU code can in fact end up fetching stale data, which was not what programmers would expect.

Building on top of the lessons learned from our second thrust, we realized that despite the growing popularity of GPU parallel programming, there is a lack of portable synchronization primitives that are needed to perform certain kinds of parallel computations. Hence, as our final main contribution, we developed such a portable synchronization primitive. We empirically and formally validated its correctness under weak memory models as implemented by various GPU architectures. Since then, we have been working on trying to incorporate our primitive into the next GPU programming language standard, in order to make it available to a multitude of GPU programmers.

Finally, we explored improving the core search algorithm of the CIVL verification engine. We implemented several search strategies and we empirically evaluated them on a number of CIVL benchmarks. Our prototype implementation showed promising results, and we hope that it will be incorporated into the main CIVL engine.

We disseminated our research results by publishing around ten research papers and reports. We also implemented tools and extensions stemming from this research, and we disseminated those to the academic community as well as practitioners in national labs and industry. We made all of the developed tools publicly available and open-source projects. As a part of this project, we also trained a generation of students and post-doctoral researchers in the areas of parallel programming and shared memory semantics where the current shortage of such manpower is crippling national productivity as well as innovation.

Last Modified: 10/26/2016
Modified by: Zvonimir Rakamaric