{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:33Z","timestamp":1750306773381,"version":"3.41.0"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2013,9,16]],"date-time":"2013-09-16T00:00:00Z","timestamp":1379289600000},"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. Archit. Code Optim."],"published-print":{"date-parts":[[2013,9,16]]},"abstract":"<jats:p>\n            In this article we use model checking to statically distribute and schedule\n            <jats:italic>Synchronous DataFlow<\/jats:italic>\n            (SDF) graphs on\n            <jats:italic>heterogeneous execution architectures<\/jats:italic>\n            . We show that model checking is capable of providing an optimal solution and it arrives at these solutions faster (in terms of algorithm runtime) than equivalent ILP formulations. Furthermore, we also show how different types of optimizations such as task parallelism, data parallelism, and state sharing can be included within our framework. Finally, comparison of our approach with the current state-of-the-art heuristic techniques show the pitfalls of these techniques and gives a glimpse of how these heuristic techniques can be improved.\n          <\/jats:p>","DOI":"10.1145\/2512435","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T13:47:05Z","timestamp":1379944025000},"page":"1-25","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Orchestrating stream graphs using model checking"],"prefix":"10.1145","volume":"10","author":[{"given":"Avinash","family":"Malik","sequence":"first","affiliation":[{"name":"IBM Research Ireland, Ireland"}]},{"given":"David","family":"Gregg","sequence":"additional","affiliation":[{"name":"Lero, Trinity College Dublin, Ireland"}]}],"member":"320","published-online":{"date-parts":[[2013,9,16]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/361604.361619"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Amnell T. Behrmann G. Bengtsson J. Dargenio P. R. David A. Fehnker A. Hune T. Jeannet B. Larsen K. G. Moller M. O. Pettersson P. Weise C. and Yi W. 2001. Modeling and Verification of Parallel Processes. Springer 99--124.   Amnell T. Behrmann G. Bengtsson J. Dargenio P. R. David A. Fehnker A. Hune T. Jeannet B. Larsen K. G. Moller M. O. Pettersson P. Weise C. and Yi W. 2001. Modeling and Verification of Parallel Processes. Springer 99--124.","DOI":"10.1007\/3-540-45510-8_4"},{"volume":"3185","volume-title":"Eds. Lecture Notes in Computer Science","author":"Behrmann G.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2005.363"},{"volume-title":"Proceedings of the Symposium on Logic in Computer Science (LICS'90)","author":"Burch J.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629395.1629406"},{"key":"e_1_2_1_7_1","unstructured":"Clarke E. M. Grumberg O. and Peled D. 2000. Model Checking. MIT Press.  Clarke E. M. Grumberg O. and Peled D. 2000. Model Checking. MIT Press."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1137\/0207001"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950406"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168917.1168877"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1015452903532"},{"volume":"1066","volume-title":"Proceedings of the DIMACS\/SYCON Workshop on Hybrid Systems III: Verification and Control, R. Alur, T. A. Henzinger, and E. D. Sontag, Eds. Lecture Notes in Computer Science","author":"Gupta V.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/T-C.1975.224171"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375596"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1987.5009446"},{"key":"e_1_2_1_17_1","unstructured":"Malik A. and Gregg D. 2012a. Executing synchronous data flow graphs on heterogeenous execution architectures using integer linear programming. Tech. rep. TCD-CS-2012-03 School of Computer Science and Statistics Trinity College Dublin.  Malik A. and Gregg D. 2012a. Executing synchronous data flow graphs on heterogeenous execution architectures using integer linear programming. Tech. rep. TCD-CS-2012-03 School of Computer Science and Statistics Trinity College Dublin."},{"key":"e_1_2_1_18_1","unstructured":"Malik A. and Gregg D. 2012b. Theorems for model-checking. Tech. rep. TCD-CS-2012-17 School of Computer Science and Statistics Trinity College Dublin.  Malik A. and Gregg D. 2012b. Theorems for model-checking. Tech. rep. TCD-CS-2012-17 School of Computer Science and Statistics Trinity College Dublin."},{"key":"e_1_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Roop P. S. Andalam S. Hanxleden R. Yuan S. and Traulsen C. 2009. Tight wcrt analysis of synchronous c programs. Tech. rep. 0912 Christian-Albrechts-Universitat Kiel Department of Computer Science. May.  Roop P. S. Andalam S. Hanxleden R. Yuan S. and Traulsen C. 2009. Tight wcrt analysis of synchronous c programs. Tech. rep. 0912 Christian-Albrechts-Universitat Kiel Department of Computer Science. May.","DOI":"10.1145\/1629395.1629424"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.242160"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2009.20"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Waingold E. Taylor M. Sarkar V. Lee V. Lee W. Kim J. Frank M. Finch P. Devabhaktumi S. Barua R. Babb J. Amarsinghe S. and Agarwal A. 1997. Baring it all to software: The raw machine. Tech. rep. MIT. http:\/\/groups.csail.mit.edu\/cag\/raw\/documents\/Waingold-LCS-TR-1997.pdf.   Waingold E. Taylor M. Sarkar V. Lee V. Lee W. Kim J. Frank M. Finch P. Devabhaktumi S. Barua R. Babb J. Amarsinghe S. and Agarwal A. 1997. Baring it all to software: The raw machine. Tech. rep. MIT. http:\/\/groups.csail.mit.edu\/cag\/raw\/documents\/Waingold-LCS-TR-1997.pdf.","DOI":"10.1109\/2.612254"}],"container-title":["ACM Transactions on Architecture and Code Optimization"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2512435","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2512435","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:59Z","timestamp":1750231739000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2512435"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,16]]},"references-count":22,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2013,9,16]]}},"alternative-id":["10.1145\/2512435"],"URL":"https:\/\/doi.org\/10.1145\/2512435","relation":{},"ISSN":["1544-3566","1544-3973"],"issn-type":[{"type":"print","value":"1544-3566"},{"type":"electronic","value":"1544-3973"}],"subject":[],"published":{"date-parts":[[2013,9,16]]},"assertion":[{"value":"2012-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-09-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}