Inter-procedural dataflow analysis of parameterized concurrent software
View Patent ↗A system and method for computing dataflow in concurrent programs of a computer system, includes, given a family of threads (U 1 , . . . , U m ) and a Linear Temporal Logic (LTL) property, f, for a concurrent program, computing a cutoff for the LTL property, f, where c is called the cutoff if for all n greater than or equal to c, U n satisfies f if U c satisfies f. The cutoff is computed using weighted multi-automata for internal transitions of the threads. Model checking a cutoff number of processes is performed to verify race freedom in the concurrent program.
1. A method implemented by a computer for computing dataflow in concurrent programs of a computer system, comprising:
given a family of threads (U 1 , . . . , U m ) and a Linear Temporal Logic (LTL) property, f, for a concurrent program, computing a cutoff for the LTL property, f, where c is called the cutoff if for all n greater than or equal to c, U n satisfies f if U c satisfies f, the cutoff being computed using weighted multi-automata for internal transitions of the threads; and
model checking a cutoff number of processes to verify data race freedom in the concurrent program.
2. The method as recited in claim 1 , wherein the step of model checking includes establishing data race freedom in a concurrent program with at least two distinct drivers, each running respective threads, by establishing data race freedom in a parameterized system comprised of a plurality of copies of the respective threads.
3. The method as recited in claim 1 , wherein the step of model checking includes establishing data race freedom in an undecidable concurrent program by establishing data race freedom in a parameterized system including the undecidable concurrent program.
4. The method as recited in claim 1 , wherein the threads are modeled as push down systems (PDSs).
5. The method as recited in claim 1 , wherein the threads interact with each other using synchronization primitives.
6. The method as recited in claim 1 , wherein the synchronization primitives include at least one of pairwise rendezvous, asynchronous rendezvous, disjunctive guards, broadcasts, nested locks and non-nested locks.
7. The method as recited in claim 1 , wherein f is a double-indexed LTL formula.
8. The method as recited in claim 1 , wherein using weighted multi-automata for internal transitions of the threads includes estimating a bound on a number of transitions fired in transit between two control states.
9. A method implemented by a computer for computing dataflow in a computer program of a computer system, comprising:
given a family of threads modeled as pushdown systems (U 1 , . . . , U m ) which interact by synchronization primitives and a Linear Temporal Logic (LTL) property, f, for a concurrent program, computing a cutoff for the LTL property, f, by computing bounds on a number of transitions fired along a computation of a thread between reachable control states of the concurrent program where the bounds are computed using weighted multi-automata on internal transitions of the threads; and
model checking a cutoff number of processes by parameterized model checking to verify data race freedom in the concurrent program.
10. The method as recited in claim 9 , wherein the step of model checking includes establishing data race freedom in a concurrent program with at least two distinct drivers, each running respective threads, by establishing data race freedom in a parameterized system comprised of a plurality of copies of the respective threads.
11. The method as recited in claim 9 , wherein the step of model checking includes establishing data race freedom in an undecidable concurrent program by establishing data race freedom in a parameterized system including the undecidable concurrent program.
12. The method as recited in claim 9 , wherein the synchronization primitives include at least one of pairwise rendezvous, asynchronous rendezvous, disjunctive guards, broadcasts, nested locks and non-nested locks.