Abstract: Due to the sharing of resources, the deadlocks often occur as concurrency bugs in multithreaded software. This paper utilizes the Petri net to model multithreaded software and use the mixed integer programming tool to test the concurrency bugs in it. Currently, multithreaded software using the mutex can be modeled and tested by the Gadara nets. Multithreaded software using semaphores can be modeled by S^*PRnets, but there is no theory to support the mixed integer programming-based concurrency bugs test method for them. This paper defines a subclass of S^*PRnets, i.e., SEM-S^*PRnets. The initial marking of resource places in it can be greater than 1 and branches can use resources symmetrically. Thus, it can model a class of multithreaded software using semaphores. By structural analysis, it can be proved that a SEM-S^*PRnet is live if and only if all its siphons are always marked during execution. This result ensures that the mixed integer programming techniques can also be applied for detecting concurrency bugs in multithreaded software modeled by SEM-S^*PRnets. Finally, two concurrency bug test examples are introduced, and the results show the validity of this work.

Key words: multithreaded software, petri nets, S^*PRnet, deadlock test, mixed integer programming