Download presentation
Presentation is loading. Please wait.
1
ソフトウェア動的更新の理論について 産総研 橋本政朋
2
動機 ユビキタスコンピューティング時代の本格到来もそう遠くなさそう ソフトのバグは加算無限個存在 機能拡張も必須 サービスを停めたくない
マイクロサーバが至る所に存在 ソフトのバグは加算無限個存在 機能拡張も必須 サービスを停めたくない 動的更新とは何なのか？ どのような動的更新が安全なのか？
3
ユビキタスな世界 It needs: 的確な状況把握 時刻表 整備された情報インフラ 位置追跡 予定表との連携 プロファイリング
環境埋込小型サーバ サービス間のシームレスな接続 （Web,プロファイル情報,etc.） ．．． どこに行けば？ 検査項目尿検査 心電図 血液検査 Direct! 小型サーバ 乗換案内 位置追跡 「右に曲がってください」 スケジュール スケジュール 位置追跡
4
文献 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 , 1996. D.Gupta. On-line Software Version Change. PhD thesis, Dept. CSE, IIT Kanpur, June 1995.
5
Plan 一般更新モデル 更新妥当性の決定不能性 妥当性が決定可能な動的更新 プログラムモデルの拡張 更新の妥当性 シンプルプログラムモデル
定理：更新の妥当性の検証は決定不能 妥当性が決定可能な動的更新 妥当な更新の構成法 プログラムモデルの拡張
6
一般更新モデル あるプログラムCからC’への更新 C，C’それぞれは“正しい”と仮定 実行状態の変換はプログラマが与える
7
プロセス 各Cに対しSC0（初期状態）を唯一定める SC0からある時点，ある入力列によってとりうる状態は 到達可能 入力 プログラム C C
Sn C S1 C SC0 C Si 状態 プロセス 各Cに対しSC0（初期状態）を唯一定める SC0からある時点，ある入力列によってとりうる状態は 到達可能
8
動的更新 入力 プログラム C S1 C SC0 C Si 状態 更新 プロセス C’ T(Si) 状態変換
9
Points 即時的変更 インクリメンタルな変更はその組み合わせで表現可能 状態変換はユーザが定義する 妥当性を決するのはタイミング
10
更新の妥当性 C Sn C S1 C SC0 C Si 更新 有限ステップで 新プログラムの到達可能な状態に達するとき妥当 C’ SC’0
T(Si)
11
更新妥当性の決定不能性 シンプルなプログラムモデルの導入 妥当性の決定不能性 より複雑なプログラムモデルででも決定不能
12
シンプルプログラムモデル 命令型言語の単純版（関数，手続きなし） プログラムCに含まれる変数の集合をV（C）
プログラムはステートメントの列 プログラムCに含まれる変数の集合をV（C） プログラムCの状態SCは変数（V（C）⋃｛PC｝）から適当な値（⊥含む）への写像 SC0は， SC0（v）=⊥（∀v∈V（C）） SC0（PC）=First（C）
13
決定不能性 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が到達可能であるかどうかは決定不能 (停止問題)
14
妥当性が決定可能な動的更新 状態変換TCC’を制限 恒等変換，変数追加，変数名変更，のみ扱う ＋変域（状態）も制限
実質，更新タイミング（更新可能状態）の制限 PCのみ制限 ←実用上の問題 まだ決定不能！ 変数名変換 CのPC値からC’のPC値への写像 TCC’は（KT，N）という形
15
やりたいこと 妥当性のための十分条件を求める 計算可能 妥当 十分条件 ステートメント実行毎にチェック 算出したPC値のときのみ更新を起こす
全ては算出不能
16
十分条件 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’’ ∃
17
更新ポイントの選定 更新前プログラムCの各コントロールポイントにおいてV1とV2を見付ける
見付けきるアルゴリズムは存在しない データフロー解析活用で近似 V1⋃V2=V（C’）となるコントロールポイントを選ぶ
18
例：階乗計算プログラム 入力nを読み，階乗を計算出力するループ
19
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; S write 1 S’1.2.3 p ← 1; S’1.2.4 while i ≤ n do S S’ p ← p * i; S S’ i ← i + 1 done S S S’1.2.5 write p end S S ｛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）
20
より一般的なプログラムモデル 関数，手続の導入 更新を関数単位として妥当性を再検討 関数間DFAは高くつく 呼び出し中の関数は更新しない
大域変数しか変更しない 関数集合Fのどの関数も呼び出し中でないときの更新が妥当であるようなFを求める 更新される関数が全てfunctional enhancementならそれらがFをなす
21
まとめと課題 動的更新の定式化 更新妥当性の決定不能性の証明 安全な更新の構成 更新に対する実用的な制限とは？ 実時間性は扱っていない
シンプルケース（関数，手続なし） CやPascal 程度ケース 更新に対する実用的な制限とは？ 実時間性は扱っていない
Similar presentations
