{"id":146452,"updated":"2025-01-20T06:50:11.900701+00:00","links":{},"created":"2025-01-19T00:21:54.893434+00:00","metadata":{"_oai":{"id":"oai:ipsj.ixsq.nii.ac.jp:00146452","sets":["934:935:8226:8350"]},"path":["8350"],"owner":"11","recid":"146452","title":["Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq"],"pubdate":{"attribute_name":"公開日","attribute_value":"2015-12-04"},"_buckets":{"deposit":"d69c8e6e-6d2f-48ca-b333-da54631f2a9e"},"_deposit":{"id":"146452","pid":{"type":"depid","value":"146452","revision_id":0},"owners":[11],"status":"published","created_by":11},"item_title":"Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq","author_link":["228686","228688","228687","228689","228684","228685"],"item_titles":{"attribute_name":"タイトル","attribute_value_mlt":[{"subitem_title":"Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq"},{"subitem_title":"Proof of Soundness of Concurrent Separation Logic for GPGPU in Coq","subitem_title_language":"en"}]},"item_keyword":{"attribute_name":"キーワード","attribute_value_mlt":[{"subitem_subject":"[通常論文] concurrent separation logic, Coq, GPGPU, barrier divergence","subitem_subject_scheme":"Other"}]},"item_type_id":"3","publish_date":"2015-12-04","item_3_text_3":{"attribute_name":"著者所属","attribute_value_mlt":[{"subitem_text_value":"Department of Mathematical and Computing Sciences, Tokyo Institute of Technology"},{"subitem_text_value":"Department of Mathematical and Computing Sciences, Tokyo Institute of Technology"},{"subitem_text_value":"Department of Mathematical and Computing Sciences, Tokyo Institute of Technology"}]},"item_3_text_4":{"attribute_name":"著者所属(英)","attribute_value_mlt":[{"subitem_text_value":"Department of Mathematical and Computing Sciences, Tokyo Institute of Technology","subitem_text_language":"en"},{"subitem_text_value":"Department of Mathematical and Computing Sciences, Tokyo Institute of Technology","subitem_text_language":"en"},{"subitem_text_value":"Department of Mathematical and Computing Sciences, Tokyo Institute of Technology","subitem_text_language":"en"}]},"item_language":{"attribute_name":"言語","attribute_value_mlt":[{"subitem_language":"eng"}]},"item_publisher":{"attribute_name":"出版者","attribute_value_mlt":[{"subitem_publisher":"情報処理学会","subitem_publisher_language":"ja"}]},"publish_status":"0","weko_shared_id":11,"item_file_price":{"attribute_name":"Billing file","attribute_type":"file","attribute_value_mlt":[{"url":{"url":"https://ipsj.ixsq.nii.ac.jp/record/146452/files/IPSJ-TPRO0804003.pdf","label":"IPSJ-TPRO0804003.pdf"},"date":[{"dateType":"Available","dateValue":"2017-12-04"}],"format":"application/pdf","billing":["billing_file"],"filename":"IPSJ-TPRO0804003.pdf","filesize":[{"value":"754.5 kB"}],"mimetype":"application/pdf","priceinfo":[{"tax":["include_tax"],"price":"0","billingrole":"5"},{"tax":["include_tax"],"price":"0","billingrole":"6"},{"tax":["include_tax"],"price":"0","billingrole":"15"},{"tax":["include_tax"],"price":"0","billingrole":"44"}],"accessrole":"open_date","version_id":"928ac571-5667-4a38-af4e-832f21a21e53","displaytype":"detail","licensetype":"license_note","license_note":"Copyright (c) 2015 by the Information Processing Society of Japan"}]},"item_3_creator_5":{"attribute_name":"著者名","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Izumi, Asakura"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Hidehiko, Masuhara"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Tomoyuki, Aotani"}],"nameIdentifiers":[{}]}]},"item_3_creator_6":{"attribute_name":"著者名(英)","attribute_type":"creator","attribute_value_mlt":[{"creatorNames":[{"creatorName":"Izumi, Asakura","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Hidehiko, Masuhara","creatorNameLang":"en"}],"nameIdentifiers":[{}]},{"creatorNames":[{"creatorName":"Tomoyuki, Aotani","creatorNameLang":"en"}],"nameIdentifiers":[{}]}]},"item_3_source_id_9":{"attribute_name":"書誌レコードID","attribute_value_mlt":[{"subitem_source_identifier":"AA11464814","subitem_source_identifier_type":"NCID"}]},"item_resource_type":{"attribute_name":"資源タイプ","attribute_value_mlt":[{"resourceuri":"http://purl.org/coar/resource_type/c_6501","resourcetype":"journal article"}]},"item_3_source_id_11":{"attribute_name":"ISSN","attribute_value_mlt":[{"subitem_source_identifier":"1882-7802","subitem_source_identifier_type":"ISSN"}]},"item_3_description_7":{"attribute_name":"論文抄録","attribute_value_mlt":[{"subitem_description":"We design a concurrent separation logic for GPGPU, namely GPUCSL, and prove its soundness by using Coq. GPUCSL is based on a CSL proposed by Blom et al., which is for automatic verification of GPGPU kernels, but employs different inference rules because the rules in Blom's CSL are not standard. For example, Blom's CSL does not have a frame rule. Our CSL is a simple extension of the original CSL, and it is more suitable as a basis of advanced properties proposed for other studies on CSLs. Our soundness proof is based on Vafeiadis' method, which is for a CSL with a fork-join concurrency model. The proof reveals two problems in Blom's approach in terms of soundness and extensibility. First, their assumption that thread ID independence of a kernel implies barrier divergence freedom does not hold. Second, it is not easy to extend their proof to other CSLs with a frame rule. Although our CSL covers only a subset of CUDA, our preliminary experiment shows that it is useful and expressive enough to verify a simple kernel with barriers.\n\\n------------------------------\nThis is a preprint of an article intended for publication Journal of\nInformation Processing(JIP). This preprint should not be cited. This\narticle should be cited as: Journal of Information Processing Vol.24(2016) No.1(online)\n------------------------------","subitem_description_type":"Other"}]},"item_3_description_8":{"attribute_name":"論文抄録(英)","attribute_value_mlt":[{"subitem_description":"We design a concurrent separation logic for GPGPU, namely GPUCSL, and prove its soundness by using Coq. GPUCSL is based on a CSL proposed by Blom et al., which is for automatic verification of GPGPU kernels, but employs different inference rules because the rules in Blom's CSL are not standard. For example, Blom's CSL does not have a frame rule. Our CSL is a simple extension of the original CSL, and it is more suitable as a basis of advanced properties proposed for other studies on CSLs. Our soundness proof is based on Vafeiadis' method, which is for a CSL with a fork-join concurrency model. The proof reveals two problems in Blom's approach in terms of soundness and extensibility. First, their assumption that thread ID independence of a kernel implies barrier divergence freedom does not hold. Second, it is not easy to extend their proof to other CSLs with a frame rule. Although our CSL covers only a subset of CUDA, our preliminary experiment shows that it is useful and expressive enough to verify a simple kernel with barriers.\n\\n------------------------------\nThis is a preprint of an article intended for publication Journal of\nInformation Processing(JIP). This preprint should not be cited. This\narticle should be cited as: Journal of Information Processing Vol.24(2016) No.1(online)\n------------------------------","subitem_description_type":"Other"}]},"item_3_biblio_info_10":{"attribute_name":"書誌情報","attribute_value_mlt":[{"bibliographic_titles":[{"bibliographic_title":"情報処理学会論文誌プログラミング（PRO）"}],"bibliographicIssueDates":{"bibliographicIssueDate":"2015-12-04","bibliographicIssueDateType":"Issued"},"bibliographicIssueNumber":"4","bibliographicVolumeNumber":"8"}]},"relation_version_is_last":true,"weko_creator_id":"11"}}