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

高性能计算对国家竞争力具有重要的战略意义。 计算能力的进步涉及到前所未有的并行性水平的使用：涉及数十亿并发活动的编程方法。 涉及共享和分布式内存编程（“混合”）的多种类型的并发是必要的。不幸的是，这样的程序很难使用现有的方法进行调试。该项目开发了正式的（基于数学的）验证工具，可以调试混合并发程序，具有非常高的确定性的错误消除，同时只消耗适度的计算资源进行验证。 该项目开发基于执行的工具，消除搜索语义上等同的替代计划，以及基于求解器的技术，消除类的错误在单次运行。基于非确定性分类和启发式执行空间减少的可扩展方法也正在开发中。预期成果包括：（1）开发基于正式算法技术的工具，验证大规模混合程序;（2）将其他研究组织开发的深入的错误搜索方法合并到我们小组开发的正式工具中;（3）将我们的验证工具和技术合并到流行的工具集成框架中;（4）使用我们的工具处理大规模案例研究;以及（5）对本科生和研究生进行这些先进验证方法的培训，建立人才库，这对高性能计算在科学和工程、能源/可持续性和国土安全方面的应用的持续发展至关重要。

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.