SYSTEM AND METHOD FOR DEMONSTRATING THE CORRECTNESS OF AN EXECUTION TRACE IN CONCURRENT PROCESSING ENVIRONMENTS

• US 20100205484A1
• Filed: 02/12/2009
• Published: 08/12/2010
• Est. Priority Date: 02/12/2009
• Status: Active Grant

• Current Assignee: GlobalFoundries, Inc.
• Original Assignee: International Business Machines Corporation
• Inventors: Bauer, Daniel Nikolaus, Dragicevic, Kristijan, Garces-Erice, Luis
• Granted Patent: US 8,413,122 B2
• Time in Patent Office: Days
• US Class Current: 714/37
• CPC Class Codes: G06F 11/3636 by tracing the execution of the program

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.

Claims

1. A method, performed by a computing device, of verifying the correctness of an execution history that includes operations executed in parallel to a data structure, said method comprising:

defining a rule set that includes an operation rule set, that defines operation behavior on the data structure, a new state rule set and an obsolete state rule set;

reading the execution history from a storage device;

building an event set that includes a start event and an end 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 event set sequentially, according to the timestamps of each respective event;

building a state set, in response to said processing, 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.

2. The method according to claim 1, wherein the data structure is a concurrent priority queue and the rule set includes an insert operation and a remove operation.

3. The method according to claim 2, further comprising defining a definite heap that includes a data set, where the concurrent priority queue includes the data set across every state in the state set.

4. The method according to claim 2, wherein an obsolete state rule is defined in the obsolete state rule set that removes a state upon processing an end event and the state describes the end event as pending

5. The method according to claim 2, wherein a new state is defined in the new state rule set that creates a new state when a value is added to the concurrent priority queue, according to the insert operation, which has a lower value that a highest priority value in the concurrent priority queue.

6. The method according to claim 1, wherein processing the events further includes adding an event to each state when processing a new event.

7. The method according to claim 6, further comprising determining for each state in the state set whether the operation corresponding to the event has completed upon processing a start event.

8. The method according to claim 7, further comprising applying pending operations in each state to make each operation complete when at least one state in the state set has a pending operation.

9. A system of verifying the correctness of an execution history that includes operations to a data structure executed in parallel on a computing device, comprising:

means, implemented on a computing device, for defining a rule set that includes an operation rule set, that defines operation behavior on the data structure, a new state rule set and an obsolete state rule set;

means implemented on a computing device, for reading the execution history from a storage device;

means, implemented on a computing device, for building an event set that includes a start event and an end 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;

means, implemented on a computing device, for processing each event in the event set sequentially, according to the timestamps of each respective event,

means, implemented on a computing device, for building a state set, in response to said processing, 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. The system according to claim 9, wherein the data structure is a concurrent priority queue and the rule set includes an insert operation and a remove operation.

11. The system according to claim 10, further comprising means, implemented on a computing device, for defining a definite heap that includes a data set, where the concurrent priority queue includes the data set across every state in the state set.

12. The system according to claim 10, wherein an obsolete state rule is defined in the obsolete state rule set that removes a state upon processing an end event and the state describes the end event as pending.

13. The system according to claim 10, wherein a new state is defined in the new state rule set that creates a new state when a value is added to the concurrent priority queue, according to the insert operation, which has a lower value that a highest priority value in the concurrent priority queue.

14. The system according to claim 9, wherein processing the events further includes adding an event to each state when processing a new event.

15. The system according to claim 14, further comprising means, implemented on a computing device, for determining for each state in the state set whether the operation corresponding to the event has completed upon processing a start event.

16. The system according to claim 15, further comprising means, implemented on a computing device, for applying pending operations in each state to make each operation complete when at least one state in the state set has a pending operation.

17. A computer-readable medium, 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 operations executed in parallel to a data structure, said method comprising:

defining a rule set that includes an operation rule set, that defines operation behavior on the data structure, a new state rule set and an obsolete state rule set;

reading the execution history from a storage device;

building an event set that includes a start event and an end 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 event set sequentially, according to the timestamps of each respective event;

building a state set, in response to said processing, 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.

18. The computer-readable medium according to claim 17, wherein the data structure is a concurrent priority queue and the rule set includes an insert operation and a remove operation.

19. The computer-readable medium according to claim 18, further comprising defining a definite heap that includes a data set, where the concurrent priority queue includes the data set across every state in the state set.

20. The computer-readable medium according to claim 18, wherein an obsolete state rule is defined in the obsolete state rule set that removes a state upon processing an end event and the state describes the end event as pending.

21. The computer-readable medium according to claim 18, wherein a new state is defined in the new state rule set that creates a new state when a value is added to the concurrent priority queue, according to the insert operation, which has a lower value that a highest priority value in the concurrent priority queue.

22. The computer-readable medium according to claim 17, wherein processing the events further includes adding an event to each state when processing a new event.

23. The computer-readable medium according to claim 22, further comprising determining for each state in the state set whether the operation corresponding to the event has completed upon processing a start event.

24. The computer-readable medium according to claim 23, further comprising applying pending operations in each state to make each operation complete when at least one state in the state set has a pending operation.