Lifting of bounded liveness counterexamples to concrete liveness counterexamples

Patent metadata

Field	Value
Publication number	US-9678853-B2
Application number	US-201514862784-A
Country	US
Kind code	B2
Filing date	Sep 23, 2015
Priority date	Jul 7, 2015
Publication date	Jun 13, 2017
Grant date	Jun 13, 2017

Abstract

A trace of a bounded liveness failure of a system component is received, by one or more processors, along with fairness constraints and liveness assertion conditions. One or more processors generate randomized values for unassigned input values and register values, of the trace, and simulate traversal of each of a sequence of states of the trace. One or more processors determine whether traversing the sequence of states of the trace results in a repetition of a state, and responsive to determining that traversing the sequence of states of the trace does result in a repetition of a state, and the set of fairness constraints are asserted within the repetition of a state, and that the continuous liveness assertion conditions are maintained throughout the repetition of the state, a concrete counterexample of a liveness property of the system component is reported.

First claim

What is claimed is:

1. A method for mapping a bounded liveness failure to a concrete counterexample of a liveness property of a system component, the method comprising:
receiving, by one or more processors, a trace of a bounded liveness failure of a system component, a set of fairness constraints and continuous liveness assertion conditions corresponding to the trace;
generating, by one or more processors, randomized values for one or more unassigned input values of one or more registers of the trace and for unassigned register values of the one or more registers of the trace;
simulating, by one or more processors, traversal of each state of a sequence of states of the trace;
determining, by one or more processors, whether a repetition of a state of the sequence of states of the trace is produced by traversing the sequence of states of the trace; and
responsive to determining that traversing the sequence of states of the trace does result in a repetition of a state of the sequence of states of the trace, and determining that the set of fairness constraints are asserted within the sequence of states leading to the repetition of a state of the sequence of states, and that the continuous liveness assertion conditions are maintained throughout the sequence of states leading to the repetition of the state of the sequence of states, reporting, by one or more processors, a concrete counterexample of a liveness property of the system component.

2. The method of claim 1 , wherein responsive to determining that traversing the sequence of states of the trace does not result in a repetition of a state of the sequence of states of the trace, the method further comprising:
performing a trace minimization, by one or more processors, wherein one or more unassigned input values of the one or more registers of the trace that are independent of determining a bounded liveness failure are removed;
analyzing incrementally, by one or more processors, the one or more registers of the trace of the bounded liveness failure, to match a register to a time interval having a start time corresponding to a first state and an end time corresponding to a second state, within a bounded timeframe of the trace; and
responsive to the fairness constraints being made and the continuous liveness assertion conditions being maintained throughout a loop of a sequence of states that includes a repetition of a state of the sequence of states of the trace, determining, by one or more processors, a concrete counterexample of a liveness property of the system component.

3. The method of claim 2 , wherein analyzing incrementally, the one or more registers of the trace of the bounded liveness failure, includes checking simultaneously for an equality of the one or more registers at the start time and the end time of the time interval.

4. The method of claim 2 , wherein one or more registers are matched between a start time and an end time of a time interval within the bounded timeframe of the trace, based on a priority of concreteness of the states, in which a priority of the concreteness is determined by the values of the one or more registers, and on which high priority unmatched registers of a state are matched incrementally.

5. The method of claim 1 , further comprising:
one or more processors performing a trace minimization, wherein at least one input value that is assigned of the one or more registers for a state of the sequence of states, which are independent of the bounded liveness failure, is removed;
one or more processors sorting the sequence of states based on a concreteness of register values of each state, wherein the concreteness of register values is determined by a quantity of Boolean values;
one or more processors determining candidate time steps as a start timeframe and an end timeframe of a state of the trace minimization, exhibiting compatible values of the one or more registers of the state for each increment of candidate time steps;
one or more processors performing an unbounded safety query check, in which a reachability of a prefix state of the sequence of states of the trace minimization, responsive to a determination of a state repetition loop, while fairness assertions and liveness assertion conditions are met;
responsive to the determination of a failed unbounded safety query check, one or more processors determining whether prefix states of the trace can be reached from a state indicating a repetition; and
responsive to the determination that the prefix states of the trace can be reached from the state indicating a repetition, one or more processors reporting a concrete counterexample of a liveness property.

6. The method of claim 1 , further comprising:
one or more processors performing a trace minimization, wherein an input value of the one or more registers that are independent of the bounded liveness failure is removed, resulting in a minimized trace;
one or more processors performing an extraction of input constraints with respect to each time step of a bounded timeframe of the minimized trace;
one or more processors performing a binary decision diagram-based liveness verification within a bounded timeframe of the minimized trace, by completing a loop of states of the sequence of states of the minimized trace which includes a repeated state, wherein reachable states from the repeated state are analyzed for fairness constraints and continuous liveness assertion conditions throughout the loop of states, beginning at a starting state of the loop of states, and the reachable states are based on suffix information resulting from the input constraints that are extracted from the repeated state; and
responsive to determining a reachable state space is constrained at every time step of the bounded timeframe of the minimized trace, by the input constraints, one or more processors reporting a concrete counterexample of a liveness property.

7. The method of claim 1 , wherein determining whether a repetition of a state of the sequence of states of the trace is produced by traversing the sequence of states of the trace, further comprises:
generating, by one or more processors, while traversing the sequence of states of the trace, a hash of each state of the sequence of states of the trace, wherein the hash of each state is stored in a hash table as each state of the sequence of states is simulated;
comparing the hash of a current state of the sequence of states of the trace to each hash stored in the has table; and
in response to determining a match of the hash of the current state of the sequence of states of the trace to a hash stored in the hash table, identifying a repeated state of the sequence of states of the trace.

8. The method of claim 1 , wherein a bounded timeframe of the trace is predetermined in which a failure of a bounded safety property check of the trace is produced, and includes a sequence of states of the trace in which a state comprises a set of values applied to all of one or more registers of the trace and inputs to the one or more registers of the trace, and each state of the sequence of states corresponds to a time interval within the bounded timeframe.

9. The method of claim 1 , wherein a hash table in which is stored a hash corresponding to the values of the registers and inputs of a state, for each state of the trace that is traversed, is cleared in response to an absence of the liveness assertion conditions continuously being applied during traversing of the sequence of states of the trace.

Assignees

• IBM

Inventors

• Baumgartner Jason R
• Gajavelly Raj Kumar
• Ivrii Alexander
• Nalla Pradeep Kumar

Classifications

• G06F11/3604

  Analysis of software for verifying properties of programs (testing of software G06F11/3668) · CPC title

• G06F11/3003

  Monitoring arrangements specially adapted to the computing system or computing system component being monitored · CPC title

• G06F11/3495 Primary

  for systems · CPC title

• G06F11/3461

  Trace driven simulation · CPC title

• G06F11/3668

  Testing of software · CPC title