排他制御を含むプログラムから論理制約付き項書換え系への変換

小嶋美咲; 西田直樹; 松原豊; 酒井正彦

文献

J-GLOBAL ID：202002222533973036 整理番号：20A1049023

排他制御を含むプログラムから論理制約付き項書換え系への変換

Transforming Programs with Exclusive Control into Logically Constrained Term Rewrite Systems

出版者サイト複写サービスで全文入手 {{ this.onShowCLink("http://jdream3.com/copy/?sid=JGLOBAL&noSystem=1&documentNoArray=20A1049023&COPY=1") }}
高度な検索・分析はJDreamⅢで {{ this.onShowJLink("http://jdream3.com/lp/jglobal/index.html?docNo=20A1049023&from=J-GLOBAL&jstjournalNo=S0532B") }}

著者 (4件)： , , ,
資料名：
巻： 119 号： 451(SS2019 41-60)(Web) ページ： 31-36 (WEB ONLY) 発行年： 2020年02月26日
JST資料番号： S0532B ISSN： 0913-5685 資料種別：会議録 (C)
記事区分：原著論文発行国：日本 (JPN) 言語：日本語 (JA)

計算モデルである論理制約付き項書換え系(LCTRS)をプログラムの検証に用いる先行研究では,逐次実行される命令型プログラムを対象としている.現実の計算機の利用状況を考えると,逐次実行されるプログラムとそれを並行化したプログラムが等価であることを検証したいという要求がある.本稿では,並行実行されるプログラムをLCTRSで表現すること目的として,セマフォによる排他制御を含むプログラムをLCTRSで表現する方法を提案する.そのためにまず,先行研究で導入された実行環境を表す関数記号の引数を,実行されるプロセスの数だけ増やすことで,プロセスの並行実行を表現する.次に,セマフォに対する操作を書換え規則で表現し,セマフォによる排他制御を含むプログラムをLCTRSに変換する.セマフォに対する待ち行列を番号札を使って管理することで,リストなどの再帰データ構造を導入せずにセマフォの操作を表現する.(著者抄録)

, , , , , , , , , , , ,
, , , ,

計算機システム開発

引用文献 (11件)：

F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998.
Ştefan Ciobâcă and D. Lucanu. A coinductive approach to proving reachability properties in logically constrained term rewriting systems. In Proc. IJCAR 2018, Vol. 10900 of LNCS, pp. 295-311. Springer, 2018.
C. Fuhs, C. Kop, and N. Nishida. Verifying procedural programs via constrained rewriting induction. ACM Transactions on Computational Logic, 18(2):14:1-14:50, 2017.
Y. Kanazawa and N. Nishida. On transforming functions accessing global variables into logically constrained term rewriting systems. In Proc. WPTE 2018, Vol. 289 of EPTCS, pp. 34-52. Open Publishing Association, 2019.
C. Kop and N. Nishida. Term rewriting with logical constraints. In Proc. FroCoS 2013, Vol. 8152 of LNCS, pp. 343-358. Springer, 2013.

, , ,

前のページに戻る