CSR: Small: Runtime Verification of Concurrent Programs

分布式多线程软件的编译和测试是一项非常具有挑战性的任务。这个项目开发的技术，方便程序员通过确定是否存在一个替代的计算线程的执行或执行进程的时间表，可能会违反有关程序的正确性的全局断言，以定位软件错误。该项目还研究了满足给定谓词的分布式多核程序的全局状态的枚举、检测和表示技术。该项目解决了并发程序的离线和运行时验证的基本问题。首先，它探讨了用于枚举感兴趣的全局状态的空间有效算法。 其次，研究了谓词检测并行算法的设计与实现。 第三，偏序集模型中关于谓词的计算切片是包括满足给定谓词的所有全局状态的最小计算。 该项目开发了通用切片技术和相关算法。第四，偏序集的切片算法用于检测在可达全局状态格上解释的基时态逻辑中表达的时态逻辑公式。该项目开发了在线验证这些公式的算法。社会依赖于越来越多的并行和分布式软件。这个软件容易出错，而且很麻烦。这个项目不仅将提高程序员的生产力，而且还减少了此类程序中的错误。此外，该项目正在开发可以分析计算的方法，以确保在接受其结果之前满足所有全局约束。该项目还将开发用于分析偏序集模型的技术，该模型具有广泛的应用，包括组合优化问题。这个项目有很强的教育成分。本项目开发的技术将被纳入并发和多核计算的课程中。本项目的成果将以技术报告、期刊文章、会议论文和论文的形式分享。只要期刊和会议论文集出版商允许，研究论文的草稿将在研究者的网站上提供。 该项目产生的计算机软件可在www.example.com上获得http://users.ece.utexas.edu/~garg/runtime-verification.This奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识价值和更广泛的影响审查标准进行评估来支持。

Debugging and testing distributed multithreaded software is a notoriously challenging task. This project develops techniques that facilitate a programmer to locate a software bug by determining if there exists an alternative computational thread of execution or a schedule of the executing processes that may violate a global assertion regarding the correctness of the programs. The project also investigates techniques for enumeration, detection and representation of global states of a distributed multicore program that satisfy a given predicate. The project solves fundamental problems in offline and runtime verification of concurrent programs.The project has four main components. First, it explores space-efficient algorithms for enumerating the global states of interest. Second, the project studies the design and implementation of parallel algorithms for predicate detection. Third, a slice of a computation in the poset model with respect to a predicate is the smallest computation that includes all global states satisfying the given predicate. The project develops general slicing techniques and associated algorithms. Fourth, slicing algorithms for posets are used to detect temporal logic formulas expressed in Basis Temporal Logic interpreted over the lattice of reachable global states. The project develops algorithms for online verification of such formulas.The society is dependent on software that is increasingly becoming parallel and distributed. Debugging this software is error prone and cumbersome. This project will not only improve programmer productivity but also reduce bugs in such programs. In addition, the project is developing methods than can analyze the computation to ensure that it satisfies all global constraints before accepting its result. The project will also develop techniques for analysis of a poset model that has wide applications including combinatorial optimization problems. There is a strong educational component for this project. Techniques developed in this project will be incorporated in the courses on concurrent and multicore computing.The outcomes of this project will be shared in the form of technical reports, journal articles, conference papers, and dissertations. Whenever allowed by the journals and conference proceedings publishers, drafts of the research papers will be available at the investigator's website. The computer software generated in this project is available at http://users.ece.utexas.edu/~garg/runtime-verification.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.