Ph.D. Thesis Proposal: Cong Hou

Add to Calendar
Date:
October 8, 2012 1:00 pm - 3:00 pm
Location:
KACB 1315

Ph.D. Thesis Proposal

Title: Synthesis for Program Inversion

Cong Hou
School of Computational Science and Engineering
College of Computing
Georgia Institute of Technology

Date: October 8th (Monday), 2012
Time: 1:00PM - 3:00PM (EDT)
Location: KACB 1315

Committee:

  • Dr. Richard Vuduc (Advisor, School of Computational Science and Engineering, Georgia Tech)
  • Dr. Richard Fujimoto (School of Computational Science and Engineering, Georgia Tech)
  • Dr. Santosh Pande (School of Computer Science,Georgia Tech)
  • Dr. Daniel Quinlan (Lawrence Livermore National Laboratory)
  • Dr. David Jefferson (Lawrence Livermore National Laboratory)

Abstract:
Program inversion has been successfully applied to several areas such as optimistic parallel discrete event simulation (OPDES) and reverse debugging. Given a program P with input state I and output state O, its inverse or reverse program, P-, produces I given O. When P is not injective or reversible, we need to build an instrumented and reversible version of P that we call a forward program and is denoted by P+, so that it becomes possible to construct P- from P+. The instrumented code in P+ stores control flow information and values that cannot be recovered. However, constructing forward and reverse programs manually is a tedious, time-consuming, and error-prone task. We need an automated tool that can generate forward and reverse programs automatically.

In this thesis we introduce an automatic program inversion framework for imperative languages. In our method, we transform the task of program inversion into a problem of retrieving values. Specifically, we build a value search graph (VSG) that explicitly expresses equality relations between values in the program. Values in the graph are represented by single static assignment (SSA) names or constant values. Equalities are detected from assignments, comparisons, some special operations, global value numbering, etc.. Each equality is constrained by a set of control flow paths on which the equality exists. The problem of building forward and reverse programs then becomes a combinatorial search problem on the VSG. The forward and reverse programs are then generated based on the search result.

Using the same framework, we first describe how to retrieve scalar values, then extend it to handling arrays and other data structures (e.g. object access and linked data structure). To handle arrays, we introduce the array subregion representations into the VSG so that the equality between two arrays holds only in the subregion attached to it. Then we retrieve an array by retrieving subregions of it. We also show that object access and linked data structure can be transformed into array-like representations so that the same method will be employed to handle them.