登入
選單
返回
Google圖書搜尋
Verification of Chare-kernel Programs
Sanjay Bhansali
Laxmikant Vasudeo Kalé
University of Illinois at Urbana-Champaign. Department of Computer Science
出版
Department of Computer Science, University of Illinois at Urbana-Champaign
, 1989
URL
http://books.google.com.hk/books?id=x0l0nn7o7q0C&hl=&source=gbs_api
註釋
Abstract: "Experience with concurrent programming has shown that concurrent programs can conceal bugs even after extensive testing. Thus, there is a need for practical techniques which can establish the correctness of parallel programs. This paper proposes a method for showing how to prove the partial correctness of programs written in the Chare-kernel language, which is a language designed to support the parallel execution of computation with irregular structures. The proof is based on the lattice proof technique of Owicki and Lamport and is divided in two parts. The first part is concerned with the program behavior within a single chare instance, whereas the second part captures the inter-chare interaction."