{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:15:24Z","timestamp":1762521324490,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,7,19]],"date-time":"2009-07-19T00:00:00Z","timestamp":1247961600000},"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":[],"published-print":{"date-parts":[[2009,7,19]]},"DOI":"10.1145\/1639622.1639624","type":"proceedings-article","created":{"date-parts":[[2009,10,27]],"date-time":"2009-10-27T13:27:28Z","timestamp":1256650048000},"page":"1-6","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Some resources for teaching concurrency"],"prefix":"10.1145","author":[{"given":"Ganesh","family":"Gopalakrishnan","sequence":"first","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu","family":"Yang","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sarvani","family":"Vakkalanka","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anh","family":"Vo","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Aananthakrishnan","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grzegorz","family":"Szubzda","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Geof","family":"Sawaya","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jason","family":"Williams","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Subodh","family":"Sharma","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"DeLisi","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simone","family":"Atzeni","sequence":"additional","affiliation":[{"name":"Univ. of Utah, Salt Lake City, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2009,7,19]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Intel Academic Alliance http:\/\/software.intel.com\/en-us\/articles\/courseware-access\/  Intel Academic Alliance http:\/\/software.intel.com\/en-us\/articles\/courseware-access\/"},{"key":"e_1_3_2_1_2_1","unstructured":"External Research Microsoft. http:\/\/research.microsoft.com\/en-us\/collaboration\/  External Research Microsoft. http:\/\/research.microsoft.com\/en-us\/collaboration\/"},{"key":"e_1_3_2_1_3_1","volume-title":"Morgan-Kauffman","author":"Herlihy Maurice","year":"2004","unstructured":"Maurice Herlihy and Nir Shavit . The Art of Multiprocessor Programming . Morgan-Kauffman , 2004 . Maurice Herlihy and Nir Shavit. The Art of Multiprocessor Programming. Morgan-Kauffman, 2004."},{"key":"e_1_3_2_1_4_1","volume-title":"Principles of Parallel Programming Addison-Wesley","author":"Snyder Lawrence","year":"2008","unstructured":"Lawrence Snyder and Calvin Lin . Principles of Parallel Programming Addison-Wesley , 2008 . Lawrence Snyder and Calvin Lin. Principles of Parallel Programming Addison-Wesley, 2008."},{"key":"e_1_3_2_1_5_1","unstructured":"Jack B. Dennis. Toward the computer utility http:\/\/csg.csail.mit.edu\/Users\/dennis\/essay.htm  Jack B. Dennis. Toward the computer utility http:\/\/csg.csail.mit.edu\/Users\/dennis\/essay.htm"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1504176.1504177"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2008.209"},{"key":"e_1_3_2_1_8_1","unstructured":"Herb Sutter. \"The Free Lunch is Over\" http:\/\/www.gotw.ca\/publications\/concurrency-ddj.htm  Herb Sutter. \"The Free Lunch is Over\" http:\/\/www.gotw.ca\/publications\/concurrency-ddj.htm"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1095408.1095421"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1400214.1400227"},{"key":"e_1_3_2_1_11_1","unstructured":"Charles Leiserson and Ilya Mirman How to survive the multicore software revolution. http:\/\/www.cilk.com\/ebook\/download5643  Charles Leiserson and Ilya Mirman How to survive the multicore software revolution. http:\/\/www.cilk.com\/ebook\/download5643"},{"key":"e_1_3_2_1_12_1","unstructured":"The MIT Cilk System. http:\/\/supertech.csail.mit.edu\/cilk\/  The MIT Cilk System. http:\/\/supertech.csail.mit.edu\/cilk\/"},{"key":"e_1_3_2_1_13_1","unstructured":"Using LLNL's Supercomputers. https:\/\/computing.llnl.gov\/tutorials\/agenda\/index.html  Using LLNL's Supercomputers. https:\/\/computing.llnl.gov\/tutorials\/agenda\/index.html"},{"key":"e_1_3_2_1_14_1","first-page":"401","volume":"2004","author":"Gopalakrishnan Ganesh","unstructured":"Ganesh Gopalakrishnan , Yu Yang , Hemanthkumar Sivaraj . QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings. Computer Aided Verification 2004 , 401 -- 413 , LNCS 3113. Ganesh Gopalakrishnan, Yu Yang, Hemanthkumar Sivaraj. QB or Not QB: An Efficient Execution Verification Tool for Memory Orderings. Computer Aided Verification 2004, 401--413, LNCS 3113.","journal-title":"Computer Aided Verification"},{"key":"e_1_3_2_1_15_1","unstructured":"MPEC\n  : A SAT-based checker for Itanium Executions. http:\/\/www.cs.utah.edu\/formal_verification\/software\/mpec.  MPEC: A SAT-based checker for Itanium Executions. http:\/\/www.cs.utah.edu\/formal_verification\/software\/mpec."},{"key":"e_1_3_2_1_16_1","volume-title":"Reasoning about Parallel Architectures","author":"Collier W. W.","year":"1992","unstructured":"W. W. Collier . Reasoning about Parallel Architectures . Prentice-Hall , 1992 . W. W. Collier. Reasoning about Parallel Architectures. Prentice-Hall, 1992."},{"key":"e_1_3_2_1_17_1","unstructured":"Sections 7.2 and 7.3 Intel Software Developer's Manual Chapter 7.: http:\/\/www.intel.com\/design\/processor\/manuals\/253668.pdf  Sections 7.2 and 7.3 Intel Software Developer's Manual Chapter 7.: http:\/\/www.intel.com\/design\/processor\/manuals\/253668.pdf"},{"key":"e_1_3_2_1_18_1","unstructured":"Geof Sawaya. Examples from Pacheco's book pacheco. http:\/\/www.cs.utah.edu\/formal_verification\/geof\/pacheco\/table.html.  Geof Sawaya. Examples from Pacheco's book pacheco. http:\/\/www.cs.utah.edu\/formal_verification\/geof\/pacheco\/table.html."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Hans Boehm. Threads cannot be implemented as a library. http:\/\/www.hpl.hp.com\/techreports\/2004\/HPL-2004-209.html PLDI 2005.  Hans Boehm. Threads cannot be implemented as a library. http:\/\/www.hpl.hp.com\/techreports\/2004\/HPL-2004-209.html PLDI 2005.","DOI":"10.1145\/1065010.1065042"},{"key":"e_1_3_2_1_20_1","unstructured":"Hans Boehm. Reordering Constraints for Pthread-style Locks. http:\/\/www.hpl.hp.com\/techreports\/2005\/HPL-2005-217R1.html?jumpid=reg_R1002_USEN PPoPP 2007.  Hans Boehm. Reordering Constraints for Pthread-style Locks. http:\/\/www.hpl.hp.com\/techreports\/2005\/HPL-2005-217R1.html?jumpid=reg_R1002_USEN PPoPP 2007."},{"key":"e_1_3_2_1_21_1","volume-title":"Morgan-Kauffman","author":"Pacheco Peter S.","year":"1997","unstructured":"Peter S. Pacheco . Parallel Programming with MPI . Morgan-Kauffman , 1997 . Peter S. Pacheco. Parallel Programming with MPI. Morgan-Kauffman, 1997."},{"key":"e_1_3_2_1_22_1","unstructured":"Pthreads\/C code of a producer\/consumer routine. http:\/\/www.eng.utah.edu\/~cs5966\/Week4\/prodcons.c  Pthreads\/C code of a producer\/consumer routine. http:\/\/www.eng.utah.edu\/~cs5966\/Week4\/prodcons.c"},{"key":"e_1_3_2_1_23_1","unstructured":"The Cilk++ tool suite. http:\/\/www.cilk.com  The Cilk++ tool suite. http:\/\/www.cilk.com"},{"key":"e_1_3_2_1_24_1","unstructured":"http:\/\/www.eng.utah.edu\/~cs5966\/  http:\/\/www.eng.utah.edu\/~cs5966\/"},{"key":"e_1_3_2_1_25_1","unstructured":"http:\/\/www.cs.utah.edu\/formal_verification\/ISP_Tests\/.  http:\/\/www.cs.utah.edu\/formal_verification\/ISP_Tests\/."},{"key":"e_1_3_2_1_26_1","unstructured":"http:\/\/www.cs.utah.edu\/formal_verification\/ISP-release\/.  http:\/\/www.cs.utah.edu\/formal_verification\/ISP-release\/."},{"key":"e_1_3_2_1_27_1","unstructured":"Examples of Using ISP on the LLNL benchmarks and the Red-Black benchmarks. http:\/\/www.cs.utah.edu\/~jtwilla\/WORK\/ISPTests.html  Examples of Using ISP on the LLNL benchmarks and the Red-Black benchmarks. http:\/\/www.cs.utah.edu\/~jtwilla\/WORK\/ISPTests.html"},{"key":"e_1_3_2_1_28_1","unstructured":"Files containing Message Passing pedagogical examples. http:\/\/www.cs.utah.edu\/formal_verification\/padtad09-files\/  Files containing Message Passing pedagogical examples. http:\/\/www.cs.utah.edu\/formal_verification\/padtad09-files\/"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_9"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1504176.1504214"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87475-1_36"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390841.1390844"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87475-1_34"},{"key":"e_1_3_2_1_34_1","unstructured":"http:\/\/research.microsoft.com\/en-us\/projects\/chess\/.  http:\/\/research.microsoft.com\/en-us\/projects\/chess\/."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250785"},{"key":"e_1_3_2_1_36_1","unstructured":"http:\/\/javapathfinder.sourceforge.net\/.  http:\/\/javapathfinder.sourceforge.net\/."},{"key":"e_1_3_2_1_38_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"1999","unstructured":"E. M. Clarke , O. Grumberg , and D. Peled . Model Checking . MIT Press , Dec. 1999 . E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Dec. 1999."},{"key":"e_1_3_2_1_39_1","volume":"36","author":"Dwyer M.","year":"1999","unstructured":"M. Dwyer , J. Hatcliff , and D. Schmidt . Bandera: Tools for automated reasoning about software system behavior. In ERCIM News , 36 , Jan. 1999 . M. Dwyer, J. Hatcliff, and D. Schmidt. Bandera: Tools for automated reasoning about software system behavior. In ERCIM News, 36, Jan. 1999.","journal-title":"In ERCIM News"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040315"},{"issue":"2","key":"e_1_3_2_1_41_1","first-page":"1998","volume":"3","author":"Godefroid P.","unstructured":"P. Godefroid , B. Hanmer , and L. Jagadeesan . Systematic software testing using VeriSoft: An analysis of the 4ess heart-beat monitor. Bell Labs Technical Journal , 3 ( 2 ), April--June 1998 . P. Godefroid, B. Hanmer, and L. Jagadeesan. Systematic software testing using VeriSoft: An analysis of the 4ess heart-beat monitor. Bell Labs Technical Journal, 3(2), April--June 1998.","journal-title":"Bell Labs Technical Journal"},{"key":"e_1_3_2_1_42_1","volume-title":"Concurrency at microsoft - an exploratory survey","author":"Godefroind P.","year":"2008","unstructured":"P. Godefroind and N. Nagappan . Concurrency at microsoft - an exploratory survey , 2008 . EC2 (Exploiting Concurrency Efficiently and Correctly), Princeton , 2008. http:\/\/www.cs.utah.edu\/ec2\/2008. P. Godefroind and N. Nagappan. Concurrency at microsoft - an exploratory survey, 2008. EC2 (Exploiting Concurrency Efficiently and Correctly), Princeton, 2008. http:\/\/www.cs.utah.edu\/ec2\/2008."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24732-6_20"},{"key":"e_1_3_2_1_45_1","unstructured":"J. Yang etal MODIST: Transparent Model Checking of Unmodified Distributed System. NSDI 09. To appear.   J. Yang et al. MODIST: Transparent Model Checking of Unmodified Distributed System. NSDI 09. To appear."},{"key":"e_1_3_2_1_46_1","first-page":"58","volume-title":"Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software. SPIN","author":"Yang Y.","year":"2007","unstructured":"Y. Yang , X. Chen , G. Gopalakrishnan , and R. M. Kirby . Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software. SPIN 2007 , Pages 58 -- 75 , Springer LNCS 4595. Y. Yang, X. Chen, G. Gopalakrishnan, and R. M. Kirby. Distributed Dynamic Partial Order Reduction Based Verification of Threaded Software. SPIN 2007, Pages 58--75, Springer LNCS 4595."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_20"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02652-2_22"},{"key":"e_1_3_2_1_49_1","unstructured":"MPI\n  : A Message-Passing Interface Standard. http:\/\/www.mpi-forum.org\/  MPI: A Message-Passing Interface Standard. http:\/\/www.mpi-forum.org\/"},{"key":"e_1_3_2_1_50_1","volume-title":"Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufman","author":"John","year":"2004","unstructured":"John L. Hennessy and David A . Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufman , 2004 . John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufman, 2004."}],"event":{"name":"ISSTA '09: International Symposium on Software Testing and Analysis","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Chicago Illinois","acronym":"ISSTA '09"},"container-title":["Proceedings of the 7th Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1639622.1639624","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1639622.1639624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:30:28Z","timestamp":1750253428000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1639622.1639624"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,7,19]]},"references-count":49,"alternative-id":["10.1145\/1639622.1639624","10.1145\/1639622"],"URL":"https:\/\/doi.org\/10.1145\/1639622.1639624","relation":{},"subject":[],"published":{"date-parts":[[2009,7,19]]},"assertion":[{"value":"2009-07-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}