Utilizing Model Checking for Automated Optimization Information Discovery in InDiGO

InDiGO framework provides an infrastructure which allows design of generic but customizable algorithms encapsulated as middleware services and provides tools to customize such algorithms for specific applications. Such customization allows one to optimize algorithms by removing communication which is redundant in the context of a specific application. Information necessary for optimization is derived by running queries of interest on the application abstraction. Each new query requires a new algorithm to be written that would operate on the application abstraction to give a yes or no answer. In this paper, we describe a different approach to answer the queries. It uses model checking and is fully automated. It also allows to answer the queries precisely as well as to verify more general properties. We present experimental results to demonstrate the optimizations when our infrastructure is utilized.