DECIDABILITY OF REACHABILITY FOR THREADS COMMUNICATING VIA LOCKS

摘要

A system and method for deciding reachability includes inputting a concurrent program having threads interacting via locks for analysis. Bounds on lengths of paths that need to be explored are computed to decide reachability for lock patterns by assuming bounded lock chains. Reachability is determined for a pair of locations using a bounded model checker. The program is updated in accordance with the reachability determination.