%0 Journal Article %1 LiaoWangChoStanleyKellyLafortuneMahlkeReveliotis13 %A Liao, Hongwei %A Wang, Yin %A Cho, HyounKyu %A Stanley, Jason %A Kelly, Terence %A Lafortune, Stéphane %A Mahlke, Scott %A Reveliotis, Spyros %B Discrete Event Dynamic Systems %D 2013 %I Springer US %J Discrete Event Dynamic Systems %K bloqueos, citas, citeulike concurrency, multithreaded, nets, petri, referencias, software %N 2 %P 157--195 %R 10.1007/s10626-012-0139-x %T Concurrency bugs in multithreaded software: modeling and analysis using Petri nets %U http://dx.doi.org/10.1007/s10626-012-0139-x %V 23 %X In this paper, we apply discrete-event system techniques to model and analyze the execution of concurrent software. The problem of interest is deadlock avoidance in shared-memory multithreaded programs. We employ Petri nets to systematically model multithreaded programs with lock acquisition and release operations. We define a new class of Petri nets, called Gadara nets, that arises from this modeling process. We investigate a set of important properties of Gadara nets, such as liveness, reversibility, and linear separability. We propose efficient algorithms for the verification of liveness of Gadara nets, and report experimental results on their performance. We also present modeling examples of real-world programs. The results in this paper lay the foundations for the development of effective control synthesis algorithms for Gadara nets.

@article{LiaoWangChoStanleyKellyLafortuneMahlkeReveliotis13, abstract = {{In this paper, we apply discrete-event system techniques to model and analyze the execution of concurrent software. The problem of interest is deadlock avoidance in shared-memory multithreaded programs. We employ Petri nets to systematically model multithreaded programs with lock acquisition and release operations. We define a new class of Petri nets, called Gadara nets, that arises from this modeling process. We investigate a set of important properties of Gadara nets, such as liveness, reversibility, and linear separability. We propose efficient algorithms for the verification of liveness of Gadara nets, and report experimental results on their performance. We also present modeling examples of real-world programs. The results in this paper lay the foundations for the development of effective control synthesis algorithms for Gadara nets.}}, added-at = {2017-09-08T10:52:59.000+0200}, author = {Liao, Hongwei and Wang, Yin and Cho, HyounKyu and Stanley, Jason and Kelly, Terence and Lafortune, St\'{e}phane and Mahlke, Scott and Reveliotis, Spyros}, biburl = {https://www.bibsonomy.org/bibtex/2374a7ab9d7ea7dad5bf645b41a5177ac/fernand0}, booktitle = {Discrete Event Dynamic Systems}, citeulike-article-id = {10689603}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/s10626-012-0139-x}, citeulike-linkout-1 = {http://www.springerlink.com/content/6700x02r314300x3}, citeulike-linkout-2 = {http://link.springer.com/article/10.1007/s10626-012-0139-x}, day = 13, doi = {10.1007/s10626-012-0139-x}, interhash = {4e26c44c331b5d6311448ac5c7279613}, intrahash = {374a7ab9d7ea7dad5bf645b41a5177ac}, issn = {0924-6703}, journal = {Discrete Event Dynamic Systems}, keywords = {bloqueos, citas, citeulike concurrency, multithreaded, nets, petri, referencias, software}, month = may, number = 2, pages = {157--195}, posted-at = {2012-09-24 18:19:04}, priority = {2}, publisher = {Springer US}, timestamp = {2017-09-08T10:53:23.000+0200}, title = {{Concurrency bugs in multithreaded software: modeling and analysis using Petri nets}}, url = {http://dx.doi.org/10.1007/s10626-012-0139-x}, volume = 23, year = 2013 }