{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,21]],"date-time":"2025-09-21T18:11:03Z","timestamp":1758478263488,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662466629"},{"type":"electronic","value":"9783662466636"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46663-6_11","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T14:37:47Z","timestamp":1427899067000},"page":"212-232","source":"Crossref","is-referenced-by-count":26,"title":["Protocols by Default"],"prefix":"10.1007","author":[{"given":"Nicholas","family":"Ng","sequence":"first","affiliation":[]},{"given":"Jose Gabriel","family":"de Figueiredo Coutinho","sequence":"additional","affiliation":[]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Aananthakrishnan, S., Bronevetsky, G., Gopalakrishnan, G.: Hybrid approach for data-flow analysis of MPI programs. In: ICS 2013, pp. 455\u2013456. ACM (2013)","DOI":"10.1145\/2464996.2467286"},{"issue":"10","key":"11_CR2","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/1562764.1562783","volume":"52","author":"K. Asanovic","year":"2009","unstructured":"Asanovic, K., Wawrzynek, J., Wessel, D., Yelick, K., Bodik, R., Demmel, J., Keaveny, T., Keutzer, K., Kubiatowicz, J., Morgan, N., Patterson, D., Sen, K.: A view of the parallel computing landscape. CACM\u00a052(10), 56 (2009)","journal-title":"CACM"},{"key":"11_CR3","unstructured":"Balaji, P., Dinan, J., Hoefler, T., Thakur, R.: Advanced MPI Programming (Tutorial at SC 2013). \n                      \n                        http:\/\/www.mcs.anl.gov\/~thakur\/sc13-mpi-tutorial\/"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Boob, S., Gonz\u00e1lez-V\u00e9lez, H., Popescu, A.M.: Automated instantiation of heterogeneous fast flow CPU\/GPU parallel pattern applications in clouds. In: PDP, pp. 162\u2013169. IEEE (2014)","DOI":"10.1109\/PDP.2014.88"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Bronevetsky, G.: Communication-Sensitive Static Dataflow for Parallel Message Passing Applications. In: CGO 2009, pp. 1\u201312. IEEE (2009)","DOI":"10.1109\/CGO.2009.32"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Cardoso, J.: a.M., Carvalho, T., Coutinho, J.G., Luk, W., Nobre, R., Diniz, P., Petrov, Z.: LARA: an aspect-oriented programming language for embedded systems. In: AOSD 2012, pp. 179\u2013190. ACM (2012)","DOI":"10.1145\/2162049.2162071"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"issue":"1","key":"11_CR8","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/99.660313","volume":"5","author":"L. Dagum","year":"1998","unstructured":"Dagum, L., Menon, R.: OpenMP: an industry standard API for shared-memory programming. Computational Science and Engineering\u00a05(1), 46\u201355 (1998)","journal-title":"Computational Science and Engineering"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-32940-1_20","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"R. Demangeon","year":"2012","unstructured":"Demangeon, R., Honda, K.: Nested protocols in session types. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 272\u2013286. Springer, Heidelberg (2012)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Deni\u00e9lou, P.M., Yoshida, N.: Dynamic multirole session types. In: POPL 2011, pp. 435\u2013446. ACM (2011)","DOI":"10.1145\/1925844.1926435"},{"issue":"4","key":"11_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(4:6)2012","volume":"8","author":"P.M. Denielou","year":"2012","unstructured":"Denielou, P.M., Yoshida, N., Bejleri, A., Hu, R.: Parameterised Multiparty Session Types. Logical Methods in Computer Science\u00a08(4), 1\u201346 (2012)","journal-title":"Logical Methods in Computer Science"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"DeSouza, J., Kuhn, B., de Supinski, B.R., Samofalov, V., Zheltov, S., Bratanov, S.: Automated, scalable debugging of MPI programs with Intel Message Checker. In: SE-HPCS 2005, pp. 78\u201382. ACM (2005)","DOI":"10.1145\/1145319.1145342"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-45255-9_47","volume-title":"Recent Advances in Parallel Virtual Machine and Message Passing Interface","author":"G.E. Fagg","year":"2000","unstructured":"Fagg, G.E., Dongarra, J.J.: FT-MPI: Fault Tolerant MPI, Supporting Dynamic Applications in a Dynamic World. In: Dongarra, J., Kacsuk, P., Podhorszki, N. (eds.) PVM\/MPI 2000. LNCS, vol.\u00a01908, pp. 346\u2013353. Springer, Heidelberg (2000)"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Ferner, C., Wilkinson, B., Heath, B.: Toward using higher-level abstractions to teach parallel computing. In: IPDPSW, pp. 1291\u20131296. IEEE (2013)","DOI":"10.1109\/IPDPSW.2013.71"},{"issue":"12","key":"11_CR15","doi-asserted-by":"publisher","first-page":"1135","DOI":"10.1002\/spe.1026","volume":"40","author":"H. Gonz\u00e1lez-V\u00e9lez","year":"2010","unstructured":"Gonz\u00e1lez-V\u00e9lez, H., Leyton, M.: A Survey of Algorithmic Skeleton Frameworks: High-level Structured Parallel Programming Enablers. Softw. Pract. Exper.\u00a040(12), 1135\u20131160 (2010)","journal-title":"Softw. Pract. Exper."},{"issue":"12","key":"11_CR16","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/2043174.2043194","volume":"54","author":"G. Gopalakrishnan","year":"2011","unstructured":"Gopalakrishnan, G., Kirby, R.M., Siegel, S., Thakur, R., Gropp, W., Lusk, E., De Supinski, B.R., Schulz, M., Bronevetsky, G.: Formal analysis of MPI-based parallel programs. CACM\u00a054(12), 82\u201391 (2011)","journal-title":"CACM"},{"key":"11_CR17","unstructured":"Graepel, T., Candela, J.Q., Borchert, T., Herbrich, R.: Web-Scale Bayesian Click-Through Rate Prediction for Sponsored Search Advertising in Microsofts Bing Search Engine. In: ICML 2010, pp. 13\u201320 (2010)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Hilbrich, T., Protze, J., Schulz, M., de Supinski, B.R., M\u00fcller, M.S.: MPI Runtime Error Detection with MUST: Advances in Deadlock Detection. In: SC 2012, pp. 1\u201311. IEEE (2012)","DOI":"10.1109\/SC.2012.79"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL 2008, vol. 5201, pp. 273\u2013284. ACM (2008)","DOI":"10.1145\/1328897.1328472"},{"key":"11_CR20","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1016\/j.future.2014.02.006","volume":"37","author":"J. Kolodziej","year":"2014","unstructured":"Kolodziej, J., Gonz\u00e1lez-V\u00e9lez, H., Wang, L.: Advances in data-intensive modelling and simulation. Future Generation Comp. Syst.\u00a037, 282\u2013283 (2014)","journal-title":"Future Generation Comp. Syst."},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Krammer, B., Bidmon, K., M\u00fcller, M.S., Resch, M.M.: MARMOT: an MPI analysis and checking tool. In: PARCO 2003, pp. 493\u2013500 (2003)","DOI":"10.1016\/S0927-5452(04)80063-7"},{"key":"11_CR22","unstructured":"Online Appendix., \n                      \n                        http:\/\/www.doc.ic.ac.uk\/~cn06\/codegen"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Mancini, E.P., Marsh, G., Panda, D.K.: An MPI-stream hybrid programming model for computational clusters. In: CCGrid 2010, pp. 323\u2013330. IEEE (2010)","DOI":"10.1109\/CCGRID.2010.33"},{"key":"11_CR24","unstructured":"Marques, E.R., Martins, F., Vasconcelos, V.T., Santos, C., Ng, N., Yoshida, N.: Protocol-based verification of C+MPI programs. DI-FCUL 13, U. of Lisbon (2014)"},{"key":"11_CR25","unstructured":"Message Passing Interface, \n                      \n                        http:\/\/www.mcs.anl.gov\/research\/projects\/mpi\/"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Ng, N., Yoshida, N.: Pabble: Parameterised Scribble. SOCA, 1\u201316 (2014)","DOI":"10.1007\/s11761-014-0172-8"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Ng, N., Yoshida, N.: Pabble: Parameterised Scribble for Parallel Programming. In: PDP, pp. 707\u2013714. IEEE (2014)","DOI":"10.1109\/PDP.2014.20"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-30561-0_15","volume-title":"Objects, Models, Components, Patterns","author":"N. Ng","year":"2012","unstructured":"Ng, N., Yoshida, N., Honda, K.: Multiparty Session C: Safe Parallel Programming with Message Optimisation. In: Furia, C.A., Nanz, S. (eds.) TOOLS 2012. LNCS, vol.\u00a07304, pp. 202\u2013218. Springer, Heidelberg (2012)"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-05032-4_7","volume-title":"Software Engineering and Formal Methods","author":"N. Ng","year":"2014","unstructured":"Ng, N., Yoshida, N., Luk, W.: Scalable Session Programming for Heterogeneous High-Performance Systems. In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol.\u00a08368, pp. 82\u201398. Springer, Heidelberg (2014)"},{"key":"11_CR30","unstructured":"Pabble project page, \n                      \n                        http:\/\/www.doc.ic.ac.uk\/~cn06\/pabble"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Rabhi, F., Gorlatch, S. (eds.): Patterns and Skeletons for Parallel and Distributed Computing. Springer (2003)","DOI":"10.1007\/978-1-4471-0097-3"},{"issue":"4","key":"11_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1862648.1862652","volume":"3","author":"M. Salda\u00f1a","year":"2010","unstructured":"Salda\u00f1a, M., Patel, A., Madill, C., Nunes, D., Wang, D., Chow, P., Wittig, R., Styles, H., Putnam, A.: MPI as a Programming Model for High-Performance Reconfigurable Computers. ACM TRETS\u00a03(4), 1\u201329 (2010)","journal-title":"ACM TRETS"},{"key":"11_CR33","unstructured":"Scribble homepage, \n                      \n                        http:\/\/scribble.org\/"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-33296-8_15","volume-title":"Formal Methods: Foundations and Applications","author":"S. Sharma","year":"2012","unstructured":"Sharma, S., Gopalakrishnan, G., Bronevetsky, G.: A sound reduction of persistent-sets for deadlock detection in mpi applications. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol.\u00a07498, pp. 194\u2013209. Springer, Heidelberg (2012)"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-642-18275-4_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S.F. Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: Collective assertions. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 387\u2013402. Springer, Heidelberg (2011)"},{"issue":"4","key":"11_CR36","first-page":"427","volume":"5","author":"S.F. Siegel","year":"2011","unstructured":"Siegel, S.F., Zirkel, T.K.: FEVS: A Functional Equivalence Verification Suite for High-Performance Scientific Computing. MSCS\u00a05(4), 427\u2013435 (2011)","journal-title":"MSCS"},{"key":"11_CR37","unstructured":"Sklml webpage, \n                      \n                        http:\/\/sklml.inria.fr"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"Vetter, J.S., de Supinski, B.R.: Dynamic Software Testing of MPI Applications with Umpire. In: SC 2000, p. 51. IEEE (2000)","DOI":"10.1109\/SC.2000.10055"},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"Vo, A., Aananthakrishnan, S., Gopalakrishnan, G., de Supinski, B., Schulz, M., Bronevetsky, G.: A scalable and distributed dynamic formal verifier for mpi programs. In: SC 2010, pp. 1\u201310. IEEE (2010)","DOI":"10.1109\/SC.2010.7"},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Vo, A., Vakkalanka, S., DeLisi, M., Gopalakrishnan, G., et al.: Formal verification of practical MPI programs. In: PPoPP 2009, pp. 261\u2013270. ACM (2008)","DOI":"10.1145\/1594835.1504214"},{"key":"11_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"859","DOI":"10.1007\/978-3-642-32820-6_85","volume-title":"Euro-Par 2012 Parallel Processing","author":"S. Wienke","year":"2012","unstructured":"Wienke, S., Springer, P., Terboven, C., an Mey, D.: OpenACC \u2013 First Experiences with Real-World Applications. In: Kaklamanis, C., Papatheodorou, T., Spirakis, P.G. (eds.) Euro-Par 2012. LNCS, vol.\u00a07484, pp. 859\u2013870. Springer, Heidelberg (2012)"},{"key":"11_CR42","doi-asserted-by":"crossref","unstructured":"Wilkinson, B., Villalobos, J., Ferner, C.: Pattern programming approach for teaching parallel and distributed computing. In: SIGCSE 2013, pp. 409\u2013414. ACM (2013)","DOI":"10.1145\/2445196.2445319"}],"container-title":["Lecture Notes in Computer Science","Compiler Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46663-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:35:22Z","timestamp":1559140522000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46663-6_11"}},"subtitle":["Safe MPI Code Generation Based on Session Types"],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466629","9783662466636"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46663-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}