Model checker for finding distributed concurrency bugs

Patent metadata

Field	Value
Publication number	US-10599552-B2
Application number	US-201815962873-A
Country	US
Kind code	B2
Filing date	Apr 25, 2018
Priority date	Apr 25, 2018
Publication date	Mar 24, 2020
Grant date	Mar 24, 2020

Abstract

Described herein are systems and methods for distributed concurrency (DC) bug detection. The method includes identifying a plurality of nodes in a distributed computing cluster; identifying a plurality of messages to be transmitted during execution of an application by the distributed computing cluster; determining a set of orderings of the plurality of messages for DC bug detection, the set of orderings determined based upon the plurality of nodes and the plurality of messages; removing a subset of the orderings from the set of orderings based upon one or more of a state symmetry algorithm, a disjoint-update independence algorithm, or a zero-crash-impact reordering algorithm; and performing DC bug detection testing using the set of orderings after the subset of the orderings is removed from the set of orderings.

First claim

What is claimed is:

1. A method for distributed concurrency (DC) bug detection, the method comprising:
identifying, by a computing device, a plurality of nodes in a distributed computing cluster;
identifying, by the computing device, a plurality of messages to be transmitted during execution of an application by the distributed computing cluster;
determining, by the computing device, a set of orderings of the plurality of messages for DC bug detection, the set of orderings determined based upon the plurality of nodes and the plurality of messages;
removing, by the computing device, a subset of the orderings, where each ordering comprises a unique sequence of message arrival at one or more of the nodes, from the set of orderings based upon one or more of a state symmetry algorithm, a disjoint-update independence algorithm, and a zero-crash-impact reordering algorithm, where the zero-crash-impact reordering algorithm is a crash-after-discard reduction or a consecutive-crash reduction, and where the consecutive-crash reduction comprises determining a first message of a first ordering causes a crash of a node, determining a second message of the first ordering causes another crash of the node, and adding a second ordering comprising the first message and the second message to the subset of the orderings; and
performing, by the computing device, DC bug detection testing using the set of orderings after the subset of the orderings is removed from the set of orderings.

2. The method of claim 1 , wherein removing the subset of the orders from the set of orderings based upon the state symmetry algorithm comprises:
comparing a first state transition of a first node of a first ordering of the set of orderings with a second state transition of a second node of a second ordering of the set of orderings; and
adding the second ordering to the subset of the orderings when the first state transition and the second state transition are symmetrical.

3. The method of claim 1 , wherein removing the subset of the orders from the set of orderings based upon the disjoint-update independence algorithm comprises:
comparing a first variable in a first message of a first ordering of the set of orderings with a second variable in a second message of the first ordering of the set of orderings; and
adding a second ordering to the subset of the orderings when the first variable and the second variable are different and the second ordering comprises the first message and the second message.

4. The method of claim 1 , further comprising:
determining, prior to performing the DC bug detection, one or more parallel flip orderings, each of the parallel flip orderings comprising a first plurality of messages for a first node and a second plurality of messages for a second node, wherein the first plurality of messages are independent of the second plurality of messages, and wherein the first plurality of messages and the second plurality of messages are reordered in each of the parallel flip orderings; and
prioritizing the parallel flip orderings when performing the DC bug detection.

5. The method of claim 1 , wherein removing the subset of the orders from the set of orderings based upon crash-after-discard reduction comprises:
determining a first message of a first ordering will be discarded by a node;
determining a second message of the first ordering causes a crash of the node; and
adding a second ordering comprising the first message and the second message to the subset of the orderings.

6. The method of claim 1 , wherein the set of orderings comprises unique orderings for each permutation of the plurality of messages received at each of the plurality of nodes.

7. The method of claim 1 , further comprising determining the subset of the orderings based upon each of the state symmetry algorithm, the disjoint-update independence algorithm, the zero-crash-impact reordering algorithm, and a parallel flips algorithm.

8. A device comprising:
a memory storage comprising instructions; and
a processor in communication with the memory, wherein the processor executes the instructions to:
identify a plurality of nodes in a distributed computing cluster;
identify a plurality of messages to be transmitted during execution of an application by the distributed computing cluster;
determine a set of orderings of the plurality of messages for distributed concurrency (DC) bug detection, the set of orderings determined based upon the plurality of nodes and the plurality of messages;
remove a subset of the orderings, where each ordering comprises a unique sequence of message arrival at one or more of the nodes, from the set of orderings based upon one or more of a state symmetry algorithm, a disjoint-update independence algorithm, and a zero-crash-impact reordering algorithm, where the zero-crash-impact reordering algorithm is a crash-after-discard reduction or a consecutive-crash reduction, and where the consecutive-crash reduction comprises determining a first message of a first ordering causes a crash of a node, determining a second message of the first ordering causes another crash of the node, and adding a second ordering comprising the first message and the second message to the subset of the orderings; and
perform DC bug detection testing using the set of orderings after the subset of the orderings is removed from the set of orderings.

9. The device of claim 8 , wherein the instructions to remove the subset of the orders from the set of orderings based upon the state symmetry algorithm comprise instructions to:
compare a first state transition of a first node of a first ordering of the set of orderings with a second state transition of a second node of a second ordering of the set of orderings; and
add the second ordering to the subset of the orderings when the first state transition and the second state transition are symmetrical.

10. The device of claim 8 , wherein the instructions to remove the subset of the orders from the set of orderings based upon the disjoint-update independence algorithm comprise instructions to:
compare a first variable in a first message of a first ordering of the set of orderings with a second variable in a second message of the first ordering of the set of orderings; and
add a second ordering to the subset of the orderings when the first variable and the second variable are different and the second ordering comprises the first message and the second message.

11. The device of claim 8 , wherein the processor further executes the instructions to:
determine, prior to performing the DC bug detection, one or more parallel flip orderings, each of the parallel flip orderings comprising a first plurality of messages for a first node and a second plurality of messages for a second node, wherein the first plurality of messages are independent of the second plurality of messages, and wherein the first plurality of messages and the second plurality of messages are reordered in each of the parallel flip orderings; and
prioritize the parallel flip orderings when performing the Dc bug detection.

12. The device of claim 8 , wherein instructions to remove the subset of the orders from the set of orderings based upon the crash-after-discard reduction comprise instructions to:
determine a first message of a first ordering will be discarded by a node;
determine a second message of the first ordering causes a crash of the node; and
add a second ordering comprising the first message and the second message to the subset of the orderings.

13. The device of claim 8 , wherein the set of orderings comprises unique orderings for each permutation of the plurality of me

Assignees

• Futurewei Technologies Inc
• Univ Chicago

Inventors

• Lukman Jeffrey
• Ke Huan
• Gunawi Haryadi
• Ye Feng
• Tian Chen
• Chen Shen Chi

Classifications

• G06F11/3692

  for test results analysis · CPC title

• G06F11/3672

  Test management · CPC title

• G06F11/3632 Primary

  of specific synchronisation aspects · CPC title

• G06F11/3688

  for test execution, e.g. scheduling of test suites · CPC title

• G06F11/3698 Primary

  Environments for analysis, debugging or testing of software · CPC title