*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
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:
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.
