Patent Document ID: 9792161
Application ID: 14553056
Patent Flag: 1

Claim One:
1. A system comprising: a hardware processor; a constraint solver executable by the hardware processor; non-transitory computer-readable medium storing instructions executable by the hardware processor to maximize detection of concurrency bugs in different threads of a multithreaded software program (“program”), the instructions and the program executable by the hardware processor to: formulate detection as a constraint-solving problem by: assigning an order variable to each of a plurality of events in an input trace of the program; ordering the order variables to corresponding events in an order of execution according to a maximal causal model, which captures a set of feasible traces that can be generated by a thread of a multithreaded program capable of generating the input trace and by a second input trace, wherein the input trace and the second input trace are thread-local traces; defining the maximal causal model with multiple axioms comprising prefix closedness and local determinism, wherein prefix closedness is that prefixes of a feasible trace are also feasible, and local determinism is that threads of the program behave deterministically; further defining local determinism to include: data-abstract equivalence of the input trace and the second input trace of the program, where the input trace and the second input trace are equal except for data values in read events and write events of the plurality of events; and a branch axiom, in relation to a first branch event of the plurality of events and using the data-abstract equivalence, comprising when read events in the input trace for the thread equal the read events in the second input trace for the thread, the first branch event in the second input trace is feasible; and generating a formula over the order variables and over a plurality of branch variables corresponding to branch events, including the first branch event, that captures the maximal causal model, control flow, and a trace property whose violation corresponds to a concurrency bug; and solve the formula with the constraint solver to determine whether the trace property is violated due to the concurrency bug, wherein employment of thread-local traces enables concurrency bug detection in multiple of the different threads in parallel, reducing runtime computation overhead of the hardware processor by at least ten percent.