ソフトウェア動的更新の理論に ついて 産総研 橋本政朋 動機 • ユビキタスコンピューティング時代の本格到来 もそう遠くなさそう – マイクロサーバが至る所に存在 • ソフトのバグは加算無限個存在 • 機能拡張も必須 • サービスを停めたくない • 動的更新とは何なのか？ • どのような動的更新が安全なのか？ ユビキタスな世界 It needs: •的確な状況把握 •位置追跡 •予定表との連携 •プロファイリング どこに 行け ば？ •整備された情報インフラ •環境埋込小型サーバ •サービス間のシームレスな接続 （Web,プロファイル情報,etc.） ．．． Direct! 乗換案内 小型サーバ 位置追跡 位置追跡 検査項目 尿検査 心電図 血液検査 文献 • D.Gupta, P.Jalote, and G.Barua. A Formal Framework for On-line Software Version Change. IEEE Transaction on Software Engineering, Vol.22 No.2, pp. 120-131, 1996. • D.Gupta. On-line Software Version Change. PhD thesis, Dept. CSE, IIT Kanpur, June 1995. Plan • 一般更新モデル – 更新の妥当性 • 更新妥当性の決定不能性 – シンプルプログラムモデル – 定理：更新の妥当性の検証は決定不能 • 妥当性が決定可能な動的更新 – 妥当な更新の構成法 • プログラムモデルの拡張 一般更新モデル • あるプログラムCからC’への更新 • C，C’それぞれは“正しい”と仮定 • 実行状態の変換はプログラマが与える プロセス プログラム 入力 C SC0 C C S1 C Sn Si 状態 プロセス •各Cに対しSC0（初期状態）を唯一定める •SC0からある時点，ある入力列によってとりうる状態は 到達可能 動的更新 プログラム 入力 C C S1 SC0 C Si 状態 更新 プロセス 状態変換 C’ T(Si) Points • 即時的変更 – インクリメンタルな変更はその組み合わせで 表現可能 • 状態変換はユーザが定義する – 妥当性を決するのはタイミング 更新の妥当性 C C C C S1 SC0 Sn Si 更新 C’ C’ SC’0 T(Si) 有限ステップで 新プログラムの 到達可能な状 態に達するとき 妥当 更新妥当性の決定不能性 シンプルなプログラムモデルの導入 妥当性の決定不能性 より複雑なプログラムモデルででも決定不能 シンプルプログラムモデル • 命令型言語の単純版（関数，手続きなし） – プログラムはステートメントの列 • プログラムCに含まれる変数の集合をV（C） • プログラムCの状態SCは変数（V（C）⋃｛PC｝） から適当な値（⊥含む）への写像 • SC0は， SC0（v）=⊥（∀v∈V（C）） SC0（PC）=First（C） 決定不能性 SがCの到達可能な状態であるような任意のC，C’，T，Sに ついて，SにおけるTを用いたCからC’への動的更新が妥当 であるかどうかは決定不能 C C SC0 S C’ T(S) C’ SC’0 任意のプログラムC に対し，SC（PC）=Last（C）+1であるような 状態SCが到達可能であるかどうかは決定不能 (停止問題) 妥当性が決定可能な動的更新 状態変換TCC’を制限 – 恒等変換，変数追加，変数名変更，のみ扱う – ＋変域（状態）も制限 • 実質，更新タイミング（更新可能状態）の制限 • PCのみ制限 ←実用上の問題 TCC’は（KT，N）という形 CのPC値からC’のPC値への写像 変数名変換 まだ決定不能！ やりたいこと • 妥当性のための十分条件を求める 計算可能 十分条件 妥当 ステートメント実行毎にチェック 算出したPC値のときのみ更新を起こす 全ては算出不能 十分条件 SにおけるCからC’へのTを用いた更新が妥当 ⇑ ∃S’’ s.t. C’で到達可能かつS’’（PC）=S’（=T（S））（PC）かつ ∀x∈V（C’），x使用前に再定義される，または S’（x）= S’’（x） •V1：更新後使用されるまでに再定義される変数 •V2：更新後そのままでOKな変数 C C SC0 S V1 A1 V2 A2 PC K C’ T(S) C’ SC’0 C’ ∃ S’’ V1 A’1 V2 A2 PC K 更新ポイントの選定 • 更新前プログラムCの各コントロールポイントに おいてV1とV2を見付ける – 見付けきるアルゴリズムは存在しない – データフロー解析活用で近似 • V1⋃V2=V（C’）となるコントロールポイントを選ぶ 例：階乗計算プログラム 入力nを読み，階乗を計算出力するループ ｛i,n,p｝ ｛i,n,p｝ ｛i,p｝ ｛i,p｝ S1 while true do read n; S’1.1 read n; S1.2 if n < 0 then S’1.2 if n < 0 then S1.2.1 write “error” else S’1.2.1 write “error” else begin S1.2.2 if n = 0 then S’1.2.2 i ← 1; S1.2.2.1 write 1 else begin S’1.2.3 p ← 1; S’1.2.4 while i ≤ n do S1.2.2.2 i ← 1; S’1.2.4.1 S1.2.2.3 p ← 1; S’1.2.4.2 S1.2.2.4 while i ≤ n do S1.2.2.4.1 S1.2.2.4.2 S1.2.2.5 ｛i,n,p｝ while true do S1.1 ｛i,p｝ V1 S’1 p ← p * i; i←i+1 done write p end done Version 1 （C） S’1.2.5 p ← p * i; i←i+1 done write p end done Version 2 （C’） V =｛n｝ 2 V1 ⋃ V2=｛i,n,p｝=V（C）=V（C’） より一般的なプログラムモデル • 関数，手続の導入 • 更新を関数単位として妥当性を再検討 – – – – 関数間DFAは高くつく 呼び出し中の関数は更新しない 大域変数しか変更しない 関数集合Fのどの関数も呼び出し中でないと きの更新が妥当であるようなFを求める 更新される関数が全て functional enhancementなら それらがFをなす まとめと課題 • 動的更新の定式化 – 更新妥当性 • 更新妥当性の決定不能性の証明 • 安全な更新の構成 – シンプルケース（関数，手続なし） – CやPascal 程度ケース • 更新に対する実用的な制限とは？ • 実時間性は扱っていない
© Copyright 2024 ExpyDoc
