Method for specifying and verifying multi-threaded object-oriented programs with invariants
First Claim
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 Assignments
0 Petitions
Accused Products
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.
-
Citations
20 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. - View Dependent Claims (2, 3, 4, 5, 6, 7, 8, 9, 10, 11)
-
-
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.
- View Dependent Claims (13, 14, 15, 16)
-
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. - View Dependent Claims (18, 19, 20)
-
Specification