ソフトウェア動的更新の理論について 産総研 橋本政朋

動機 ユビキタスコンピューティング時代の本格到来もそう遠くなさそう ソフトのバグは加算無限個存在 機能拡張も必須 サービスを停めたくない マイクロサーバが至る所に存在 ソフトのバグは加算無限個存在 機能拡張も必須 サービスを停めたくない 動的更新とは何なのか？ どのような動的更新が安全なのか？

ユビキタスな世界 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（初期状態）を唯一定める SC0からある時点，ある入力列によってとりうる状態は 到達可能 入力 プログラム C C Sn C S1 C SC0 C Si 状態 プロセス 各Cに対しSC0（初期状態）を唯一定める SC0からある時点，ある入力列によってとりうる状態は 到達可能

動的更新 入力 プログラム C S1 C SC0 C Si 状態 更新 プロセス C’ T(Si) 状態変換

Points 即時的変更 インクリメンタルな変更はその組み合わせで表現可能 状態変換はユーザが定義する 妥当性を決するのはタイミング

更新の妥当性 C Sn C S1 C SC0 C Si 更新 有限ステップで 新プログラムの到達可能な状態に達するとき妥当 C’ SC’0 T(Si)

更新妥当性の決定不能性 シンプルなプログラムモデルの導入 妥当性の決定不能性 より複雑なプログラムモデルででも決定不能

シンプルプログラムモデル 命令型言語の単純版（関数，手続きなし） プログラムCに含まれる変数の集合をV（C） プログラムはステートメントの列 プログラム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 SC0 C S C’ T(S) C’ SC’0 任意のプログラムC に対し，SC（PC）=Last（C）+1であるような 状態SCが到達可能であるかどうかは決定不能　(停止問題)

妥当性が決定可能な動的更新 状態変換TCC’を制限 恒等変換，変数追加，変数名変更，のみ扱う ＋変域（状態）も制限 実質，更新タイミング（更新可能状態）の制限 PCのみ制限　←実用上の問題 まだ決定不能！ 変数名変換 CのPC値からC’のPC値への写像 TCC’は（KT，N）という形

やりたいこと 妥当性のための十分条件を求める 計算可能 妥当 十分条件 ステートメント実行毎にチェック 算出した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な変数 V1 A1 V2 A2 PC K C SC0 C S C’ T(S) V1 A’1 V2 A2 PC K C’ SC’0 C’ S’’ ∃

更新ポイントの選定 更新前プログラムCの各コントロールポイントにおいてV1とV2を見付ける 見付けきるアルゴリズムは存在しない データフロー解析活用で近似 V1⋃V2=V（C’）となるコントロールポイントを選ぶ

例：階乗計算プログラム 入力nを読み，階乗を計算出力するループ

V1 ⋃ V2=｛i,n,p｝=V（C）=V（C’） Version 1 （C） while true do S’1 S1.1 read n; S’1.1 S1.2 if n < 0 then S’1.2 S1.2.1 write “error” else S’1.2.1 else begin S1.2.2 if n = 0 then S’1.2.2 i ← 1; S1.2.2.1 write 1 S’1.2.3 p ← 1; S’1.2.4 while i ≤ n do S1.2.2.2 S’1.2.4.1 p ← p * i; S1.2.2.3 S’1.2.4.2 i ← i + 1 done S1.2.2.4 S1.2.2.4.1 S’1.2.5 write p end S1.2.2.4.2 S1.2.2.5 ｛i,n,p｝ ｛i,p｝ ｛i,p｝ ｛i,p｝ V1 Version 2 （C’） V2=｛n｝ ｛i,n,p｝ V1 ⋃ V2=｛i,n,p｝=V（C）=V（C’） Version 1 （C）

より一般的なプログラムモデル 関数，手続の導入 更新を関数単位として妥当性を再検討 関数間DFAは高くつく 呼び出し中の関数は更新しない 大域変数しか変更しない 関数集合Fのどの関数も呼び出し中でないときの更新が妥当であるようなFを求める 更新される関数が全てfunctional enhancementならそれらがFをなす

まとめと課題 動的更新の定式化 更新妥当性の決定不能性の証明 安全な更新の構成 更新に対する実用的な制限とは？ 実時間性は扱っていない シンプルケース（関数，手続なし） CやPascal 程度ケース 更新に対する実用的な制限とは？ 実時間性は扱っていない