{"id":795,"date":"2015-05-08T12:06:42","date_gmt":"2015-05-08T21:06:42","guid":{"rendered":"http:\/\/prg.is.titech.ac.jp\/?page_id=795"},"modified":"2020-01-18T13:36:41","modified_gmt":"2020-01-18T22:36:41","slug":"gpucsl","status":"publish","type":"page","link":"https:\/\/prg.is.titech.ac.jp\/ja\/projects\/gpgpu\/gpucsl\/","title":{"rendered":"GPGPU\u306e\u305f\u3081\u306e\u4e26\u884c\u5206\u96e2\u8ad6\u7406\u306eCoq\u306b\u3088\u308b\u5065\u5168\u6027\u8a3c\u660e"},"content":{"rendered":"<p>\u671d\u5009\u6cc9\" target=\"_blank\" rel=\"noopener\">Izumi Asakura<\/a><\/li>\n<li><a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/masuhara\/\" data-internallinksmanager029f6b8e52c=\"285\" title=\"\u5897\u539f\u82f1\u5f66\" target=\"_blank\" rel=\"noopener\">Hidehiko Masuhara<\/a><\/li>\n<li><a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/aotani\/\" data-internallinksmanager029f6b8e52c=\"290\" title=\"&lt;!--:en--&gt;Tomoyuki Aotani&lt;!--:--&gt;&lt;!--:ja--&gt;\u9752\u8c37\u77e5\u5e78&lt;!--:--&gt;\" target=\"_blank\" rel=\"noopener\">Tomoyuki Aotani<\/a><\/li>\n<\/ul>\n<h2>Soundness proof<\/h2>\n<p><a href=\"https:\/\/prg.is.titech.ac.jp\/wp-content\/uploads\/2015\/06\/GPUCSL.tar.gz\">Coq script(for 8.4pl4)<\/a><\/p>\n<h2>publication<\/h2>\n<ul>\n<li><a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/asakura\/\" data-internallinksmanager029f6b8e52c=\"291\" title=\"\u671d\u5009\u6cc9\" target=\"_blank\" rel=\"noopener\">Izumi Asakura<\/a>, <a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/masuhara\/\" data-internallinksmanager029f6b8e52c=\"285\" title=\"\u5897\u539f\u82f1\u5f66\" target=\"_blank\" rel=\"noopener\">Hidehiko Masuhara<\/a>, <a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/aotani\/\" data-internallinksmanager029f6b8e52c=\"290\" title=\"&lt;!--:en--&gt;Tomoyuki Aotani&lt;!--:--&gt;&lt;!--:ja--&gt;\u9752\u8c37\u77e5\u5e78&lt;!--:--&gt;\" target=\"_blank\" rel=\"noopener\">Tomoyuki Aotani<\/a><a href=\"https:\/\/prg.is.titech.ac.jp\/wp-content\/uploads\/2015\/10\/paper.pdf\"><br \/>\n<\/a><strong>Proof of Soundness of Concurrent Separation Logic\u00a0for GPGPU in Coq<\/strong><br \/>\nJournal of Information Processing Vol.24 No.1 132\u2013140 (2016)<br \/>\n<a href=\"https:\/\/prg.is.titech.ac.jp\/wp-content\/uploads\/2015\/10\/paper.pdf\">(PDF file)<\/a><\/li>\n<\/ul>\n<p>GPGPU \u5411\u3051\u306e\u4e26\u884c\u5206\u96e2\u8ad6\u7406 (GPUCSL) \u3092\u8a2d\u8a08\u3057,\u5b9a\u7406\u8a3c\u660e\u652f\u63f4\u5668 Coq \u3092\u7528\u3044\u305f\u5065\u5168\u6027\u306e\u8a3c\u660e\u3092\u4e0e\u3048\u308b. Blom \u3089\u306f GPGPU \u30ab\u30fc\u30cd\u30eb\u306e\u81ea\u52d5\u691c\u8a3c\u306e\u305f\u3081\u306b CSL \u3092\u8a2d\u8a08\u3057\u305f\u304c,\u305d\u306e\u63a8\u8ad6\u898f\u5247\u306f frame \u898f\u5247\u304c\u306a\u3044\u306a\u3069,\u6a19\u6e96\u7684\u306a CSL \u3068\u7570\u306a\u308b.\u672c\u7814\u7a76\u3067\u8a2d\u8a08\u3057\u305f GPUCSL \u306f,\u6a19\u6e96\u7684\u306a CSL \u306e\u7d20\u76f4\u306a\u62e1\u5f35\u3067\u3042\u308b\u305f\u3081, CSL \u306b\u95a2\u3059\u308b\u4ed6\u306e\u7814\u7a76\u6210\u679c\u3092\u53d6\u308a\u8fbc\u307f\u3084\u3059\u304f\u306a\u3063\u3066\u3044\u308b.\u5065\u5168\u6027\u306e\u8a3c\u660e\u306b\u306f, fork-join \u30e2\u30c7\u30eb\u306e\u4e26\u884c\u30d7\u30ed\u30b0\u30e9\u30e0\u5411\u3051 CSL \u306e\u5065\u5168\u6027\u306b\u3064\u3044\u3066\u306e Vafeiadis \u306e\u8a3c\u660e\u6cd5\u3092\u5fdc\u7528\u3057\u305f.\u3053\u306e\u8a3c\u660e\u3092\u901a\u3057\u3066, (1)\u00a0\u30b9\u30ec\u30c3\u30c9 ID \u72ec\u7acb\u6027\u3092\u30d0\u30ea\u30a2\u76f8\u9055 (barrier divergence) \u304c\u306a\u3044\u3053\u3068\u306e\u5341\u5206\u6761\u4ef6\u3068\u3057\u305f Blom \u3089\u306e\u8b70\u8ad6\u306e\u4e0d\u5099\u3068 (2) Blom \u3089\u306e\u8a3c\u660e\u306e\u5358\u7d14\u306a\u62e1\u5f35\u3067\u306f frame \u898f\u5247\u306e\u3042\u308b CSL \u306e\u5065\u5168\u6027\u3092\u793a\u305b\u306a\u3044\u3053\u3068\u3092\u660e\u3089\u304b\u306b\u3057\u305f.GPUCSL \u306f CUDA \u8a00\u8a9e\u306e\u30b5\u30d6\u30bb\u30c3\u30c8\u3092\u30e2\u30c7\u30eb\u5316\u3057\u305f\u3082\u306e\u3060\u304c,\u30d0\u30ea\u30a2\u540c\u671f\u3092\u7528\u3044\u305f\u5358\u7d14\u306a\u30ab\u30fc\u30cd\u30eb\u304c\u4ed5\u69d8\u3092\u6e80\u305f\u3059\u3053\u3068\u3092\u691c\u8a3c\u3059\u308b\u306e\u306b\u5341\u5206\u306a\u8868\u73fe\u529b\u3092\u6301\u3064.\u3053\u306e\u3053\u3068\u3092\u4e88\u5099\u5b9f\u9a13\u3092\u901a\u3057\u3066\u793a\u3057\u305f.<\/p>\n<h2>Members<\/h2>\n<ul>\n<li><a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/asakura\/\" data-internallinksmanager029f6b8e52c=\"291\" title=\"\u671d\u5009\u6cc9\" target=\"_blank\" rel=\"noopener\">\u671d\u5009<\/a> \u6cc9<\/li>\n<li><a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/masuhara\/\" data-internallinksmanager029f6b8e52c=\"285\" title=\"\u5897\u539f\u82f1\u5f66\" target=\"_blank\" rel=\"noopener\">\u5897\u539f<\/a> \u82f1\u5f66<\/li>\n<li><a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/aotani\/\" data-internallinksmanager029f6b8e52c=\"290\" title=\"&lt;!--:en--&gt;Tomoyuki Aotani&lt;!--:--&gt;&lt;!--:ja--&gt;\u9752\u8c37\u77e5\u5e78&lt;!--:--&gt;\" target=\"_blank\" rel=\"noopener\">\u9752\u8c37<\/a> \u77e5\u5e78<\/li>\n<\/ul>\n<h2>\u5065\u5168\u6027\u306e\u8a3c\u660e<\/h2>\n<p><a href=\"https:\/\/prg.is.titech.ac.jp\/wp-content\/uploads\/2015\/06\/GPUCSL.tar.gz\">Coq\u30b9\u30af\u30ea\u30d7\u30c8(for 8.4pl4)<\/a><\/p>\n<h2>\u8ad6\u6587<\/h2>\n<ul>\n<li><a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/asakura\/\" data-internallinksmanager029f6b8e52c=\"291\" title=\"\u671d\u5009\u6cc9\" target=\"_blank\" rel=\"noopener\">Izumi Asakura<\/a>, <a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/masuhara\/\" data-internallinksmanager029f6b8e52c=\"285\" title=\"\u5897\u539f\u82f1\u5f66\" target=\"_blank\" rel=\"noopener\">Hidehiko Masuhara<\/a>, <a href=\"https:\/\/prg.is.titech.ac.jp\/ja\/people\/aotani\/\" data-internallinksmanager029f6b8e52c=\"290\" title=\"&lt;!--:en--&gt;Tomoyuki Aotani&lt;!--:--&gt;&lt;!--:ja--&gt;\u9752\u8c37\u77e5\u5e78&lt;!--:--&gt;\" target=\"_blank\" rel=\"noopener\">Tomoyuki Aotani<\/a><a href=\"https:\/\/prg.is.titech.ac.jp\/wp-content\/uploads\/2015\/10\/paper.pdf\"><br \/>\n<\/a><strong>Proof of Soundness of Concurrent Separation Logic\u00a0for GPGPU in Coq<\/strong><br \/>\nJournal of Information Processing Vol.24 No.1 132\u2013140 (2016)<br \/>\n<a href=\"https:\/\/prg.is.titech.ac.jp\/wp-content\/uploads\/2015\/10\/paper.pdf\">(PDF file)<\/a><\/li>\n<\/ul>\n<p><\/p>","protected":false},"excerpt":{"rendered":"<p>\u671d\u5009\u6cc9&#8221; target=&#8221;_blank&#8221; rel=&#8221;noopener&#8221;>Izumi Asakura Hidehiko Masuhara Tomoyuki Aotani Soundness proof Coq script&hellip; <a class=\"continue\" href=\"https:\/\/prg.is.titech.ac.jp\/ja\/projects\/gpgpu\/gpucsl\/\">Continue Reading GPGPU\u306e\u305f\u3081\u306e\u4e26\u884c\u5206\u96e2\u8ad6\u7406\u306eCoq\u306b\u3088\u308b\u5065\u5168\u6027\u8a3c\u660e<\/a><\/p>\n","protected":false},"author":2,"featured_media":0,"parent":2581,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"nf_dc_page":"","footnotes":""},"class_list":["post-795","page","type-page","status-publish","hentry","radius"],"jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages\/795","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/comments?post=795"}],"version-history":[{"count":7,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages\/795\/revisions"}],"predecessor-version":[{"id":1161,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages\/795\/revisions\/1161"}],"up":[{"embeddable":true,"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/pages\/2581"}],"wp:attachment":[{"href":"https:\/\/prg.is.titech.ac.jp\/ja\/wp-json\/wp\/v2\/media?parent=795"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}