One of the initial problems we were having was figuring out how to model the stack of numbers that each thread manages. One way was to model it as a linked list for each thread. We thought of representing linked lists as a collection of StackFrames referencing to each other with a “next” relation. This would make it easy to find things like the topmost stack frame, or the stack frame that comes after another one. However, it became hard to manage multithreaded environments because StackFrames did not explicitly have a field for which threads they were a part of; the only way to tell which thread a frame was a part of was to find which thread was associated with the end frame connected to this frame. The “next” operation was shared among all the threads, so it was hard to find which “next” tuples belonged to which stack. Also, if every element in every stack requires a StackFrame atom, we would have to know beforehand how many StackFrames need to be in the bounds, and we would have to recycle unused StackFrames to be used in new stacks.

So, we decided to instead represent thread stacks using Int-indexed relations. This makes it easier to to tell which stack belongs to each thread, makes it easier to access specific points into the stack (since we can just use direct Ints now instead of tracing next multiple times), and means that we do not need to keep track of separate StackFrame objects for every item in the stack. The only turnoff is that we would have to deal with the “nasty” Forge arithmetic syntax for all of our stack logic. However, this allowed us to achieve pretty clean stack manipulation logic, since we can more easily refer to any point in the stack with just their indices.

We had to make a similar decision between an indexed array and a linked list for the list of operations, as well. Choosing an indexed array made it easy to add control flow operations that can make a thread jump to an arbitrary point in the operations list.

In our proposal, we expected that we would be able to provide a set of example inputs and outputs, and let Forge search for a sequence of operations (a function) that maps those inputs to those outputs. For simple operations, this worked: for example, the model is able to construct the function “f(n) = (n + 1) * n” from a few input/output pairs. We had also hoped to do this with more complicated functions; in particular, we wondered what conditions would cause the model to find programs that are simply a table of “if”s rather than functions that actually manipulate the inputs. However, it ends up being that even a simple if-table requires too many operations to run in any reasonable amount of time. We had also hoped to try more complicated functions like prime factorization, but decided not to try this when we found that even a simple absolute value function took about 20 minutes to run on 5 inputs (i.e., 5 threads, each with a different starting value).

The visualization displays the states of each thread, in order. Threads are separated by a black line. Within each thread, the light rectangles contain stack states, and the dark rectangles contain states of the operation list. The operation to go from one stack state to another is highlighted in the operation list between them.

We used the file code_generator.py to generate Forge syntax specifying initial stack states, final stack states, and operation lists, so we did not have to write all that by hand.