Methods and systems for testing parallel queues

• US 6,510,531 B1
• Filed: 09/23/1999
• Issued: 01/21/2003
• Est. Priority Date: 09/23/1999
• Status: Expired due to Term

• Current Assignee: Wi-LAN Inc.
• Original Assignee: Lucent Technologies, Inc. (Nokia Corporation)
• Inventors: Gibbons, Phillip B.
• Primary Examiner(s): BADERMAN, SCOTT T
• Application Number:
  US09/401,897
• Time in Patent Office: 1,216 Days
• Field of Search: 714/37, 714/38, 714/39, 714/42, 707/3, 707/4, 707/5, 707/7
• US Class Current: 714/37
• CPC Class Codes: G06F 11/3672 Test management
• CPC Class Codes: Y10S 707/99937 Sorting

Abstract

There is provided methods and systems for testing linearizable, linearizable priority, and non-linearizable queues. According to one embodiment of the invention, there is provided a method for verifying correct function of a linearizable queue with respect to a program executed by a plurality of processors in a computer processing system. A distinct-values trace is given that includes operations on the queue and an identifier associated with each of the operations. Each operation is associated with two timestamps respectively corresponding to a start time and an end time of the operation. The method includes the step of matching the operations to generate corresponding operation pairs, based on the identifiers. The function of the queue is identified as correct, when, for any operation pair comprising an enqueue operation e and a corresponding dequeue operation e′, there does not exist another operation pair comprising an enqueue operation d and a corresponding dequeue operation d′ such that an end time of the enqueue operation e precedes a start time of the enqueue operation d and an end of the dequeue operation d′ precedes a start of the dequeue operation e′.

Claims

1. In a computer processing system comprising a linearizable queue and a plurality of processors, a method for verifying correct function of the queue with respect to a program executed by the processors, given a trace comprising events on the queue and an identifier associated with each of the events, wherein each event is associated with two timestamps respectively corresponding to a start time and an end time of the event, the method comprising the steps of:

matching the events to generate corresponding event pairs, based on the identifiers; and

identifying the function of the queue as correct, when, for any event pair comprising an enqueue event e and a corresponding dequeue event e′

, there does not exist another event pair comprising an enqueue event d and a corresponding dequeue event d′

such that an end time of the enqueue event e precedes a start time of the enqueue event d and an end of the dequeue event d′

precedes a start time of the dequeue event e′

.

2. The method according to claim 1, further comprising the step of identifying the other event pair comprising the enqueue event d and the corresponding dequeue event d′

as an offending event pair, when the function of the queue is not identified as correct.

3. The method according to claim 1, wherein the trace is a partial trace comprising some, but not all, of the events on the queue with respect to the program executed by the processors, and said method is performed with respect to only the events comprised in the partial trace.

4. The method according to claim 1, wherein the trace is one of a distinct-values trace and a non-distinct-values trace.

5. The method according to claim 1, wherein said method is performed substantially in parallel by the plurality of processors comprised in the computer processing system, an other plurality of processors comprised in an other computer processing system, or a combination thereof.

6. In a computer processing system comprising a linearizable queue and a plurality of processors, a method for verifying correct function of the queue with respect to a program executed by the processors, given a trace comprising events on the queue and an identifier associated with each of the events, wherein each event is associated with two timestamps respectively corresponding to a start time and an end time of the event, the method comprising the steps of:

matching the events to generate corresponding event pairs, based on the identifiers; and

for all event pairs comprising an enqueue event e and a corresponding dequeue event e′

, identifying other event pairs comprising an enqueue event d and a corresponding dequeue event d′

such that an end of the dequeue event d′

precedes a start time of the dequeue event e′

;

determining a maximum start time of the enqueue event d from among all the identified, other event pairs; and

identifying the function of the queue as correct, when the end time of the enqueue event e is not less than the maximum start time.

7. The method according to claim 6, further comprising the step of identifying the other event pair comprising the enqueue event d and the corresponding dequeue event d′

as an offending event pair, when the function of the queue is not identified as correct.

8. The method according to claim 6, wherein the trace is a partial trace comprising some, but not all, of the events on the queue with respect to the program executed by the processors, and said method is performed with respect to only the events comprised in the partial trace.

9. The method according to claim 6, wherein the trace is one of a distinct-values trace and a non-distinct-values trace.

10. In a computer processing system comprising a linearizable queue and a plurality of processors, a method for verifying correct function of the queue with respect to a program executed by the processors, given a trace comprising events on the queue and an identifier associated with each of the events, wherein each event is associated with two timestamps respectively corresponding to a start time and an end time of the event, the method comprising the steps of:

sorting the timestamps in one of ascending and descending order and placing the timestamps in an array A;

matching the events to generate corresponding event pairs, based on the identifiers;

populating each element of an array B, such that B[i], the ith element of array B, is equal to a start time of an enqueue event of a given event pair when A[i], the ith element of array A, is equal to an end time of a dequeue event of the given event pair, and such that B[i] is equal to zero when A[i] is not equal to the end time of the dequeue event of the given event pair;

populating each element of an array C such that C[i], the ith element of array C, is equal to a maximum value corresponding to all values in the array B from one to i when said sorting is ascending, and from i to an end value in the array B when said sorting is descending; and

identifying the function of the queue as correct, when there does not exist i such that A[i] is equal to a start time of a dequeue event of a respective event pair and an end time of an enqueue event of the respective event pair is less than C[i].

11. The method according to claim 10, further comprising the step of, upon performing said matching step, identifying the function of the queue as incorrect when there exists one of an unpaired event and an event pair such that a dequeue event of the pair ends before an enqueue event of the pair begins.

12. The method according to claim 10, further comprising the step of identifying the function of the queue as incorrect, when there exists i such that A[i] is equal to a start time of the dequeue event of the respective event pair and the end time of the enqueue event of the respective event pair is less than C[i].

13. The method according to claim 11, further comprising the step of identifying the unpaired event, when there exists the unpaired event.

14. The method according to claim 11, further comprising the step of identifying the event pair, when the event pair exists such that the dequeue event of the pair ends before the enqueue event of the pair begins.

15. The method according to claim 10, wherein the trace is a partial trace comprising some, but not all, of the events on the queue with respect to the program executed by the processors, and said method is performed with respect to only the events comprised in the partial trace.

16. The method according to claim 10, wherein the trace is one of a distinct-values trace and a non-distinct-values trace.

17. In a computer processing system comprising a linearizable priority queue and a plurality of processors, wherein the queue supports insert and one of deletemax and deletemin events, a method for verifying correct function of the queue with respect to a program executed by the processors, given a trace comprising the events on the queue and an identifier associated with each of the events, wherein each event is associated with two timestamps respectively corresponding to a start time and an end time of the event, the method comprising the steps of:

matching the events to generate corresponding event pairs, based on the identifiers; and

identifying the function of the queue as correct, if, for all corresponding event pairs comprising an enqueue event f and a corresponding dequeue event f, there exists a time t between the start time and end time of the dequeue event f such that, for each event pair comprising an enqueue event e and a corresponding dequeue event e′

, an end time of the enqueue event e is one of less than and equal to the time t and less than the start time of the dequeue event e′

, and a value corresponding to the enqueue event f is one of greater than, when the queue supports deletemax events, and less than, when the queue supports deletemin events, a value corresponding to an enqueue event e.

18. The method according to claim 17, wherein the trace is a partial trace comprising some, but not all, of the events on the queue with respect to the program executed by the processors, and said method is performed with respect to only the events comprised in the partial trace.

19. The method according to claim 17, wherein the trace is one of a distinct-values trace and a non-distinct-values trace.

20. The method according to claim 17, wherein said identifying step comprises the steps of:

computing a minmax skyline with respect to the timestamps of the events; and

for all event pairs, determining whether the time t exists such that the value corresponding to the enqueue event f is greater than the skyline corresponding to the time t.

21. The method according to claim 17, further comprising the step of, upon performing said matching step, identifying the function of the queue as incorrect when there exists one of an unpaired event and an event pair such that a dequeue event of the pair ends before an enqueue event of the pair begins.

22. The method according to claim 21, further comprising the step of identifying the unpaired event as offending when the unpaired event exists.

23. The method according to claim 21, further comprising the step of identifying as offending the event pair comprising the dequeue event that ends before the enqueue event of the pair begins, when the event pair exists.

24. The method according to claim 17, further comprising the step of identifying the function of the queue as incorrect, if, for all corresponding event pairs comprising an enqueue event f and a corresponding dequeue event f′

, there does not exist a time t between the start time and end time of the dequeue event f′

such that, for each event pair comprising the enqueue event e and a corresponding dequeue event e′

, an end time of the enqueue event e is one of less than and equal to the time t and less than the start time of the dequeue event e′

, and a value corresponding to the enqueue event f is one of greater than, when the queue supports deletemax events, and less than, when the queue supports deletemin events, a value corresponding to an enqueue event e.

25. The method according to claim 24, further comprising the step of identifying as offending the event pair comprising the enqueue event f and the dequeue event f′

, when the function of the queue is identified as incorrect.

26. In a computer processing system comprising a linearizable priority queue and a plurality of processors, wherein the queue supports insert and one of deletemax and deletemin events, a method for verifying correct function of the queue with respect to a program executed by the processors, given a trace comprising the events on the queue and an identifier associated with each of the events, wherein each event is associated with two timestamps respectively corresponding to a start time and an end time of the event, the method comprising the steps of:

sorting the timestamps in one of ascending and descending order and placing the timestamps in an array A;

matching the events to generate corresponding event pairs, based on the identifiers;

for all I in the array A where A[i] is the ith element in the array, in ascending order when said sorting is ascending, in descending order when said sorting is descending, starting with a set being initially empty, inserting a value associated with a given event pair into the set when A[i] is equal to an end time of an enqueue event of the given event pair that precedes a start time of a dequeue event of the given event pair, and deleting the value associated with the given event pair from the set when A[i] is equal to the start time of the dequeue of the given event pair that succeeds the end time of the enqueue event of the given event pair;

for each i in an array B where B[i] is the ith element in array B, populating each element B[i] with one of, a maximum value when the queue supports deletemax operations, and a minimum value when the queue supports deletemin operations, in the set upon processing A[i]; and

identifying the function of the queue as correct, when there does not exist a respective event pair such that one of, a minimum value when the queue supports deletemax events, and a maximum value when the queue supports deletemin events, in the array B in an entire range max(a start time of an enqueue event of the respective event pair, a start time of a dequeue event of the respective event pair) to an end time of the dequeue event of the respective event pair is one of, greater than when the queue supports deletemax event, and less than when the queue supports deletemin events, the value associated with the given event pair.

27. The method according to claim 26, further comprising the step of, upon performing said matching step, identifying the function of the queue as incorrect when there exists one of an unpaired event and an event pair such that a dequeue event of the pair ends before an enqueue event of the pair begins.

28. The method according to claim 26, further comprising the step of preprocessing the array B for range minima queries, before performing said identifying step.

29. The method according to claim 26, further comprising the step of identifying the function of the queue as incorrect, when there exists the respective event pair such that the minimum value in the array B in the entire range max(the start time of the enqueue event of the respective event pair, the start time of the dequeue event of the respective event pair) to the end time of the dequeue event of the respective event pair is greater than the value associated with the given event pair.

30. The method according to claim 29, further comprising the step of identifying the respective event pair as offending when the function of the queue is identified as incorrect.

31. The method according to claim 26, wherein the trace is a partial trace comprising some, but not all, of the events on the queue with respect to the program executed by the processors, and said method is performed with respect to only the events comprised in the partial trace.

32. The method according to claim 26, wherein the trace is one of a distinct-values trace and a non-distinct-values trace.

33. In a computer processing system comprising a non-linearizable queue and a plurality of processors, a method for verifying correct function of the queue with respect to a program executed by the processors, given a trace comprising events on the queue, a chain of events for each processor, and an identifier associated with each of the events, the method comprising the steps of:

matching the events to generate corresponding event pairs, based on the identifiers;

constructing a graph G having nodes corresponding to the events, and directed edges from a node α

to a node β

when one of the node α

is an immediate predecessor of the node β

with respect to a given chain, and the nodes α and

β

correspond to enqueue events on different chains and the node α

must precede the node β

in a queue sort; and

for each node remaining in the graph G, given an empty queue Q, an empty topological sort σ

, and a set S of eligible enqueue events, wherein an event e is eligible to be added to the sort when all parents of the event e are in the sort, one of;

selecting and removing an enqueue event a from the set S and a node corresponding to the event a from the graph G, adding an event a to the sort, and enqueuing a value corresponding to the event a to the queue Q, and

removing a node corresponding to a dequeue event h′

from the graph G, adding the dequeue event h′

to the sort, and dequeuing a value corresponding to an enqueue event h from the queue Q, when the enqueue event h and the dequeue event h′

are comprised in an event pair and a value corresponding to the event h is at a head of the queue;

for each node b which is a child of the removed node such that the node b is an enqueue event, adding an event corresponding to the node b to the set S, when the node b is eligible; and

returning the sort.

34. The method according to claim 33, further comprising the step of, upon performing said matching step, identifying the function of the queue as incorrect, when there exists an unpaired event.

35. The method according to claim 34, further comprising the step of identifying the unpaired event as offending when the unpaired event exists.

36. The method according to claim 33, further comprising the step of identifying the function of the queue as incorrect, when the set S is empty, there exists the enqueue event h such that the value corresponding to the event h is at the head of the queue Q, the enqueue event h and the dequeue event h′

are comprised in an event pair, and the dequeue event h′

is not eligible.

37. The method according to claim 33, further comprising the step of identifying the function of the queue as incorrect, when the set S and the queue Q are empty.

38. The method according to claim 33, wherein the trace is a partial trace comprising some, but not all, of the events on the queue with respect to the program executed by the processors, and said method is performed with respect to only the events comprised in the partial trace.

39. The method according to claim 33, wherein the trace is one of a distinct-values trace and a non-distinct-values trace.

40. The method according to claim 33, further comprising the step of, upon constructing the graph G, for a given node w on a first chain having edges to a plurality of nodes on a second chain, removing at least some of the edges other than an edge corresponding to a first node of the plurality of nodes.