並行論理型言語における同期ポイント移動の安全性について
スポンサーリンク
概要
- 論文の詳細を見る
並行論理型言語では, プロセス間の同期は変数に対する入出力によって行われる.したがって入力が不完全なために何も出力できないプロセスは, 必要な入力を待った後で実行すればよいであろう.このプロセス変換は同期ポイントの移動と呼ばれており, プロセスの最適な実行順序を計算するために使用して実装の最適化に応用可能である.この手法を実装するには, プロセスが何かを出力するために必要な入力を求める必要があるが, 並行論理型言語のような非決定的な枠組みにおいて, それを正確に求めることは一般には難しい.そこで本論文では, 何らかの値に具体化されている必要のある変数を指摘する抽象実行の方法を紹介し, その正当性を論じる.発散も失敗もしないプロセスは, 同期ポイントの移動の前後で表示的意味が保存されることを証明した.正当性を論じるために使用した表示的意味論は, 操作的意味論におけるプロセスの入出力の時系列を集めたものであり, その定義の簡素さによって表示的意味の等価性の証明を容易にしている.また, 述語呼び出しの書き換え時に起こる変数名の付け替えについて, 式の上で新しい変数を入手可能にする変数変換と呼ばれる記法を導入し, いくつかの性質を証明した.それを利用して構成した, プロセスの書き換えの親子関係を明示的に残す操作的意味論についても説明する.
- 2000-03-15
著者
関連論文
- 並列計算機システムFOLON上へのPVMの移植と評価
- 階層グラフ書換え言語における並行プロセスの型推論
- 双対モデリングを用いた充足可能性問題のCNF encoding
- 微分制約論理式によるハイブリッドシステムのモデリングと検証
- なぜソフトウェア論文を書くのは難しい(と感じる)のか
- 特集「ソフトウェア論文」の編集にあたって
- 3A-1 大規模メモリ環境下におけるモデル検査ツールSpinのマルチコア検証機能の性能評価(高性能計算,一般セッション,アーキテクチャ)
- 3A-2 強連結成分ベースのグラフ分割による分散並列LTLモデル検査の高速化(高性能計算,一般セッション,アーキテクチャ)
- 6ZJ-9 階層グラフ書換え言語LMNtalによるモデル検査(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 4K-2 分散検証環境DiVinEを用いた分散LTLモデル検査アルゴリズムの性能評価(情報爆発時代における分散処理とセキュリティ,一般セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 6ZJ-7 並列SATソルバにおけるlemma共有およびプール制約伝播高速化(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- SATソルバ MiniSat の並列化とそのチューニング手法(HPC-2 : 数値解析I)
- A-022 数式処理システムMathematica上における再帰除去システム(A分野:モデル・アルゴリズム・プログラミング)
- プロファイルを使用した並列LTLモデル検査のチューニング
- ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法
- A-007 区間演算を用いたODE Solverにおける任意精度演算の導入とパラメタ最適化(モデル・アルゴリズム・プログラミング,一般論文)
- ハイブリッドシステムの高信頼シミュレーションのための区間に基づく制約伝播手法
- LMNtalモデル検査器における状態爆発対策(高信頼化,2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
- 強連結成分の特性を用いた並列モデル検査アルゴリズムSCC-OWCTYの設計と評価(高信頼化,2010年並列/分散/協調処理に関する『金沢』サマー・ワークショップSWoPP2010)
- ソフトウェア論文座談会
- 階層グラフ書換え言語LMNtalの処理系(ソフトウェア論文)
- LMNtal処理系および他言語インタフェースの設計と実装
- 制約に基づく解析による並行論理プログラムの自動デバッグ
- 6K-4 LMNtal処理系SLIMのモデル検査機能の並列化(情報爆発時代における並列分散処理技術,一般セッション,「情報爆発」時代に向けた新IT基盤技術,情報処理学会創立50周年記念(第72回)全国大会)
- 6K-2 クラスタ向け並列precosatの開発と性能評価(情報爆発時代における並列分散処理技術,一般セッション,「情報爆発」時代に向けた新IT基盤技術,情報処理学会創立50周年記念(第72回)全国大会)
- 1M-1 ハイブリッドシステムモデリング言語HydLaの区間制約に基づく全解シミュレーション実行処理系(モデリング・上流設計,学生セッション,アーキテクチャ,情報処理学会創立50周年記念)
- 論理・制約プログラミングと並行計算(論理と推論技術の展開)
- 特集「論理と推論技術の展開」の編集にあたって
- 6ZJ-8 軽量なLMNtal実行時処理系SLIMの設計と実装(情報爆発時代における並列分散処理技術,学生セッション,「情報爆発」時代に向けた新しいIT基盤技術)
- 4N-2 KLICへのデータ並列処理機能の導入について
- 3K-2 汎用並列組合せ最適化パッケージの構想
- C. A. R. Hoare : Communicating Sequential Processes(20世紀の名著名論)
- シンガポール国立大学
- 私はCrusoeを使いたい(インタラクティブ・エッセイ)
- A-014 LMNtalコンパイラにおける並び替えとグループ化を用いた命令列の最適化(A分野:モデル・アルゴリズム・プログラミング)
- 並列計算機システムFOLONの通信ライブラリの設計と評価
- 見込み計算を用いたニュースリーダの応答性改善法
- 10. 21世紀COEプロジェクト「プロダクティブICTアカデミア」(21世紀卓越した情報研究拠点プログラムの目指す研究(前編))
- 21世紀COEプロジェクト「プロダクティブICTアカデミア」
- 4T-7 WWW全文検索システムVernoのアーキテクチャ
- 4T-6 WWW全文検索システムVernoのデータベース
- 分散型WWW全文収集ロボットIron33
- 学習型WWW検索エンジンVerno
- LA_003 後継関数を持つリスト型非線形再帰プログラムに対する再帰除去法(A分野:モデル・アルゴリズム・プログラミング)
- 制約プログラミングに関する日本・フランス間の研究交流
- E-026 JPドメインにおける茶筌を用いた中国語ページの抽出(E分野:自然言語)
- B-030 キャッシュヒント自動付加を用いたソフトウェア高速化(B分野:ソフトウェア)
- LA-003 LMNtal処理系におけるグラフ構造の操作機能の設計と実装(A分野:モデル・アルゴリズム・プログラミング)
- SATソルバzchaffのMPIによる並列化(HPC-1 : 並列プログラミング)(2004年並列/分散/協調処理に関する『青森』サマー・ワークショップ(SWoPP青森2004) : 研究会・連続同時開催)
- 言語モデルLMNtal
- 萩谷昌己,横森 貴共編 : DNAコンピュータ,培風館(2001)
- J. A. Robinson : A Machine-Oriented Logic Based on the Resolution Principle(20世紀の名著名論)
- インタフェースに基づく並行論理プログラム最適化コンパイラの構成法
- 人工知能とソフトウェア文化
- 並列KLIC処理系上での配列演算の最適化
- 並行論理プログラムのプログラム空間に関する考察
- 並行論理型言語における同期ポイント移動の安全性について
- 自己調整二分木の並列操作
- 4N-4 並行論理プログラム静的解析系Kimaの実装
- 3N-2 オブジェクト共有空間を利用した分散プログラミング支援フレームワーク
- 並行論理プログラムの参照数解析
- 静的解析と制約充足によるプログラム自動デバッグ
- 基数制約に対応するクラスタ向け並列SATソルバとその評価(高信頼設計,2011年並列/分散/協調処理に関する『鹿児島』サマー・ワークショップ(SWoPP鹿児島2011))
- 理論と実際のギャップ : 並列プログラミング (<特別論説> 情報処理最前線)
- Moded Flat GHCのモード体系
- LMNtal並列モデル検査における状態生成数削減及び高速化