Developing a Dynamic Verification Tool for Atomic Dataflow (ADF) Programs

Participant: Erdal Mutlu

Home Institution: 
Research Center for Multi-Core Software Engineering, Koc University

Home Country: Turkey

Host: Dr. Osman Unsal

Host Institution: Department for Computer Architecture for Parallel Paradigms, Barcelona Supercomputing Center
Host Country: Spain

Start Date:

End Date: 2013-12-08 

We propose a dynamic verification tool for characterizing and exploring be- haviors of programs written using hybrid dataflow programming models. We focus in particular on the Atomic DataFlow (ADF) programming model as a representative of this class of programming models. In the ADF model, a program is based on tasks for which data dependencies are explicitly defined by a programmer and used by the runtime system to coordinate the task execution, while the memory shared between potentially concurrent tasks is managed using transactional memory (TM). While ideally these two domains should be well separated within a program, concurrency bugs can lead to an unexpected interleaving between these domains, leading to incorrect program behavior.
We devised a randomized scheduling method for exploring programs written using ADF. The key challenge in our work was precisely characterizing and exploring the concurrency visible and meaningful to the programmer, as opposed to the concurrency present in the dataflow runtime or TM implementations. For exploration of different interleavings, we adapted the dynamic exploration technique “Probabilistic Concurrency Testing (PCT)” to ADF programs in order to amplify the randomness of observed schedules. For shared memory concurrent programs, PCT provides probabilistic guarantees for bug detection. By properly selecting the scheduling points that PCT randomly chooses from, we aim to provide a similar guarantee for ADF programs.

Report: here