{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:08:23Z","timestamp":1770282503817,"version":"3.49.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2017,1,31]],"date-time":"2017-01-31T00:00:00Z","timestamp":1485820800000},"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":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,1,31]]},"abstract":"<jats:p>We study a Hoare Logic to reason about parallel programs executed on graphics processing units (GPUs), called GPU kernels. During the execution of GPU kernels, multiple threads execute in lockstep, that is, execute the same instruction simultaneously. When the control branches, the two branches are executed sequentially, but during the execution of each branch only those threads that take it are enabled; after the control converges, all the threads are enabled and again execute in lockstep. In this article, we first consider a semantics in which all threads execute in lockstep (this semantics simplifies the actual execution model of GPUs) and adapt Hoare Logic to this setting by augmenting the usual Hoare triples with an additional component representing the set of enabled threads. It is determined that the soundness and relative completeness of the logic do not hold for all programs; a difficulty arises from the fact that one thread can invalidate the loop termination condition of another thread through shared memory. We overcome this difficulty by identifying an appropriate class of programs for which the soundness and relative completeness hold. Additionally, we discuss thread interleaving, which is present in the actual execution of GPUs but not in the lockstep semantics mentioned above. We show that if a program is race free, then the lockstep and interleaving semantics produce the same result. This implies that our logic is sound and relatively complete for race-free programs, even if the thread interleaving is taken into account.<\/jats:p>","DOI":"10.1145\/3001834","type":"journal-article","created":{"date-parts":[[2017,2,27]],"date-time":"2017-02-27T13:06:52Z","timestamp":1488200812000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A Hoare Logic for GPU Kernels"],"prefix":"10.1145","volume":"18","author":[{"given":"Kensuke","family":"Kojima","sequence":"first","affiliation":[{"name":"Kyoto University and CREST, JST, Kyoto, Japan"}]},{"given":"Atsushi","family":"Igarashi","sequence":"additional","affiliation":[{"name":"Kyoto University and CREST, JST, Kyoto, Japan"}]}],"member":"320","published-online":{"date-parts":[[2017,2,22]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.2197\/ipsjjip.24.132"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_15"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2743017"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2014.03.013"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_15"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966475"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_18"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_16"},{"key":"e_1_2_2_11_1","volume-title":"Gunter and Didier R\u00e9my","author":"Carl","year":"1993","unstructured":"Carl A. Gunter and Didier R\u00e9my . 1993 . A Proof-Theoretic Assessment of Runtime Type Errors. Technical Report. AT8T Bell Laboratories Technical Memo 11261-921230-43TM. Carl A. Gunter and Didier R\u00e9my. 1993. A Proof-Theoretic Assessment of Runtime Type Errors. Technical Report. AT8T Bell Laboratories Technical Memo 11261-921230-43TM."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_16"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_5"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Kensuke Kojima Akifumi Imanishi and Atsushi Igarashi. 2016. Automated Verification of Functional Correctness of Race-Free GPU Programs. (2016). draft.  Kensuke Kojima Akifumi Imanishi and Atsushi Igarashi. 2016. Automated Verification of Functional Correctness of Race-Free GPU Programs. (2016). draft.","DOI":"10.1007\/978-3-319-48869-1_7"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882320"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPSW.2012.302"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2145816.2145844"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/2388996.2389036"},{"key":"e_1_2_2_20_1","unstructured":"NVIDIA. 2014. NVIDIA CUDA C Programming Guide. NVIDIA.  NVIDIA. 2014. NVIDIA CUDA C Programming Guide. NVIDIA."},{"key":"e_1_2_2_21_1","unstructured":"NVIDIA. 2015. Parallel Thread Execution ISA Version 4.3. NVIDIA.  NVIDIA. 2015. Parallel Thread Execution ISA Version 4.3. NVIDIA."},{"key":"e_1_2_2_22_1","volume-title":"Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL\u201916)","author":"Okumura Kentaro","year":"2016","unstructured":"Kentaro Okumura , Kensuke Kojima , and Atsushi Igarashi . 2016 . Mechanization of hoare logic for SIMT in coq and verification of parallel prefix-sum algorithms . In Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL\u201916) . in Japanese. Kentaro Okumura, Kensuke Kojima, and Atsushi Igarashi. 2016. Mechanization of hoare logic for SIMT in coq and verification of parallel prefix-sum algorithms. In Proceedings of the 18th JSSST Workshop on Programming and Programming Languages (PPL\u201916). in Japanese."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1467-8659.2007.01012.x"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268134"},{"key":"e_1_2_2_26_1","volume-title":"The Formal Semantics of Programming Languages","author":"Winskel Glynn","unstructured":"Glynn Winskel . 1993. The Formal Semantics of Programming Languages . The MIT Press . Glynn Winskel. 1993. The Formal Semantics of Programming Languages. The MIT Press."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3001834","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3001834","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:50:07Z","timestamp":1750218607000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3001834"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,31]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,1,31]]}},"alternative-id":["10.1145\/3001834"],"URL":"https:\/\/doi.org\/10.1145\/3001834","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,1,31]]},"assertion":[{"value":"2014-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-02-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}