{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:50:39Z","timestamp":1740099039969,"version":"3.37.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319779348"},{"type":"electronic","value":"9783319779355"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-77935-5_25","type":"book-chapter","created":{"date-parts":[[2018,3,10]],"date-time":"2018-03-10T10:02:34Z","timestamp":1520676154000},"page":"367-382","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Model-Checking Task Parallel Programs for Data-Race"],"prefix":"10.1007","author":[{"given":"Radha","family":"Nakade","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2264-2958","authenticated-orcid":false,"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0602-2000","authenticated-orcid":false,"given":"Peter","family":"Aldous","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jay","family":"McCarthy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,3,11]]},"reference":[{"issue":"1","key":"25_CR1","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1006\/jpdc.1996.0107","volume":"37","author":"RD Blumofe","year":"1996","unstructured":"Blumofe, R.D., Joerg, C.F., Kuszmaul, B.C., Leiserson, C.E., Randall, K.H., Zhou, Y.: Cilk: an efficient multithreaded runtime system. J. Parallel Distrib. Comput. 37(1), 55\u201369 (1996)","journal-title":"J. Parallel Distrib. Comput."},{"issue":"10","key":"25_CR2","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1145\/1103845.1094852","volume":"40","author":"P Charles","year":"2005","unstructured":"Charles, P., Grothoff, C., Saraswat, V., Donawa, C., Kielstra, A., Ebcioglu, K., von Praun, C., Sarkar, V.: X10: an object-oriented approach to non-uniform cluster computing. SIGPLAN Not. 40(10), 519\u2013538 (2005)","journal-title":"SIGPLAN Not."},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Cav\u00e9, V., Zhao, J., Shirako, J., Sarkar, V.: Habanero-Java: the new adventures of old X10. In: Proceedings of the 9th International Conference on Principles and Practice of Programming in Java, pp. 51\u201361. ACM (2011)","DOI":"10.1145\/2093157.2093165"},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Imam, S., Sarkar, V.: Habanero-Java library: a Java 8 framework for multicore programming. In: Proceedings of the 2014 International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools, pp. 75\u201386. ACM (2014)","DOI":"10.1145\/2647508.2647514"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Feng, M., Leiserson, C.E.: Efficient detection of determinacy races in Cilk programs. In: Proceedings of the Ninth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1997, pp. 1\u201311. ACM, New York (1997)","DOI":"10.1145\/258492.258493"},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"Cheng, G.I., Feng, M., Leiserson, C.E., Randall, K.H., Stark, A.F.: Detecting data races in Cilk programs that use locks. In: Proceedings of the Tenth Annual ACM Symposium on Parallel Algorithms and Architectures, SPAA 1998, pp. 298\u2013309. ACM, New York (1998)","DOI":"10.1145\/277651.277696"},{"key":"25_CR7","doi-asserted-by":"crossref","unstructured":"Bender, M.A., Fineman, J.T., Gilbert, S., Leiserson, C.E.: On-the-fly maintenance of series-parallel relationships in fork-join multithreaded programs. In: Proceedings of the Sixteenth Annual ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2004, pp. 133\u2013144. ACM, New York (2004)","DOI":"10.1145\/1007912.1007933"},{"issue":"3","key":"25_CR8","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/s10703-012-0143-7","volume":"41","author":"R Raman","year":"2012","unstructured":"Raman, R., Zhao, J., Sarkar, V., Vechev, M.T., Yahav, E.: Efficient data race detection for async-finish parallelism. Form. Methods Syst. Des. 41(3), 321\u2013347 (2012)","journal-title":"Form. Methods Syst. Des."},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Utterback, R., Agrawal, K., Fineman, J.T., Lee, I.T.A.: Provably good and practically efficient parallel race detection for fork-join programs. In: Proceedings of the 28th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2016, pp. 83\u201394. ACM, New York (2016)","DOI":"10.1145\/2935764.2935801"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-319-46982-9_23","volume-title":"Runtime Verification","author":"R Surendran","year":"2016","unstructured":"Surendran, R., Sarkar, V.: Dynamic determinacy race detection for task parallelism with futures. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 368\u2013385. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_23"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Mellor-Crummey, J.: On-the-fly detection of data races for programs with nested fork-join parallelism. In: Proceedings of the 1991 ACM\/IEEE Conference on Supercomputing, Supercomputing 1991, pp. 24\u201333. ACM, New York (1991)","DOI":"10.1145\/125826.125861"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Raman, R., Zhao, J., Sarkar, V., Vechev, M., Yahav, E.: Scalable and precise dynamic datarace detection for structured parallelism. In: ACM SIGPLAN Notices, vol. 47, no. 6, pp. 531\u2013542. ACM (2012)","DOI":"10.1145\/2254064.2254127"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1007\/978-3-642-31057-7_27","volume-title":"ECOOP 2012 \u2013 Object-Oriented Programming","author":"E Westbrook","year":"2012","unstructured":"Westbrook, E., Zhao, J., Budimli\u0107, Z., Sarkar, V.: Practical permissions for race-free parallelism. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 614\u2013639. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31057-7_27"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Gligoric, M., Mehlitz, P.C., Marinov, D.: X10X: model checking a new programming language with an \u201cold\u201d model checker. In: 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, pp. 11\u201320. IEEE (2012)","DOI":"10.1109\/ICST.2012.81"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-38088-4_14","volume-title":"NASA Formal Methods","author":"TK Zirkel","year":"2013","unstructured":"Zirkel, T.K., Siegel, S.F., McClory, T.: Automated verification of chapel programs using model checking and symbolic execution. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 198\u2013212. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_14"},{"issue":"1","key":"25_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2557833.2560582","volume":"39","author":"P Anderson","year":"2014","unstructured":"Anderson, P., Chase, B., Mercer, E.: JPF verification of Habanero Java programs. ACM SIGSOFT Softw. Eng. Notes 39(1), 1\u20137 (2014)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"issue":"7","key":"25_CR17","doi-asserted-by":"crossref","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"issue":"6","key":"25_CR18","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1145\/3140587.3062374","volume":"52","author":"D Kini","year":"2017","unstructured":"Kini, D., Mathur, U., Viswanathan, M.: Dynamic race prediction in linear time. SIGPLAN Not. 52(6), 157\u2013170 (2017)","journal-title":"SIGPLAN Not."},{"issue":"6","key":"25_CR19","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1145\/2666356.2594315","volume":"49","author":"J Huang","year":"2014","unstructured":"Huang, J., Meredith, P.O., Rosu, G.: Maximal sound predictive race detection with control flow abstraction. SIGPLAN Not. 49(6), 337\u2013348 (2014)","journal-title":"SIGPLAN Not."},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Dennis, J.B., Gao, G.R., Sarkar, V.: Determinacy and repeatability of parallel program schemata. In: 2012 Data-Flow Execution Models for Extreme Scale Computing (DFM), pp. 1\u20139. IEEE (2012)","DOI":"10.1109\/DFM.2012.10"},{"issue":"1","key":"25_CR21","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1145\/2103621.2103681","volume":"47","author":"A Bouajjani","year":"2012","unstructured":"Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. ACM SIGPLAN Not. 47(1), 203\u2013214 (2012)","journal-title":"ACM SIGPLAN Not."},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Mercer, E., Anderson, P., Vrvilo, N., Sarkar, V.: Model checking task parallel programs using gradual permissions. In: Proceedings of 30th IEEE\/ACM International Conference on Automated Software Engineering, New Ideas Category, pp. 535\u2013540. ACM (2015)","DOI":"10.1109\/ASE.2015.75"},{"issue":"6","key":"25_CR23","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1002\/1096-9128(200005)12:6<375::AID-CPE480>3.0.CO;2-M","volume":"12","author":"JM Bull","year":"2000","unstructured":"Bull, J.M., Smith, L.A., Westhead, M.D., Henty, D.S., Davey, R.A.: A benchmark suite for high performance Java. Concurr. - Pract. Exp. 12(6), 375\u2013388 (2000)","journal-title":"Concurr. - Pract. Exp."},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-11454-5_2","volume-title":"Using and Improving OpenMP for Devices, Tasks, and More","author":"P Virouleau","year":"2014","unstructured":"Virouleau, P., Brunet, P., Broquedis, F., Furmento, N., Thibault, S., Aumage, O., Gautier, T.: Evaluation of OpenMP dependent tasks with the KASTORS benchmark suite. In: DeRose, L., de Supinski, B.R., Olivier, S.L., Chapman, B.M., M\u00fcller, M.S. (eds.) IWOMP 2014. LNCS, vol. 8766, pp. 16\u201329. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11454-5_2"},{"key":"25_CR25","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Sinha, N., Kruus, E., Zhang, Y.: Static data race detection for concurrent programs with asynchronous calls. In: Proceedings of the 7th Joint Meeting of the European Software Engineering Conference and the Foundations of Software Engineering, pp. 13\u201322. ACM (2009)","DOI":"10.1145\/1595696.1595701"},{"key":"25_CR26","unstructured":"Kulikov, S., Shafiei, N., Van Breugel, F., Visser, W.: Detecting data races with Java PathFinder (2010)"},{"key":"25_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-15769-1_28","volume-title":"Static Analysis","author":"M Vechev","year":"2010","unstructured":"Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic verification of determinism for structured parallel programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 455\u2013471. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_28"},{"key":"25_CR28","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using Verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1997, pp. 174\u2013186. ACM, New York (1997)","DOI":"10.1145\/263699.263717"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Freund, S.N.: FastTrack: efficient and precise dynamic race detection. In: ACM SIGPLAN Notices, vol. 44, no. 6, pp. 121\u2013133. ACM (2009)","DOI":"10.1145\/1542476.1542490"},{"issue":"5","key":"25_CR30","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/543552.512560","volume":"37","author":"JD Choi","year":"2002","unstructured":"Choi, J.D., Lee, K., Loginov, A., O\u2019Callahan, R., Sarkar, V., Sridharan, M.: Efficient and precise datarace detection for multithreaded object-oriented programs. SIGPLAN Not. 37(5), 258\u2013269 (2002)","journal-title":"SIGPLAN Not."},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Dimitrov, D., Raychev, V., Vechev, M., Koskinen, E.: Commutativity race detection. In: ACM SIGPLAN Notices, vol. 49, no. 6, pp. 305\u2013315. ACM (2014)","DOI":"10.1145\/2666356.2594322"},{"key":"25_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-74061-2_14","volume-title":"Static Analysis","author":"A Malkis","year":"2007","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Precise thread-modular verification. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 218\u2013232. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_14"},{"key":"25_CR33","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Berdine, J., Cook, B., Sagiv, M.: Thread-modular shape analysis. In: ACM SIGPLAN Notices, vol. 42, no. 6, pp. 266\u2013277. ACM (2007)","DOI":"10.1145\/1250734.1250765"},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: ACM SIGOPS Operating Systems Review, vol. 37, no. 5, pp. 237\u2013252. ACM (2003)","DOI":"10.1145\/945445.945468"},{"key":"25_CR35","doi-asserted-by":"crossref","unstructured":"Elmas, T., Qadeer, S., Tasiran, S.: Goldilocks: a race and transaction-aware Java runtime. In: ACM SIGPLAN Notices, vol. 42, no. 6, pp. 245\u2013255. ACM (2007)","DOI":"10.1145\/1273442.1250762"},{"key":"25_CR36","doi-asserted-by":"crossref","unstructured":"Voung, J.W., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Proceedings of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, pp. 205\u2013214. ACM (2007)","DOI":"10.1145\/1287624.1287654"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-77935-5_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,12]],"date-time":"2019-10-12T13:02:00Z","timestamp":1570885320000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-77935-5_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319779348","9783319779355"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-77935-5_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}