Model checking of multi threaded software
AssigneeNEC Laboratories America, Inc.
InventorsVineet Kahlon, Aarti Gupta
Life of this patent
Estimating the term…
Abstract
A technique for model checking of multi-threaded software is herein disclosed which advantageously can be used to verify correctness properties expressed using temporal logic, e.g., linear time temporal logic and branching time temporal logic. The model checking problem of a concurrent system is decomposed into a plurality of model checking problems on individual threads of the multi-threaded software.
Claims17
A method for model checking of a concurrent multi-threaded software program for a correctness property, said method comprising computer implemented steps of:
- modeling the multi-threaded software program as a concurrent system of pushdown systems communicating using nested locks, each thread modeled as a pushdown system;
- analyzing each individual thread of the program such that each lock is associated, between the lock's acquisition and release, with a separate set of backward and forward lock acquisition histories, where a backward lock acquisition history for a given lock is the set of only the locks that have been released before the given lock is released, and a forward lock acquisition history for the given lock is the set of only the locks that have been acquired after the given lock is acquired;
- and
- merging analysis results by checking compatibility of lock acquisition histories from a plurality of said individual threads to determine whether the program satisfies the correctness property, expressed as a temporal logic formula.
A method for model checking of a concurrent multi-threaded software program for a correctness property, said method comprising computer implemented steps of:
- modeling the multi-threaded software program as a concurrent system of pushdown systems communicating using nested locks, each thread modeled as a pushdown system;
- constructing an automaton for the correctness property;
- constructing a product automaton for the automaton and for the concurrent system of pushdown systems;
- and
- determining whether there is an acceptance path in the product automaton for the correctness property by:
- analyzing each individual thread of the program such that each lock is associated, between the lock's acquisition and release, with a separate set of backward and forward lock acquisition histories, where a backward lock acquisition history for a given lock is the set of only the locks that have been released before the given lock is released, and a forward lock acquisition history for the given lock is the set of only the locks that have been acquired after the given lock is acquired;
- and
- merging analysis results by checking compatibility of lock acquisition histories from the plurality of individual threads to determine whether the program satisfies the correctness property, expressed as a temporal logic formula.
A method for model checking of a concurrent multi-threaded software program for a correctness property, said method comprising computer implemented steps of:
- constructing an automaton from a model of the multi-threaded soft-ware program and the correctness property;
- decomposing a search for an acceptance path in the automaton into multiple instances of reachability problems across individual threads in the model of the multi-threaded software program;
- wherein each thread is modeled as a pushdown system;
- analyzing each individual thread of the program such that each lock is associated, between the lock's acquisition and release, with a separate set of backward and forward lock acquisition histories, where a backward lock acquisition history for a given lock is the set of only the locks that have been released before the given lock is released, and a forward lock acquisition history for the given lock is the set of only the locks that have been acquired after the given lock is acquired;
- and
- merging analysis results by checking compatibility of lock acquisition histories from a plurality of said individual threads to determine whether the program satisfies the correctness property, expressed as a temporal logic formula.
Dependencies are inferred from the claim text.