Murali
Sitaraman and Greg Kulczycki
Dept. of Computer Science
Clemson University
451 Edwards Hall
Clemson, SC 29634-0974 USA
{murali, gregwk}@cs.clemson.edu
Phone: +1 864 656 3444
URL: http://www.cs.clemson.edu/~resolve
RESOLVE concepts are designed so that a client can write defensive programs if he chooses to do so. This ability to defend should also be available against situations where a client wants to be sure that there is enough memory to declare variables, facilities, or call certain procedures. This is a proposal for accomplishing this objective.
Keywords
Specification of displacement requirements, checking
Paper Category: technical paper
Emphasis: research and education1. Introduction
The objective of this position paper is to illustrate how to add checks for displacements to simply bounded, communal, and globally-bounded modules.The rest of this document discusses how to achieve the goal of providing defensiveness against displacement violations (including language support), and introduces the need for ghost facilities in the process.
2. Examples to Illustrate Technical Details
Concept Stack_Template(type Entry; evaluates Max_Depth: Integer);
uses Std_Integer_Fac, String_Theory;
requires Max_Depth > 0;
Type Family StackÍ Str(Entry);
exemplar S;
constraints ½S½ £ Max_Depth;
initialization
requires Stack.Disp(L) £ Rem_Mem_Cap;
ensures S = L;
Operation Push(alters E: Entry; updates S: Stack);
requires ½S½ < Max_Depth;
ensures S = <#E> ° #S;
Operation Pop(replaces R: Entry; updates S: Stack);
requires ½S½ > 0 ;
ensures #S = <R> ° S;
Operation Depth( restores S: Stack ): Integer;
ensures Depth = (½S½);
Operation Rem_Capacity( restores S: Stack ): Integer;
ensures Rem_Capacity = (Max_Depth -½S½);
Operation Clear(clears S: Stack);
end Stack_Template;
Discussion
We believe that there is a fundamental difference between truly temporary displacement needed to perform a procedure call versus the displacement needed to create a new bounded stack or push an additional entry on a globally-bounded stack. This is because a runtime system can set aside sufficient memory to handle a nominal number of procedure calls. "Out of memory" errors are more likely to occur on facility and variable initializations and certain operations on globally-bounded concepts (and infrequently-used recursive calls).
Displacement is an operation implicitly declared on every type and a procedure for it is provided by an implementation. Like initialization, the code for this procedure is often automatic, and therefore, can be omitted. The type initialization requires clause is automatic, but we may decide to leave it in till becomes entrenched.
Client Usage
If SF.Stack.Displacement ( ) <= Rem_Mem_Cap( ) then
Var S:SF.Stack;
Example #2
Concept Stack_Template(type Entry);
uses Std_Integer_Fac, String_Theory;
Type Family StackÍ Str(Entry);
exemplar S;
constraints ½S½ £ Max_Depth;
initialization
requires Stack.Disp(L) £ Rem_Mem_Cap;
ensures S = L;
Defines Push_Disp: N+;
Operation Push(alters E: Entry; updates S: Stack);
requires Push_Disp £ Rem_Mem_Cap;
ensures S = <#E> ° #S;
Operation Push_Displacement: Integer;
ensures Push_Displacement = (Push_Disp);
Operation Pop(replaces R: Entry; updates S: Stack);
requires ½S½ > 0 ;
ensures #S = <R> ° S;
Operation Depth( restores S: Stack ): Integer;
ensures Depth = (½S½);
Operation Clear(clears S: Stack);
end Stack_Template;
Figure 1: A Concept for Locally Bounded Stack_Template
Client Usage
If SF.Push_Displacement ( ) <= Rem_Mem_Cap( ) then
Push(E, S);
Example #3
Concept Communal_Stack_Template(type Entry;
evaluates Total_Max_Depth: Integer);
uses Std_Integer_Fac, String_Theory;
requires Tot_Max_Depth > 0;
Defines Disp;
Facility initialization
requires Disp £ Rem_Mem_Cap;
Operation Displacement: Integer;
ensures Displacement =( Disp );
…
end Communal_Stack_Template;
Displacement is an operation implicitly declared on every facility and a procedure for it is provided by an implementation. As usual, the code for this procedure is often automatic, and therefore, can be omitted. (This operation is also defined for simply bounded and globally bounded facilities, but it is trivial in those cases.) All related assertions and terms in the concept are pre-defined and automatic, and can be omitted.
Client Usage
Ghost Facilty SF is Communal_Stack_Template(Integer, 1000)
realized by Shared_Realiz;
If SF.Displacement ( ) <= Rem_Mem_Cap( ) then
Ghost SF is permanent;
Facility-wide displacement checking raises a problem because the facility needs to be declared before a question about its displacement requirement can be asked.To solve this problem, we propose ghost facilities.The only operation that can be called on a ghost facility is Displacement. When a ghost facility is declared, all the facilities declared in the ghost facility also become ghost facility declarations automatically.Once the client has checked memory is available, then she can declare the actual facility
Acknowledgments
This research is funded in part by NSF grant CCR-0113181. This draft paper is motivated in part by what we said we would do under the NSF grant and a discussion with Bill Ogden concerning the specification of Location_Referencing_Template.