US 8,413,122 B2Granted

System and method for demonstrating the correctness of an execution trace in concurrent processing environments

AssigneeInternational Business Machines Corporation

InventorsKristijan Dragicevic, Luis Garces-Erice, Daniel Nikolaus Bauer

Life of this patent

Estimating the term…

Abstract

Since multi-core processors have become the standard architecture for general purpose machines, programmers are required to write software optimized for parallelism. Verification of correctness is an important issue for parallel code because of its complexity. There are still tools missing that provide verification for complex code, such as testing the execution of code provides. Consequently, described herein are systems and methods to evaluate the correctness of program traces. Furthermore, the systems and methods described herein do not demand excessive computational requirements and the size of the program trace being evaluated increases.

Claims24

Dependent claims

A method, performed by a computing device, of verifying the correctness of an execution history that includes operations executed in parallel to a concurrent priority queue having insert and remove operations, said method comprising:

defining a rule set that includes an operation rule set, that defines insert and remove operation behavior on the priority queue, a new state rule set and an obsolete state rule set;
reading the execution history from a storage device;
building a list of events to be processed that includes a start of insertion event, an end of insertion event, a start of removal event and an end of removal event for each operation included in the execution history, where each event includes a timestamp according to the respective start time and end time of each operation;
processing each event in the list of events sequentially, according to the timestamps of each respective event;
building a state set, in response to said processing, each state set having:
a definite heap collection including a data set shared by all states including the elements in the priority queue;
an “associated removal” list including a collection of pairs of insert and remove operations;
a “pending removal” list including a collection of remove operations;
a “pending insert” list including a collection of insert operations;
and a “finished insertion” list including a collection of insertion operations that have succeeded;
where a new state is added to the state set when processing an event creates a new state according to a new state rule included the new state rule set, and removing an obsolete state in the state set when processing an event removes an obsolete state according to a obsolete state rule included in the obsolete state rule set;
and
when the state set is empty, outputting a incorrect result to at least one of a storage device or a display device;
wherein,
when every event has been processed and the state set includes at least one state, outputting a correct result to at least one of a storage device or a display device.

12 more elements

A system of verifying the correctness of an execution history that includes insert and remove operations applied to a concurrent priority queue executed in parallel on a computing device, the system comprising a programmed processor unit and associated memory storage unit, said programmed processor unit configured to run a method comprising:

defining a rule set that includes an operation rule set, that defines insert and remove operation behavior on said priority queue, a new state rule set and an obsolete state rule set;
reading the execution history from a storage device;
building a list of events to be processed that includes a start of insertion event, an end of insertion event, a start of removal event and an end of removal event for each operation included in the execution history, where each event includes a timestamp according to the respective start time and end time of each operation that includes a start event and an end event for each operation included in the execution history;
processing each event in the list of events sequentially, according to the timestamps of each respective event;
building a state set, in response to said processing, each state set having:
a definite heap collection including a data set shared by all states including the elements in the priority queue;
an “associated removal” list including a collection of pairs of insert and remove operations;
a “pending removal” list including a collection of remove operations;
a “pending insert” list including a collection of insert operations;
and a “finished insertion” list including a collection of insertion operations that have succeeded;
where a new state is added to the state set when processing an event creates a new state according to a new state rule included the new state rule set, and removing an obsolete state in the state set when processing an event removes an obsolete state according to a obsolete state rule included in the obsolete state rule set;
when the state set is empty, means, implemented on a computing device, for outputting a negative result to at least one of a storage device or a display device;
when every event has been processed and the state set includes at least one state, means, implemented on a computing device, for outputting a positive result to at least one of a storage device or a display device.

10 more elements

A tangible computer-readable memory device, embodying computer-executable program code, when executed by a computing device, adapts said computing device to perform a method of verifying the correctness of an execution history that includes insert and remove operations executed in parallel applied to a concurrent priority queue, said method comprising:

defining a rule set that includes an operation rule set, that defines insert and remove operation behavior on the priority queue, a new state rule set and an obsolete state rule set;
reading the execution history from a storage device;
building a list of events to be processed that includes a start of insertion event, an end of insertion event, a start of removal event and an end of removal event for each operation included in the execution history, where each event includes a timestamp according to the respective start time and end time of each operation;
processing each event in the list of events sequentially, according to the timestamps of each respective event;
building a state set, in response to said processing, each state set having:
a definite heap collection including a data set shared by all states including the elements in the priority queue;
an “associated removal” list including a collection of pairs of insert and remove operations;
a “pending removal” list including a collection of remove operations;
a “pending insert” list including a collection of insert operations;
and a “finished insertion” list including a collection of insertion operations that have succeeded;
where a new state is added to the state set when processing an event creates a new state according to a new state rule included the new state rule set, and removing an obsolete state in the state set when processing an event removes an obsolete state according to a obsolete state rule included in the obsolete state rule set;
and
when the state set is empty, outputting a incorrect result to at least one of a storage device or a display device;
wherein,
when every event has been processed and the state set includes at least one state, outputting a correct result to at least one of a storage device or a display device.

12 more elements

Dependencies are inferred from the claim text.

patentgrep

Loading patent…

Abstract

defining a rule set that includes an operation rule set, that defines insert and remove operation behavior on the priority queue, a new state rule set and an obsolete state rule set;
reading the execution history from a storage device;
building a list of events to be processed that includes a start of insertion event, an end of insertion event, a start of removal event and an end of removal event for each operation included in the execution history, where each event includes a timestamp according to the respective start time and end time of each operation;
processing each event in the list of events sequentially, according to the timestamps of each respective event;
building a state set, in response to said processing, each state set having:
a definite heap collection including a data set shared by all states including the elements in the priority queue;
an “associated removal” list including a collection of pairs of insert and remove operations;
a “pending removal” list including a collection of remove operations;
a “pending insert” list including a collection of insert operations;
and a “finished insertion” list including a collection of insertion operations that have succeeded;
where a new state is added to the state set when processing an event creates a new state according to a new state rule included the new state rule set, and removing an obsolete state in the state set when processing an event removes an obsolete state according to a obsolete state rule included in the obsolete state rule set;
and
when the state set is empty, outputting a incorrect result to at least one of a storage device or a display device;
wherein,
when every event has been processed and the state set includes at least one state, outputting a correct result to at least one of a storage device or a display device.

12 more elements