Source: https://patents.google.com/patent/US6704923?oq=inventor%3A%22Arthur+R.+Hair%22
Timestamp: 2018-03-22 21:57:40
Document Index: 619327379

Matched Legal Cases: ['art 1', 'art 2', 'art 1', 'art 1', 'art 2', 'art 1', 'art 2']

US6704923B1 - System and method for pre-verification of stack usage in bytecode program loops - Google Patents
US6704923B1
US6704923B1 US09514536 US51453600A US6704923B1 US 6704923 B1 US6704923 B1 US 6704923B1 US 09514536 US09514536 US 09514536 US 51453600 A US51453600 A US 51453600A US 6704923 B1 US6704923 B1 US 6704923B1
US09514536
This application is a continuation of patent application Ser. No. 08/858,793, filed May 19, 1997, now U.S. Pat. No. 6,075,940, which was a division of patent application Ser. No.08/359,882, filed: Dec. 20, 1994, now U.S. Pat. No. 5,668,999.
As represented generally in FIG. 1, in a typical prior art networked computer system 100, a first computer 102 may download a computer program 103 residing on a second computer 104. In this example, the first user node 102 will typically be a user workstation having a central processing unit 106, a user interface 108, a primary memory 110 (e.g., random access memory) for program execution, a secondary memory 112 (e.g., a hard disc) for storage of an operating system 113, programs, documents and other data, and a modem or other communication interface 114 for connecting to a computer network 120 such as the Internet, a local area network or a wide area network. The computers 102 and 104 are often called “nodes on the network” or “network nodes.”
To avoid detailed analysis of the bytecode program's instruction sequence flow, and to avoid verifying bytecode instructions multiple times, all points (called multiple-entry points) in the specified program that can be can be immediately preceded in execution by two or more distinct bytecodes in the program are identified. In general, at least one of the two or more distinct bytecodes in the program will be a jump/branch bytecode. During processing of the specified program, the verifier takes a “snapshot” of the virtual operand stack immediately prior to each multiple-entry point (i.e., subsequent to any one of the preceding bytecode instructions), compares that snapshot with the virtual operand stack state after processing each of the other preceding bytecode instructions for the same multiple-entry point, and generates a program fault if the virtual stack states are not identical.
FIGS. 4A-4G represent a flow chart of the bytecode program verification process in the preferred embodiment of the present invention.
Accordingly, a plurality of bytecodes are included within the instruction set to perform the same basic function (for example to add two numbers), with each such bytecode being used to process only data of a corresponding distinct data type. In addition, the OAK instruction set is notable for instructions not included. For instance, there are no “computed goto” instructions in the OAK language instruction set, and there are no instructions for modifying object references or creating new object references (other than copying an existing object reference). These two restrictions on the OAK instruction set, as well as others, help to ensure that any bytecode program which utilizes data in a manner consistent with the data type specific instructions in the OAK instruction set will not violate the integrity of a user's computer system.
In the preferred embodiment, the available data types are integer, long integer, short integer (16 bit signed integer), single precision floating point, double precision floating point, byte, character, and object pointer (sometimes herein called an object reference). The “object reference” data type includes a virtually unlimited number of data subtypes because each “object reference” data type can include an object class specification as part of the data type. In addition, constants used in programs are also data typed, with the available constant data types in the preferred embodiment comprising the data types mentioned above, plus class, fieldref, methodref, string, and Asciz, all of which represent two or more bytes having a specific purpose.
Referring now to FIG. 3, the execution of th e bytecode program verifier 240 will be explained in conjunction with a particular bytecode program 340. The verifier 240 uses a few temporary data structures to store information it needs during the verification process. In particular, the verifier 240 uses a stack counter 342, a virtual stack 344, a virtual local variable array 345, and a stack snapshot storage structure 346.
where “R” in the virtual stack indicates an object reference and each “I” in the virtual stack indicates an integer. Furthermore, the stack counter 342 in this example would store a value of 3, corresponding to three values being stored in the virtual stack 344.
Data of each possible data type is assigned a corresponding virtual stack marker value, for instance: integer (I), long integer (L), single precision floating point number (F), double precision floating point number (D), byte (B), short (S), and object reference (R). The marker value for an object reference will often include an object class value (e.g., R:point, where “point” is an object class).
One aspect of program verification in accordance with present invention is verification that the number and data type of the operands in the operand stack status is identical every time a particular instruction is executed. If a particular bytecode instruction can be immediately preceded in execution by two or more different instructions, then the virtual stack status immediately after processing of each of those different instructions must be compared. Usually, at least one of the different preceding instructions will be a conditional or unconditional jump or branch instruction. A corollary of the above “stack consistency” requirement is that each program loop must not result in a net addition or reduction in the number of operands stored in the operand stack.
The stack snapshot storage structure 346 is used to store “snapshots” of the stack counter 342 and virtual stack 344 to enable efficient comparison of the virtual stack status at various points in the program. Each stored stack snapshot is of the form:
“Target” instructions are defined to be all bytecode instructions that can be the destination of a jump or branch instruction. For example, a conditional branch instruction includes a condition (which may or may not be satisfied) and a branch indicating to which location (target) in the program the execution is “jump” in the event the condition is satisfied. In evaluating a conditional jump instruction, the verifier 300 utilizes the stack snapshot storage structure 346 to store both the identity of the target location (in the directory portion 348) and the status of the virtual stack 344 (in the snapshot portion 350) just before the jump. The operation of the stack snapshot storage structure 346 will be explained in greater detail below in conjunction with the description of the execution of the bytecode verifier program.
Referring to FIG. 4E, if the currently selected instruction causes a conditional or unconditional jump or branch forward in the program beyond the ordinary sequential step operation (step 480) the verifier will first check (482) to see if a snapshot for the target location of the jump instruction is stored in the stack snapshot storage structure 346. If a stack snapshot has not been stored, then the virtual stack configuration (subsequent to any virtual stack updates associated with the jump) is stored (484) in the stack snapshot storage structure 346 at a location associated with the target program location. Note that any stack pop operations associated with the jump will have already been reflected in the virtual stack by the previously executed step 460 (see FIG. 4C) .
If a stack snapshot has been stored (indicating that another entry point associated with this target instruction has already been processed), then the verifier compares (486) the virtual stack snapshot information stored in the snapshot portion 340 of the stack snapshot storage structure 346 with the current state of the virtual stack. If the comparison shows that the current state and the snapshot do not match, then an error message is generated (488) identifying the place in the bytecode program where the stack status mismatch occurred. In the preferred embodiment, a mismatch will arise if the current virtual stack and snapshot do not contain the same number or types of entries. Furthermore, a mismatch will arise if one or more data type values in the current virtual stack do not match corresponding data type values in the snapshot. The verifier will then set a verification status value 245 for the program to false and abort (490) the verification process. If a stack status match is detected at step 486, then the verifier continues processing at step 500 (FIG. 4F) .
If the verifier returns a “verification failure” value (564), the attempt to execute the specified bytecode program is aborted by the interpreter (566).
If the verifier 242 returns a “Verification Success” value (564), the specified bytecode program is linked (568) to resource utility programs and any other programs, functions and objects that may be referenced by the program. Such a linking step is a conventional pre-execution step in many program interpreters. Then the linked bytecode program is interpreted and executed (570) by the interpreter. The bytecode interpreter of the present invention does not perform any operand stack overflow and underflow checking during program execution and also does not perform any data type checking for data stored in the operand stack during program execution. These conventional stack overflow, underflow and data type checking operations can be skipped by the present invention because the interpret has already verified that errors of these types will not be encountered during program execution.
BYTECODES IN OAK LANGUAGE
INSTRUCTION NAME SHORT DESCRIPTION
aaload load object reference from array
aastore store object reference into object reference
aconst_null push null object
aload load local object variable
areturn return object reference from function
arraylength get lenth of array
astore store object reference into local variable
astore_<n> store object reference into local variable
athrow throw exception
bipush push one-byte signed integer
breakpoint call breakpoint handler
catchsetup set up exception handler
catchteardown reset exception handler
checkcast make sure object is of a given type
df2 convert double floating point number to single
precision floating point number
d2i convert double floating point number to integer
d2l convert double floating point number to long
dadd add double floating point numbers
daload load double floating point number from array
dastore store double floating point number into array
dcmpg compare two double floating point numbers
(return 1 on incomparable)
dcmpl compare two double floating point numbers
(return −1 on incomparable)
dconst_<d> push double floating point number
ddiv divide double floating point numbers
dload load double floating point number from local
dload_<n> load double floating point number from local
dmod perform modulo function on double floating
dmul miltiply double floating point numbers
dneg negate double floating point number
dreturn return double floating point number from
dstore store double floating point number into local
dstore_<n> store double floating point number into local
dsub subtract double floating point numbers
dup duplicate top stack word
dup2 duplicate top two stack words
dup2_×1 duplicate top two stack words and put two
dup2_×2 duplicate top two stack words and put three
dup_×1 dulicate top stack word and put two down
dup_×2 duplicate top stack word and put three down
f2d convert single precision floating point number
to double floating point number
f2i convert single precision floating point number
f2l convert Single precision floating point number
to long integer
fadd add single precision floating point numbers
faload load single precision floating point number
fastore store into single precision floating point
fempg compare single precision floating point
numbers (return 1 on incomparable)
fempl compare Single precision floating point
numbers (return −1 on incomparable)
fconst_<f> push single precision floating point number
fdiv divide single precision floating point numbers
fload load single precision floating point number
from local variable
fload_<n> load single precision floating point number
fmod perform modulo function on single precision
fmul multiply single precision floating point
fneg negate single precision floating point number
freturn return single precision floating point number
fstore store single precision floating point number
into local variable
fstore_<n> store single precision floating point number
fsub subtract single precision floating point numbers
getfield fetch field from object
getstatic set static field from class
goto branch always
i2d convert integer to double floating point number
i2f convert integer to single precision floating
i2l convert integer to long integer
iadd add integers
iaload load integer from array
iand boolean AND two integers
iastore store into integer array
iconst_<n> push integer
iconst_m1 push integer constant minus 1
idiv integer divide
if_acmpeq branch if objects same
if_acmpne branch if objects not same
if_icmpeq branch if integers equal
if_icmpge branch if integer greater than or equal to
if_icmpgt branch if integer greater than
if_icmple branch if integer less than or equal to
if_icmpit branch if integer less than
if_icmpne branch if integers not equal
ifeq branch if equal to 0
ifge branch if greater than or equal to 0
ifgt branch if greater than 0
ifle branch if less than or equal to 0
iflt branch if less than 0
ifne branch if not equal to 0
iinc increment local variable by constant
iload load integer from local variable
iload_<n> load integer from local variable
imod peform modulo function on integers
imul multiply integers
ineg negate integer
instanceof determine if object is of given type
int2byte convert integer to signed byte
int2char convert integer to char
invokeinterface invoke interface method
invokemethod invoke class method
invokesuper invoke superclass method
ior boolean OR two integers
ireturn return integer from function
ishl integer shift left
ishr integer arithmetic shift right
istore store integer into local variable vindex
istore_<n> store integer into local variable n
isub subtract integers
iushr integer logical shift right
ixor boolean XOR two integers
12d convert long integer into double floating point
12f convert long integer into single precision
12i convert long integer into integer
ladd add long integers
laload load long integer from array
land boolean AND two long integers
lastore store into long integer array
lcmp compare long integers
lconst_<l> push long integer constant
ldc1 push item from constant pool
ldc2 push item from constant pool
ldc2w push long or double from constant pool
ldiv divide long integers
lload load long integer from local variable
lload_<n> load long integer from local variable
lmod perform modulo function on long integers
lmul multiply long integers
lneg Negate long integer
lookupswitch Access jump table by key match and jump
lor boolean OR two long integers
lreturn return long integer from function
lshl long integer shift left
lshr long integer arithmetic shift right
lstore store long integer into local variable
lstore_<n> store long integer into local variable
lsub subract long integers
lushr long integer logical shift right
lxor boolean XOR long integers
monitorenter enter monitored region of code
monitorexit exit monitored region of code
new create new object
newarray allocate new array
newfromname create new object from name
nop do nothing
pop pop top stack word
pop2 pop top two stack words
putfield set field in object
putstatic set static field in class
return return (void) from procedure
saload load signed byte from array
sastore store into signed byte array
siaload load unsigned short from array
siastore store into unsigned short array
sipush push two byte signed integer
tableswitch access jump table by index and jump
verifystack verify stack empty
Pseudocode for OAK Bytecode Verifier
Create Virtual Operand Stack Data Structure for storing stack status
information and Virtual Local Variable Array for storing local variable
data type information.
First Pass through Bytecode Program:
Locate all instructions that are the targets of conditional and
unconditional jumps or branches (i.e., can be entered from more than
one prior instruction).
Store list of such target instructions in Virtual Stack Snapshot data
Second Pass through Bytecode Program:
Do Until Last Bytecode Instruction has been processed:
Select next bytecode instruction (in sequential order in program)
If instruction is in list of target instructions
Compare current state of virtual stack with stored snapsh
Compare data type of each operand popped from stack with
data type required (if any) by the bytecode instruction
Print message identifying place in program that overfiow
Add information to Virtual Stack indicating data type of data
pushed onto operand stack
Case=Instruction is a forward jump or branch instruction
If snapshot of virtual stack for the target instruction already
Compare current state of virtual stack with stored
stack mismatch occurred
Store snapshot of current virtual stack state as snapshot
for the target instruction;
Case=Instruction is an end of loop backward jump or other
backward jump or branch instruction:
Compare current virtual stack state with stored snapshot for
Case=Instruction reads data from local variable
Compare data type of each datum read from local variable
with data type required (if any) by the bytecode instruction
Case=Instruction stores data into a local variable
If corresponding virtual local variable alteady stores a data
Compare data type value stored in virtual local variable
with data type of datum that would be stored in the
corresponding local variable (as determined by the data
type handled by the current bytecode instruction)
Add information to Virtual Local Variable indicating data
type of data that would be stored in corresponding local
} /* End of Do Loop */
Pseudocode for Bytecode Interpreter
Interpret and execute Specified Bytecode Program instructions without
(B1) determining the state of a virtual stack associated with the program before execution of each bytecode in the program, the virtual stack state storing data type values for operands that would be stored in an operand stack during execution of the program;
step B includes:
step B including, processing each bytecode in the program, including processing at least a subset of the bytecodes in the program by: (B4A) determining if a snapshot for a successor program location, comprising a program location that contains a bytecode executable immediately after the bytecode being processed, has previously been stored, (B4B) if the determination is positive, comparing the virtual stack state subsequent to the execution of the jump/branch bytecode being processed with the previously stored virtual stack state snapshot for the successor program location and generating a program fault signal if the virtual stack state is not compatible with the previously stored virtual stack state snapshot for the successor program location, and (B4C) if the determination is negative, storing a snapshot for the successor program location, comprising a snapshot of the virtual stack state subsequent to the execution of the jump/branch bytecode being processed.
stack status tracking instructions for determining the state of a virtual stack associated with the program before execution of each bytecode in the program, the virtual stack state storing data type values for operands that would be stored in an operand stack during execution of the program;
during a second pass through the program, processing each bytecode in the program, including processing each jump/branch bytecode in the program by: (A) determining for each successor program location, comprising each program location in the snapshot list that contains a bytecode that is executable immediately after the jump/branch bytecode being processed, whether or not a snapshot of the virtual stack state for that program location has previously been stored, (B) it the determination is positive, comparing the virtual stack state subsequent to the execution of the jump/branch bytecode being processed with the previously stored virtual stack state snapshot for the successor program location and generating a program fault signal if the virtual stack state is not compatible with the previously stored virtual stack state snapshot for the successor program location, and (C) if the determination is negative, storing a snapshot for the successor program location, comprising a snapshot of the virtual stack state subsequent to the execution of the jump/branch bytecode being processed.
US09514536 1994-12-20 2000-02-28 System and method for pre-verification of stack usage in bytecode program loops Expired - Fee Related US6704923B1 (en)
US08858793 Continuation US6075940A (en) 1994-12-20 1997-05-19 System and method for pre-verification of stack usage in bytecode program loops
US6704923B1 true US6704923B1 (en) 2004-03-09
ID=31891087
US09514536 Expired - Fee Related US6704923B1 (en) 1994-12-20 2000-02-28 System and method for pre-verification of stack usage in bytecode program loops
US (1) US6704923B1 (en)
EP1708083A1 (en) * 2005-03-31 2006-10-04 Sun Microsystems, Inc. Supporting dynamically-typed languages in typed assembly languages
US20080052498A1 (en) * 2006-08-28 2008-02-28 International Business Machines Corporation Runtime code modification in a multi-threaded environment
US20110072417A1 (en) * 2009-03-16 2011-03-24 Dinakar Dhurjati Directed testing for property violations
US8843908B2 (en) 2010-12-23 2014-09-23 Microsoft Corporation Compiler validation via program verification
US9306956B2 (en) * 2013-04-30 2016-04-05 Globalfoundries Inc. File system level data protection during potential security breach
US3878513A (en) 1972-02-08 1975-04-15 Burroughs Corp Data processing method and apparatus using occupancy indications to reserve storage space for a stack
EP0424056A2 (en) 1989-10-16 1991-04-24 Ge Fanuc Automation North America, Inc. Programmable logic controllers and the expression of relay ladder diagrams
US5179734A (en) 1984-03-02 1993-01-12 Texas Instruments Incorporated Threaded interpretive data processor
US5422992A (en) 1992-04-30 1995-06-06 Ricoh Company, Ltd. Method and system to handle state variables in a document processing language
US5446875A (en) 1989-08-17 1995-08-29 Fujitsu Limited System to pass through resource information
EP0718764A2 (en) 1994-12-20 1996-06-26 Sun Microsystems, Inc. Bytecode program interpreter apparatus and method with pre-verification of data type restrictions
US5590329A (en) 1994-02-04 1996-12-31 Lucent Technologies Inc. Method and apparatus for detecting memory access errors
"A Postscript Backgrounder," Seybold Report On Desktop Publishing, vol. 5, No. 7, Mar. 4, 1991 p. 9(1).
Adobe Systems Inc., "PostScript Language Reference Manual Second Edition," 1990, pp. 23-143.
Ahamad et al., "An Application of Name Based Addressing to Low Level Distributed Algorithms," Jan. 1985, IEEE Transactions On Software Engineering, vol. SE-11, No. 1, p. 59.
Almes et al., "Edmas: A Locally Distributed Mail System," Department of Computer Science, University of Washington Seattle, Technical Report 83-07-01, Jul. 7, 1983, pp. 1-17.
Almes et al., "Edmas: An Object-Oriented, Locally Distributed Mail System," Department of Computer Science, FR-35 University of Washington Seattle, Technical Report 84-08-03, Dec. 13, 1984, pp. 1-19.
Almes et al., "Research in Integrated Distributed Computing," Department of Computer Science, University of Washington Seattle, Oct. 1979 pp. 1-42.
Almes et al., "The Eden System: A Technical Review," Department of Computer Science, University of Washington Seattle, Technical Report 83-10-05, Oct. 1983, pp. 1-25.
Almes et al., "The Eden System: A Technical Review," Jan. 1985, IEEE Transactions On Software Engineering, vol. SE-11, No. 1, pp. 43-58.
Almes, Guy. T, "Eden Project Proposal," Department of Computer Science, University of Washington Seattle, Technical Report 80-10-01, Oct. 1980, pp. i-ii.
Almes, Guy. T, "Integration and Distribution in the Eden System," Department of Computer Science, University of Washington Seattle, Technical Report 83-01-02, Jan. 19, 1983, pp. 1-18.
Almes, Guy. T, "The Evolution of the Eden Invocation Mechanism," Department of Computer Science, University of Washington Seattle, Technical Report 08-01-03, Jan. 19, 1983, pp. 1-14.
Auerbach et al., "High-Level Language Support for Programming Distributed Systems," IEEE Transactions On Software Engineering, 1992 p. 320.
Bertz, David., "Drool Over A Little Language That Sports Multiple Inheritance," Dr. Dobb's Journal, vol. 18, No. 11, p. 74(4), Oct. 1993.
Bertz, David., "Embedded Languages : ExTalk Allows Users To Extend The Capabilities Of Your Application Programs," BYTE Nov. 1988; pp. 419-423; vol. 13, No. 12.
Bertz, David., Your Own Tiny Object-Oriented Language: C++? Smalltalk? What About Bob? (An interpreter formed from C++ and Lisp) Dr. Dobb's Journal, Sep., 1991, vol. 16, No. 9, p.26(8).
Betz, David, "EMBEDDED LANGUAGES: ExTalk Allows user to extend the capabilities of your application programs", BYTE, vol. 13, No. 12, Nov. 1988, p. 419.
Betz, David, "Your own tiny object-oriented language: C ++? Smalltalk? What about Bob?", Dr Dobb's Journal, vol. 16, No. 9, Sep. 1993, p. 26(8).
Black et al., "Distribution and Abstract Types in Emerald," Department of Computer Science, University of Washington Seattle, Technical Report 85-08-05, Aug. 1985, pp. 1-10.
Black et al., "Distribution and Abstract Types in Emerald," IEEE Transactions On Software Engineering, vol. SE-13 No. 1 Jan. 1987, pp. 65-76.
Black et al., "Distribution and Abstract Types In Emerald," University of Washington Seattle, Technical Report 86-02-04, pp. 1-189.
Black et al., "Object Structure in the Emerald System," University of Washington Seattle, Technical Report 86-04-03, pp. 1-9.
Black et al., "The Eden Project: A Final Report," Department of Computer Science, University of Washington Seattle, Technical Report 86-11-01, pp. 1-28.
Black eta l., "A Language For Distributed Programming" Department of Computer Science, University of Washington, Technical Report 86-02-03, Feb. 1986, p. 10.
Black, Andrew P. ,Supporting Distributed Applications: Experience With Eden Department of Computer Science, University of Washington Seattle, Technical Report 85-03-02, Mar. 1985, pp. 1-21.
Black, Andrew P., "Supporting Distributed Applications: Experience With Eden," University of Washington Seattle, Presentation at Tenth ACM Symposium on Operating System Principles, Sep. 1985, pp. 1-14.
Black, Andrew P., "The Eden Programming Language," Department of Computer Science, FR-35 University of Washington Seattle, Technical Report 85-09-01, Sep. 1985, pp. 1-19.
Cardelli, L., "The Amber Machine," Proceedings Of The Thirteenth Spring School Of The LITP Proceedings, 1986, pp. 48-70.
Cardelli, Luca, "The Amber Machine", Proceedings of the Thirteenth Spring School of the LITP, May 6-10, 1985, pp. 48-70.
Chambers, Craig, et al., "An Efficient Implementation of SELF, a Dynamically-Typed Object-Oriented Language Based on Phototypes", OOSPLA '89 Proceedings, Oct. 1-6, 1989, ACM SIGPLAN NOTICES, vol. 24, No. 10, Oct. 1989, pp. 49-70.
Chambers, Craig.,An Efficient Implementation of SELF, A Dynamically-Typed Object Oriented Language Based On Prototypes Conference Proceedings, Special Issue of SIGPLAN Notices, vol. 24, No.: 10, Oct. 1989.
Chung et al., "A "Tiny" Pascal Compiler Part 1: The P-Code Interpreter," BYTE Publications, Sep. 1978, pp. 58-65, 148-155.
Chung et al., "A "Tiny" Pascal Compiler Part 2: The P-Compiler" BYTE Publications, Sep. 1978, pp. 34-52.
Duff, Charles B., "Designing An Efficient Language," BYTE, Aug. 1986, p. 211.
Franks, Neville., "Adding An Extension Language To Your Software: The Little Language/Application Interface" Dr. Dobb's Journal, Sep. 1991, vol. 16, No. 9, p. 34(6).
Goldberg et al., "Smalltalk-80 The Language and its Implementation,"Xerox Palo Alto Research Center pp. 1-707.
Goldberg, Adele, et al., "Smalltalk-80: The Language and its Implementation", Addison-Wesley Publishing Company, 1983.
Gosling et al., "The Java Language Environment A White Paper," The Java Language Environment, Sun Microsystems, Oct. 1995, pp. 1-84.
Gosling, James., "Bytecode Program Interpreter Apparatus And Method With Pre-Verification Of Data Type Restrictions", US Application Ser. No.: 08/360,202, Filed Dec. 21, 1994 pp. 1-41 (Pat. No. 5,748,964).
Gosling, James., "Java Intermediate Bytecodes" ACM SIGPLAN Workshop On Intermediate Representations (IR '95), Jan. 1995, San Francisco, ACM SIGPLAN Notices, vol. 30, No. 3, Mar. 1995 pp. 111-118.
Gosling, James., "System And Method For Pre-Vertification Of Stack Usage In ByteCode Program Loops", US Application Ser. No.: 08/359,882, Filed Dec. 20, 1994 pp. 1-38 Fig 1-5 (Pat. No. 5,668,999).
Grimaud et al., "FACADE: A Typed Intermediate Language Dedicated To Smart Cards," Software Engineering Notes, Association For Computing Machinery. New York, US, vol. 24, No. 6, Sep. 6, 1999, pp. 476-493.
Guibas et al., "Compilation and Delayed Evaluation In APL," Fifth Annual ACM Symposium On Principles Of Programming Languages, Jan. 23-25, 1978, 1-8.
Guttman et al., "The VLISP Verified Scheme System," LISP And Symbolic Computation: An International Journal, 8, 1995, pp. 33-110.
Holman et al., "The Eden Shared Calender System," Department of Computer Science, FR-35, University of Washington Seattle, Technical Report 85-05-02, Jun. 22, 1985, pp. 1-14.
Hsu, Felix Shamson., "Reimplementing Remote Procedure Calls," University of Washington, Masters Thesis, 1985, pp. 1-76.
Hutchinson, Norman C., "An Object Based Language for Distributed Programming," University of Washington, Dissertation for Doctor of Philosophy, 1987, pp. 1-103.
IBM Technical Disclosure Bulletin, "Intrinsic Language Of Syntax For Setting And Accessing Instance Variables In An Object-Oriented Environment", 1990, vol. 33(1B), pp. 408-410.
Johnston, Robert L., "The Dynamic Incremental Compiler of APL/3000," Association of Computing Machinery, May 30-Jun. 1, 1979, vol. 9 No. 4-Part 1, pp. 82-87.
Jul et al., "Fine-Grained Mobility in the Emerald System," University of Washington, ACM Transactions On Computer Systems, vol. 6, No. 1., Feb. 1988, pp. 109-133.
Jul, Eric., "Object Mobility in a Distributed Object Oriented System," University of Washington Dissertation for Doctor Of Philosophy, 1989, pp. 1-154.
Kinchin, Corinna., "Postscript: P.S. it's a programming language, too!" EXE, vol. 6, No. 1, Jun. 1991, p. 66(5).
King, James C., "A Program Verifier," IBM Thomas J. Watson Research Center. Yorktown Heights, New York 10598, USA.
Kin-Man Chung and Herbert Yuen, "A 'Tiny' Pascal Complier; Part 1: The P-Code Interpreter," BYTE Publications, Inc., Sep. 1978.
Kin-Man Chung and Herbert Yuen, "A 'Tiny' Pascal Complier; Part 2: The P-Compiler," BYTE Publications, Inc., Oct. 1978.
Kin-Man Chung and Herbert Yuen, "A ‘Tiny’ Pascal Complier; Part 1: The P-Code Interpreter," BYTE Publications, Inc., Sep. 1978.
Kin-Man Chung and Herbert Yuen, "A ‘Tiny’ Pascal Complier; Part 2: The P-Compiler," BYTE Publications, Inc., Oct. 1978.
Korfhage et al., "Hermes Language Experiences," Software-Practice and Experience, vol. 25(4), Apr. 1995, p. 389.
Korfhage, Willard, et al., "Hermes Language Experience", Software-Practice and Experience, vol. 25, No. 4, Apr. 1995, pp. 389-402.
Krasner, Glen., "Smalltalk-80 Bits of History, Words of Advice," Xerox Palo Alto Research Center, 1983, pp. 1-343.
Lazowska et al.,"The Architecture of the Eden System," Proceedings of the Eighth Symposium On Operating System Principles, Dec. 14-16, 1981, Asilomar Conference Grounds, Pacific Grove, California, Dec. 1981, vol. 15, No. 5.
McDaniel, Gene.,"An Analysis of a Mesa Instruction Set," Association for Computing Machinery, Xerox Palo Alto Research Center, May 1982.
Mitchell et al., "Mesa Language Manual," Xerox Palo Alto Research Center, Palo Alto, California pp. 1-147.
Perrott et al.,"A Supercomputer Program Development System," Software-Practice and Experience, Oct. 1987, vol. 17 (10), pp. 663-668.
Pier, Kenneth A., "A Retrospective on the Dorado, A High-Performance Personal Computer," Association for Computing Machinery, Xerox Palo Alto Research Center, 1983, pp. 252-269.
Proudfoot, Andrew Blaine., "Replects: Data Repliation in the Eden System," University of Washington, Department of Computer Science, Technical Report No. TR-85-12-04, pp. 1-154.
Pu, Calton., "Replication and Nested Transactions in the Eden Distributed System.," University of Washington, Department of Computer Science, Dissertation for Doctor of Philosophy, 1986, pp. 1-179.
Reznik, Assaf, "Character simulation with ScriptX, a general-purpose farmework for dynamic behavior", Dr. Dobb's Journal, vol. 19, No. 13, Nov. 1994, p. 76(6).
Rose et al., "Lightweight ByteCode Verification", Extended Abstract For FUJ'98, Sep. 21, 1998, pp. 1-23.
Schauer, H., "Architektur und Implementierung eines PASCAL-Systems für Mikrocomputer", Elektronische Rechenanlagen, vol. 24, No. 3, Jun. 1982, pp. 108-117.
Shih et al., "An Automated Design Specification and Verification Tool for Systolic Architectures", IEEE, 1992, pp. 6-17.
Strom et al., "Extending Typestate Checking Using Conditional Liveness Analysis." IEEE Transactions On Software Engineering, vol. 19, No. 5, May 1993, p. 478.
Strom et al., "NIL: An Integrated Language and System For Distributed Programming," Association for Computing Machinery, 1983, p. 73.
Strom, Robert E., et al., "Hermes: A Language for Distributed Computing", Prentice Hall, 1991, pp. 67-71, 109-123.SIGPLAN Debates (1996), pp. 5-10.
Takahashi et al., "Validating Network Protocols Using A Flexible Verifier", IEEE, 1994, pp. 811-817.
Thompson, Ken., "Regular Expression Search Algorithm," Communications of the ACM, vol. 11, No. 6, Jun. 1968, pp. 419-422.
Ungar et al., "Object, Message, and Performance: How They Coexist In Self," Computer, vol. 25 No. 10, Oct. 1, 1992, pp. 53-64.
Wang et al., "A Verifier for Distributed Real-Time Systems with Bounded Integer Variables", IEEE, 1993, pp. 135-151.
Wright et al., "A Practical Soft Type System for Scheme," LISP 94, Jun. 1994, Orlando, Florida, pp. 250-262.
Wright, Andrew K., et al., "A Practical Soft Type System for Scheme", LISP 94-Jun. 1994 Orlando, Florida, pp. 250-262.
Wright, Andrew K., et al., "A Practical Soft Type System for Scheme", LISP 94—Jun. 1994 Orlando, Florida, pp. 250-262.
Yellin, Dan.,"Do Programmers Need Seat Belts?" ACM SIGPLAN Debates (1996), p. 5.
US20080276223A1 (en) * 2005-01-11 2008-11-06 Morgan Fabian F Dynamic Source Code Analyzer
US7478367B2 (en) 2005-01-11 2009-01-13 International Business Machines Corporation Dynamic source code analyzer
US8572572B2 (en) 2005-01-11 2013-10-29 International Business Machines Corporation Dynamic source code analyzer
US7574700B2 (en) 2005-03-31 2009-08-11 Sun Microsystems, Inc. Supporting dynamically-typed languages in typed assembly languages
US8584111B2 (en) * 2006-08-28 2013-11-12 International Business Machines Corporation Runtime code modification in a multi-threaded environment
US8589900B2 (en) * 2006-08-28 2013-11-19 International Business Machines Corporation Runtime code modification in a multi-threaded environment
US20080052697A1 (en) * 2006-08-28 2008-02-28 International Business Machines Corporation Runtime code modification in a multi-threaded environment
US8572596B2 (en) * 2006-08-28 2013-10-29 International Business Machines Corporation Runtime code modification in a multi-threaded environment
US20080052725A1 (en) * 2006-08-28 2008-02-28 International Business Machines Corporation Runtime code modification in a multi-threaded environment
US6374286B1 (en) 2002-04-16 Real time processor capable of concurrently running multiple independent JAVA machines
US20060200663A1 (en) 2006-09-07 Methods for describing processor features