CSR: Small: Runtime Verification of Concurrent Programs

CSR：小：并发程序的运行时验证

基本信息

批准号：
1812351
负责人：
Vijay Garg
金额：
$ 41.48万
依托单位：
University of Texas at Austin
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2018
资助国家：
美国
起止时间：
2018-09-01 至 2022-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1812351&HistoricalAwards=false
关键词：
CSR Small Runtime Verification Concurrent

项目摘要

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.

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