Browse Prior Art Database

Method for Saving Space on Stack for Recursive and Non-Recursive Function Calls Disclosure Number: IPCOM000016009D
Original Publication Date: 2002-Nov-29
Included in the Prior Art Database: 2003-Jun-21

Publishing Venue



Invention A call index for software model checking Problem When modeling the stack in software model checking in the conventional way, the number of bits needed is prohibitive. As an example, in a conventional stack, every time a procedure or function is called, the program counter is pushed onto the stack. If x bits are needed to represent the program counter, and the stack is y deep, then x*y bits are used. Solution When calling a procedure or function in the modeling process, do not push the program counter onto the stack. Instead, number the calls for each procedure or function. Call this numbering the "call index." Then, push the call index onto a special, narrower stack instead. For example, if the program includes procedures p1(), p2(), and p3(), with p1() being called from only one program location, p2() being called from three different program locations, and p3() being called from two different program locations, then we need two bits to represent the call index. If 10 bits are used to represent the PC, and the stack is 25 deep (current technology, under development), then we have saved 200 10*25 2*25 bits. Since model checking is exponential in the number of bits it uses, this represents a significant savings. However, we still need to interpret the call index. For this purpose, we need a table which tells us how to interpret the call index as a function of the current program counter. Specifically, the table would consist of three columns, with a row for each combination of procedure and call index in the program. The first column would contain the maximum program counter for this procedure. The second column would contain the call index, and the third column would contain the location to return to. When returning from a procedure, we take the current program counter, and find the first row in the table for which the current program counter is less than the value of the first column. Then we read down until we find the value of the call index indicated by our narrow stack. Finally, we return to the location indicated by the third column. In model checking, the table does not cost any bits, since a combinational function comes for free. The problem solved is one in software model checking. However, the same method can be used to save memory in microprocessors, specifically, smart cards