Browse Prior Art Database

Method for Saving Space on Stack for Recursive and Non-Recursive Function Calls

IP.com Disclosure Number: IPCOM000016009D
Original Publication Date: 2002-Nov-29
Included in the Prior Art Database: 2003-Jun-21
Document File: 2 page(s) / 44K

Publishing Venue

IBM

Abstract

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.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 52% of the total text.

Page 1 of 2

  Method for Saving Space on Stack for Recursive and Non-Recursive Function Calls

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 s...