文献

J-GLOBAL ID：202002250245505842   整理番号：20A2436339

型システムを用いたロックフリースタックの検証

著者 (2件)： 佐藤駿太朗 (東北大 大学院情報科学研究科) ,  住井英二郎 (東北大 大学院情報科学研究科)
資料名： 日本ソフトウェア科学会大会講演論文集(Web)  (Proceeding of the JSSST Annual Conference (Web))
巻： 37th  ページ： ROMBUNNO.61-L (WEB ONLY)  発行年： 2020年 
JST資料番号： U1746A  ISSN： 1349-3515  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ・ロックフリー性とTyPiCalについて説明:デッドロックやライブロックが起きない,並行システムの重要な性質,π計算のプロセスのロックフリー性を型システムにもとづき検証するツール。
・TyPiCalを再帰型を持つセル構造で拡張,Treiberのロックフリースタックを表現,そのデッドロックフリー性を検証。
・デッドロックに限らないロックフリー性は,有限回のスタック操作についてハイブリッド型システムを用いて検証,その際に必要な停止性をすべての遷移列を列挙して検証。

シソーラス用語： *デッドロック ,  仕様記述 ,  データ型 ,  データ構造 ,  入出力制御 ,  並行処理 ,  制御理論 ,  ハイブリッド系 ,  計算機プログラミング ,  スレッド ,  同期制御 ,  相互排除 ,  プログラム解析 ,  並列演算 ,  アルゴリズム ,  π計算 ,  ハイブリッドシステム ,  型システム ,  静的コード解析
準シソーラス用語： ロックフリー ,  *ロックフリースタック ,  静的解析 ,  排他制御 ,  並行システム ,  並行プログラミング

分類 (1件)： 制御方式  (JC02030K)

タイトルに関連する用語 (4件)： 型システム ,  ロック ,  スタック ,  検証