{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:48Z","timestamp":1750306608607,"version":"3.41.0"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,4,30]],"date-time":"2015-04-30T00:00:00Z","timestamp":1430352000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2015,5,21]]},"abstract":"<jats:p>\n            Recently, new libraries, such as Grand Central Dispatch (GCD), have been proposed to directly harness the power of multicore platforms and to make the development of concurrent software more accessible to software engineers. When using such a library, the programmer writes so-called\n            <jats:italic>blocks<\/jats:italic>\n            , which are chunks of code, and dispatches them using\n            <jats:italic>synchronous<\/jats:italic>\n            or\n            <jats:italic>asynchronous<\/jats:italic>\n            calls to several types of waiting queues. A scheduler is then responsible for dispatching those blocks among the available cores. Blocks can synchronize via a global memory. In this article, we propose Queue-Dispatch Asynchronous Systems as a mathematical model that faithfully formalizes the synchronization mechanisms and behavior of the scheduler in those systems. We study in detail their relationships to classical formalisms such as pushdown systems, Petri nets, F\n            <jats:sc>ifo<\/jats:sc>\n            systems, and counter systems. Our main technical contributions are precise worst-case complexity results for the Parikh coverability problem and the termination problem for several subclasses of our model. We also consider an extension of Q\n            <jats:sc>das<\/jats:sc>\n            with a fork-join mechanism. Adding fork-join to any of the subclasses that we have identified leads to undecidability of the coverability problem. This motivates the study of over-approximations. Finally, we consider handmade abstractions as a practical way of verifying programs that cannot be faithfully modeled by decidable subclasses of Q\n            <jats:sc>das<\/jats:sc>\n            .\n          <\/jats:p>","DOI":"10.1145\/2700072","type":"journal-article","created":{"date-parts":[[2015,5,1]],"date-time":"2015-05-01T17:49:08Z","timestamp":1430502548000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["On the Verification of Concurrent, Asynchronous Programs with Waiting Queues"],"prefix":"10.1145","volume":"14","author":[{"given":"Gilles","family":"Geeraerts","sequence":"first","affiliation":[{"name":"Universit\u00e9 libre de Bruxelles, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Heu\u00dfner","sequence":"additional","affiliation":[{"name":"Otto-Friedrich-Universit\u00e4t Bamberg, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[{"name":"Universit\u00e9 libre de Bruxelles, Belgium"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,4,30]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Apple. 2009. DispatchWebServer in Mac Developper Library. Retreived from https:\/\/developer.apple.com\/library\/mac\/.  Apple. 2009. DispatchWebServer in Mac Developper Library. Retreived from https:\/\/developer.apple.com\/library\/mac\/."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103681"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of CONCUR\u201997 (LNCS)","volume":"1243","author":"Bouajjani A.","unstructured":"A. Bouajjani , J. Esparza , and O. Maler . 1997. Reachability analysis of pushdown automata: Application to model-checking . In Proceedings of CONCUR\u201997 (LNCS) , Vol. 1243 . Springer, 135--150. A. Bouajjani, J. Esparza, and O. Maler. 1997. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of CONCUR\u201997 (LNCS), Vol. 1243. Springer, 135--150."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/322374.322380"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_8_1","volume-title":"LNCS","volume":"1491","author":"Esparza J.","year":"1998","unstructured":"J. Esparza . 1998 . Decidability and complexity of Petri net problems\u2014an introduction. In Lectures on Petri nets I . LNCS , Vol. 1491 . Springer. J. Esparza. 1998. Decidability and complexity of Petri net problems\u2014an introduction. In Lectures on Petri nets I. LNCS, Vol. 1491. Springer."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of CAV\u201900 (LNCS)","volume":"1855","author":"Esparza J.","unstructured":"J. Esparza , D. Hansel , P. Rossmanith , and S. Schwoon . 2000. Efficient algorithms for model checking pushdown systems . In Proceedings of CAV\u201900 (LNCS) , Vol. 1855 . Springer, 232--247. J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. 2000. Efficient algorithms for model checking pushdown systems. In Proceedings of CAV\u201900 (LNCS), Vol. 1855. Springer, 232--247."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2160910.2160915"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480895"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38697-8_4"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2013.18"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"A. Heu\u00dfner J. Leroux A. Muscholl and G. Sutre. 2012. Reachability analysis of communicating pushdown systems. Logical Methods in Computer Science 8 3 (2012).  A. Heu\u00dfner J. Leroux A. Muscholl and G. Sutre. 2012. Reachability analysis of communicating pushdown systems. Logical Methods in Computer Science 8 3 (2012).","DOI":"10.2168\/LMCS-8(3:23)2012"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00139-1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190266"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_21"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of TACAS\u201908 (LNCS)","volume":"4963","author":"Torre S. La","unstructured":"S. La Torre , P. Madhusudan , and G. Parlato . 2008. Context-bounded analysis of concurrent queue systems . In Proceedings of TACAS\u201908 (LNCS) , Vol. 4963 . Springer, 299--314. S. La Torre, P. Madhusudan, and G. Parlato. 2008. Context-bounded analysis of concurrent queue systems. In Proceedings of TACAS\u201908 (LNCS), Vol. 4963. Springer, 299--314."},{"key":"e_1_2_1_19_1","unstructured":"libdispatch. 2013. Project Web Page. Retrieved from http:\/\/libdispatch.macosforge.org\/.  libdispatch. 2013. Project Web Page. Retrieved from http:\/\/libdispatch.macosforge.org\/."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1095587"},{"key":"e_1_2_1_22_1","unstructured":"mist2. 2014. Tool repository and web page. (2014). https:\/\/github.com\/pierreganty\/mist.  mist2. 2014. Tool repository and web page. (2014). https:\/\/github.com\/pierreganty\/mist."},{"key":"e_1_2_1_23_1","unstructured":"QDAS. 2014. mist2 Example Code. Retrieved from http:\/\/www.swt-bamberg.de\/aheussner\/research\/qdas.html.  QDAS. 2014. mist2 Example Code. Retrieved from http:\/\/www.swt-bamberg.de\/aheussner\/research\/qdas.html."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(78)90036-1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_29"},{"key":"e_1_2_1_26_1","unstructured":"SPIN. 2014. Project Web Page. Retrieved from http:\/\/www.spinroot.com.  SPIN. 2014. Project Web Page. Retrieved from http:\/\/www.spinroot.com."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2700072","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2700072","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:17:00Z","timestamp":1750227420000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2700072"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,30]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,5,21]]}},"alternative-id":["10.1145\/2700072"],"URL":"https:\/\/doi.org\/10.1145\/2700072","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2015,4,30]]},"assertion":[{"value":"2013-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-04-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}