CSR: Small: Runtime Verification of Concurrent Programs

University Of Texas At Austin, Austin TX

Investigators

Abstract

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.