講演抄録/キーワード |
講演名 |
2020-03-04 15:10
排他制御を含むプログラムから論理制約付き項書換え系への変換 ○小嶋美咲・西田直樹・松原 豊・酒井正彦(名大) SS2019-46 |
抄録 |
(和) |
計算モデルである論理制約付き項書換え系(LCTRS)をプログラムの検証に用いる先行研究では,逐次実行される命令型プログラムを対象としている.現実の計算機の利用状況を考えると,逐次実行されるプログラムとそれを並行化したプログラムが等価であることを検証したいという要求がある.本稿では,並行実行されるプログラムをLCTRSで表現すること目的として,セマフォによる排他制御を含むプログラムをLCTRSで表現する方法を提案する.そのためにまず,先行研究で導入された実行環境を表す関数記号の引数を,実行されるプロセスの数だけ増やすことで,プロセスの並行実行を表現する.次に,セマフォに対する操作を書換え規則で表現し,セマフォによる排他制御を含むプログラムをLCTRSに変換する.セマフォに対する待ち行列を番号札を使って管理することで,リストなどの再帰データ構造を導入せずにセマフォの操作を表現する. |
(英) |
To apply Logically Constrained Term Rewrite Systems (LCTRSs, for short) to program verification, a previous work targets programs that are executed sequentially. Considering actual usage of computers, it has been expected to develop a verification method for equivalence between sequentially executed programs and their concurrent versions. In this paper, we propose a transformation of programs with exclusive control based on semaphores into LCTRSs, aiming at modeling concurrent programs by LCTRSs. To this end, we first expand arguments of a function symbol that has been introduced to represent a configuration of sequential execution, so as to store all executed processes. Next, we show how to represent operations for semaphores by rewrite rules, and show a transformation of programs with exclusive control based on semaphores into LCTRSs. We manage waiting lists for semaphores by means of number checks, avoiding recursive data structures such as lists. |
キーワード |
(和) |
制約付き書換え / プログラム変換 / プログラム検証 / 命令型プログラム / 並行性 / / / |
(英) |
constrained rewriting / program transformation / program verification / imperative programs / concurrency / / / |
文献情報 |
信学技報, vol. 119, no. 451, SS2019-46, pp. 31-36, 2020年3月. |
資料番号 |
SS2019-46 |
発行日 |
2020-02-26 (SS) |
ISSN |
Online edition: ISSN 2432-6380 |
著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します.(許諾番号:10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) |
PDFダウンロード |
SS2019-46 |