Taming Schedule Space Explosion in Message Passing Application Verification

Message passing (MP) has gained a widespread adoption over the years. Traditionally, message passing has been employed in the application construction specifically meant for high performance computing, however, this is not true anymore. We are witnessing quite a shift in computing practices with message passing serving a much larger audience than ever before. With such growing importance, it becomes essential to have formal tools and methodologies to establish correctness of MP applications. While there has been some state-of-the-art verifiers and methodologies for MP applications, they all suffer from a common problem: schedule-space explosion! In this talk, I will present and discuss two strategies to effectively contain the schedule-space explosion. These strategies are specifically meant for dynamic verification engines which operate in a closed environment (i.e. for a fixed input). I would further discuss the soundness and completeness aspects of these strategies and their ability to verify practical MP applications in a scalable manner.