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

• US 20060155905A1
• Filed: 01/11/2005
• Published: 07/13/2006
• Est. Priority Date: 01/11/2005
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Schulte, Wolfram, Leino, K. Rustan M., Jacobs, Bart
• Granted Patent: US 7,774,787 B2
• Time in Patent Office: Days
• US Class Current: 710/243
• 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 of ensuring that invariants are preserved within a data structure, the method comprising:

executing multiple threads on a computer;

a thread T1 acquiring a lock on a top hierarchical object;

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

wherein ownership confers upon thread T1 the right to modify any field of the owned object; and

wherein the lock excludes all other threads from accessing the top object and any descendant objects.

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

3. The method of claim 1, further comprising an invariant, where the invariant comprises legal values for at least two fields in two different objects.

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

5. 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;

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

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

8. 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, 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 T1 is updated with a representation of the object O1 with the owner field of O1 being updated.

9. The method of claim 1, wherein the program is verified using one of static verification, model checking, or run-time checking.

10. 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 an invariant of the object is established.

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

12. A method of ensuing that there are minimal dataraces between first and second memory accesses within a multi-threaded program, comprising:

ensuring that first and second memory access requests are owned by a single thread prior to performing said memory access requests, wherein owning comprises the thread owning a common ancestor of objects requesting the memory accesses.

13. The method of claim 12, wherein at least one of the first and second memory access locations is declared within a precondition in a routine in the computer program.

14. The method of claim 12, wherein the first and second memory access locations are declared as modified variables in a routine in the computer program.

15. The method of claim 12, wherein at least one of the first and second memory access locations is declared within a postcondition in a routine in the computer program.

16. A computer-readable medium storing computer-executable instructions for causing a computer system to perform the method of claim 12.

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

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 the entity that owns the 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 the thread owns the object and the object owner field indicates that the object is owned by the thread; and

a writer module;

which writes a value into the object variable field if the object is owned by the thread requesting write access.

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

19. The computer system of claim 17, further comprising an object invariant condition which states legal values for the at least one variable field of at least one object;

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