SI2-SSE: Correctness Verification Tools for Extreme Scale Hybrid Concurrency

点击翻译按钮获取中文摘要

High Performance Computing is strategically important to national competitiveness. Advances in computational capabilities involve the use of unprecedented levels of parallelism: programming methods that involve billions of concurrent activities. Multiple styles of concurrency involving shared and distributed memory programming ("hybrid") are necessary. Unfortunately, such programs are very difficult to debug using existing methods. This project develops formal (mathematically based) verification tools that can debug hybrid concurrent programs with very high certainty of bug elimination, while consuming only modest computational resources for verification. The project develops execution-based tools that eliminate search over semantically equivalent alternative schedules as well as solver-based techniques that eliminate classes of bugs over single runs. Scalable methods based on non-determinism classification and heuristic execution-space reduction are also being developed. Expected results include: (1) development of tools based on formal algorithmic techniques that verify large-scale hybrid programs; (2) amalgamation of incisive bug-hunting methods developed at other research organizations within formally based tools developed in our group; (3) incorporation of our verification tools and techniques within popular tool-integration frameworks; (4) large-scale case studies handled using our tools; and (5) training of undergraduate and graduate students on these advanced verification methods, building the talent pool vital to continued progress in high performance computing with applications to science and engineering, energy/sustainability, and homeland security.