Linked List Reversal

Storyboard

In the storyboard programming framework,  the user describes the desired data structure manipulation by providing a Storyboard, i.e. a set of pairs of abstract input-output examples as shown in the figure below. Each of these input-output pairs are called a scenario, and they are abstract because in addition to concrete nodes, they can also contain summary nodes.

The figure presents an intuitive visualization of the input and output configurations describing the list
reversal. Notice that instead of showing a concrete list of a particular size, the scenario uses a summary node mid to represent the middle part of the list, which may vary in size for different runs of the algorithm. Out of all the nodes in the sublist represented by mid, the first and last node deserve special attention because other nodes outside the set mid are going to be pointing to them. We call these special nodes attachment points of the summary node.

The left part of the figure presents the text notation actually used by our system to describe Scenario 1 on the right; the visualization on the right is generated from this description. The storyboard consists of an environment description followed by a sequence of scenario descriptions. The environment description defines the set of variables used in the implementation, the set of fields in the objects that make up the data structure (which are called selectors in the shape analysis literature), and the set of concrete and summary locations. In the list reverse example, the storyboard defines an environment with four program variables head, temp1, temp2 and temp3, one selector corresponding to the field next which points from a Node to another Node, and six concrete locations a, f, e, b, f' and e'. The concrete locations f and e represent the front and end attachment points of the summary
node mid. Similarly, the concrete locations f' and e' represent the attachment points for the summary node mid', where mid' represents the set of nodes whose next pointers have been reversed.

A scenario description defines the state configuration for the input and output states. Each state configuration is comprised of a set of variable predicates, selector predicates and data constraint predicates. The variable predicates of the form var = loc denote that variable var points to location loc. The selector predicates of the form loc1.sel = loc2 denote that the field sel of location loc1 points to location loc2; we denote such predicates as sel(loc1, loc2) borrowing the notation from shape analysis. The state configuration can also define additional constraints involving the data values of the locations using the data constraint predicates.

unfold and fold operations for ll reverse
The scenario 1 in the figure uses a summary node to convey that the algorithm should work the same way regardless of how long the list is. However, in the case of linked list reversal, one cannot reason about the algorithm without knowing something about the structure of the set of nodes represented by the summary node mid. In the storyboard language, this structure is conveyed through fold and unfold predicates as shown in the figure below; the graphical visualization of these predicates is illustrated towards the right. These rules describe the recursive structure of the summary nodes in terms of their attachment points. For example, the unfold rule shows two alternatives for the summary node mid: either the attachment points f and e are actually the same node x, and this is the only node in mid, or alternatively f is a node x whose next pointer points to the attachment point f of another mid node. For this example, fold is really just an inverse of unfold and could easily be derived automatically.

Control Flow Skeleton

In addition to the fold and unfold, the framework also requires a skeleton of the looping structure of the desired program as shown in controlflowlinklistreversal. The structure says that the implementation should contain one while loop with some blocks of code before and after it, in addition to the block of code inside. The code produced by the synthesizer will have each of these blocks replaced by a series of conditional assignment statements. The challenge is to derive the assignments that will lead the resulting code to satisfy the storyboard.


----------
while(-----)
{
  ----------
}
----------

Synthesized Implementation

The implementation synthesized by the framework for the linked list reverse example is shown below.

Node llReverse(Node head){

  Node temp1 = null, temp2 =null;
  Node temp3 = null;
  temp1 = head;

  while(temp1 != null){
    // unfold temp1;
    head = temp1;
    temp1 = temp1.next;
    head.next = head;
    head.next = temp3;
    temp3 = head;
    // fold head;
  }
}