Method for specifying and verifying multi-threaded object-oriented programs with invariants

• US 7,774,787 B2
• Filed: 01/11/2005
• Issued: 08/10/2010
• Est. Priority Date: 01/11/2005
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Jacobs, Bart, Schulte, Wolfram, Leino, K. Rustan M.
• Primary Examiner(s): An; Meng-Ai
• Assistant Examiner(s): KRISHNAN, NIKHIL R
• Application Number:
  US11/041,014
• Publication Number:
  US 20060155905A1
• Time in Patent Office: 2,037 Days
• Field of Search: 718/100, 718/107, 717/116, 717/131, 715/708, 715/762, 713/1, 712/209, 707/102, 705/1, 702/186, 702/189, 719/316
• US Class Current: 718/107
• CPC Class Codes: G06F 9/526 Mutual exclusion algorithms

Abstract

Various new and non-obvious systems and methods for ensuring within a multi-threaded environment that object fields hold legal values are disclosed. One of the disclosed embodiments is a method for a thread locking the top object of an object hierarchy. The thread then gains ownership of the locked object and any children of the locked object, by successively unpacking child objects, allowing the thread to write to any unpacked object field. By owning the top hierarchical object, the thread also achieves transitive ownership to any descendants of the object, allowing the thread to read any object fields which it transitively owns. When a thread locks an object within this exemplary embodiment all other threads are denied access to the locked object and to any descendants of the locked object.

Claims

1. A method comprising:

executing multiple threads on a computer;

a thread T1 acquiring a lock on a top object in a hierarchy of objects, wherein an invariant condition is specified for the top object, the invariant condition specifies a relation on data of the top object, and the invariant condition references at least two fields, wherein the at least two fields are of at least two different objects;

wherein acquiring the lock changes ownership to thread T1 of the top object;

wherein ownership confers upon thread T1 a right to modify any field of the top object;

wherein the lock excludes all other threads from accessing the top object and any descendant objects in the hierarchy of objects;

after acquiring the lock, unpacking the top object, wherein unpacking the top object comprises designating the top object as being of a mutable state, which allows invariants to be temporarily violated and allows field assignments of the top object that temporarily violate the invariant condition; and

packing the top object, wherein packing the top object comprises verifying that the invariant condition holds and taking the top object from the mutable state to designated as being of a consistent state, wherein being designated as being of a consistent state prevents further modifications.

2. The method of claim 1 wherein each object in the hierarchy of objects is owned by a thread, is owned by an object, or is free.

3. The method of claim 1, wherein at least one modified object field temporarily violates the invariant condition.

4. The method of claim 1, wherein if thread T1 owns the top object of an object hierarchy then thread T1 transitively owns all descendants of the top object and wherein if thread T1 transitively owns a descendant object then allowing the thread T1 to read at least one object field from at least one descendant object.

5. The method of claim 1, wherein the thread Tl gains ownership of a descendent object O1 directly owned by another object O2 by unpacking O2.

6. The method of claim 1, wherein thread T1 can gain ownership of any descendent object O1 directly owned by another object O2 when thread T1 owns object O2.

7. The method of claim 1, wherein

at least one object O1 has an owner field, and each time a thread T1 gains ownership of the object O1, the owner field is updated with a representation of the thread T1;

and

wherein the thread T1 has an owns field and the owns field of thread T1 is updated with a representation of the object O1 with the owner field of O1 being updated.

8. The method of claim 1, wherein:

a program defines the hierarchy of objects; and

the program is verified using one of static verification, model checking, or run-time checking.

9. The method of claim 1, further comprising

an object being created by a thread;

the object initially being owned by the thread that created it;

the object being released prior to a subsequent thread gaining ownership of the object;

wherein prior to the object being released, the invariant condition is established.

10. The method of claim 1 wherein:

packing the top object comprises;

checking that the invariant condition holds; and

generating an error condition if the invariant condition does not hold.

11. A computer-readable storage medium storing computer-executable instructions for causing a computer system to perform the method of claim 1.

12. A computer system having a multi-threaded operating system, the computer system comprising:

one or more processing units;

memory;

at least one thread with a thread table for determining object ownership;

at least two objects hierarchically arranged, at least one object further comprising;

an owner field for determining an entity that owns the at least one object; and

at least one variable field;

a thread-object consistency module which ensures that for each thread-object transition, the thread table indicates that a thread owns the at least one object and the owner field indicates that the at least one object is owned by the thread;

a writer module which writes a value into the variable field if the at least one object is owned by a thread requesting write access;

a representation of an invariant condition specified for a top object of the at least two objects, wherein the invariant condition specifies a relation on data of the top object, and the invariant condition references at least two fields, wherein the at least two fields are in at least two different objects;

a variable indicating whether the invariant condition holds;

wherein an unpack statement switches the variable off and designates the top object as being of a mutable state, which allows invariants to be temporarily violated and allows field assignments of the top object that temporarily violate the invariant condition; and

wherein a pack statement switches the variable on, verifies that the invariant condition holds, and takes the top object from the mutable state to designated as being of a consistent state, wherein being designated as being of a consistent state prevents further modifications.

13. The computer system of claim 12, further comprising a reader module which reads an object if the object is owned by a thread requesting read access.

14. The computer system of claim 13, further comprising an invariant checker, which ensures that the at least one object variable field contains the legal values for the object invariant condition, and which is called after the writer module is accessed for a given object.

15. A method comprising:

executing multiple threads on a computer;

a thread T1 acquiring a lock on an object in a hierarchy of objects, wherein an invariant condition is specified for the object, and the invariant condition specifies a relation on data of the top object, and the invariant condition comprises legal values for at least two fields in two different objects;

wherein acquiring the lock changes ownership to thread T1 of the object;

wherein ownership confers upon thread T1 rights to modify any field of the object;

wherein the lock excludes other threads from accessing the object and any descendant objects in the hierarchy of objects;

after acquiring the lock, unpacking the object, wherein unpacking the object comprises designating the object as being of a mutable state, which allows invariants to be temporarily violated and temporarily allows field assignments of the object that violate the invariant condition;

packing the object, wherein packing the object comprises (a)-(b);

(a) checking whether the invariant condition holds;

(b) choosing between taking the object from the mutable state to a consistent state, provided the invariant condition holds and generating an error condition if the invariant condition does not hold; and

wherein the hierarchy of objects is defined via a definition comprising a keyword specifying object ownership of one or more fields; and

wherein being designated as being of a consistent state prevents further modifications.