Mercurial > hg > Papers > 2023 > moririn-sigos
changeset 8:2514493ae067 default tip
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 15 May 2023 18:42:52 +0900 |
| parents | cedf88ea18b9 |
| children | |
| files | fig/denotation.graffle fig/denotation.svg fig/logic-and-impl.graffle fig/logic-and-impl.svg presen.ind |
| diffstat | 5 files changed, 307 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/denotation.svg Mon May 15 18:42:52 2023 +0900 @@ -0,0 +1,154 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns:xl="http://www.w3.org/1999/xlink" xmlns="http://www.w3.org/2000/svg" viewBox="81.316 84.276 559.1417 205.724" width="559.1417" height="205.724"> + <defs> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -3 7 6" markerWidth="7" markerHeight="6" color="black"> + <g> + <path d="M 4.8 0 L 0 -1.8 L 0 1.8 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -2 4 4" markerWidth="4" markerHeight="4" color="black"> + <g> + <path d="M 1.584 0 L 0 -.594 L 0 .594 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/> + </g> + </marker> + </defs> + <g id="Canvas_1" fill-opacity="1" stroke-opacity="1" stroke-dasharray="none" fill="none" stroke="none"> + <title>Canvas 1</title> + <g id="Canvas_1_Layer_1"> + <title>Layer 1</title> + <g id="Graphic_2"> + <text transform="translate(86.316 104.5)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="3907985e-19" y="15">Specification</tspan> + </text> + </g> + <g id="Graphic_4"> + <text transform="translate(377.5 146.5)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="4369838e-19" y="15">Invariant</tspan> + </text> + </g> + <g id="Graphic_6"> + <ellipse cx="249.86258" cy="99.724" rx="15.3008842768261" ry="14.2240217519925" fill="white"/> + <ellipse cx="249.86258" cy="99.724" rx="15.3008842768261" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + <text transform="translate(242.6219 93.584)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.1256878" y="10">K1</tspan> + </text> + </g> + <g id="Graphic_7"> + <ellipse cx="215.80086" cy="150.724" rx="15.300884276826" ry="14.2240217519925" fill="white"/> + <ellipse cx="215.80086" cy="150.724" rx="15.300884276826" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + <text transform="translate(208.56017 144.584)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.1256878" y="10">K0</tspan> + </text> + </g> + <g id="Graphic_8"> + <ellipse cx="288.36258" cy="150.724" rx="15.300884276826" ry="14.2240217519925" fill="white"/> + <ellipse cx="288.36258" cy="150.724" rx="15.300884276826" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + <text transform="translate(281.1219 144.584)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.8656878" y="10">k2</tspan> + </text> + </g> + <g id="Line_9"> + <line x1="241.2334" y1="112.64433" x2="231.59467" y2="127.07622" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_10"> + <line x1="259.25724" y1="112.16888" x2="271.19565" y2="127.9834" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_11"> + <text transform="translate(302.06172 107)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="3161915e-19" y="15">k1 < k2</tspan> + </text> + </g> + <g id="Graphic_17"> + <ellipse cx="530.3626" cy="99.5" rx="15.3008842768261" ry="14.2240217519925" fill="white"/> + <ellipse cx="530.3626" cy="99.5" rx="15.3008842768261" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + <text transform="translate(523.1219 93.36)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.1256878" y="10">K1</tspan> + </text> + </g> + <g id="Graphic_16"> + <ellipse cx="496.30086" cy="150.5" rx="15.3008842768261" ry="14.2240217519925" fill="white"/> + <ellipse cx="496.30086" cy="150.5" rx="15.3008842768261" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + <text transform="translate(489.0602 144.36)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.1256878" y="10">K0</tspan> + </text> + </g> + <g id="Graphic_15"> + <ellipse cx="568.8626" cy="150.5" rx="15.3008842768262" ry="14.2240217519925" fill="white"/> + <ellipse cx="568.8626" cy="150.5" rx="15.3008842768262" ry="14.2240217519925" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + <text transform="translate(561.6219 144.36)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="10" fill="black" x="1.8656878" y="10">k2</tspan> + </text> + </g> + <g id="Line_14"> + <line x1="521.7334" y1="112.42033" x2="512.09467" y2="126.85222" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_13"> + <line x1="539.75724" y1="111.94488" x2="551.69565" y2="127.7594" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_12"> + <text transform="translate(582.5617 106.776)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="3161915e-19" y="15">k1 < k2</tspan> + </text> + </g> + <g id="Graphic_21"> + <path d="M 387 130.25 L 387 119.75 L 406.6017 119.75 L 406.6017 114.5 L 417.6017 125 L 406.6017 135.5 L 406.6017 130.25 Z" fill="white"/> + <path d="M 387 130.25 L 387 119.75 L 406.6017 119.75 L 406.6017 114.5 L 417.6017 125 L 406.6017 135.5 L 406.6017 130.25 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Group_40"> + <g id="Graphic_38"> + <rect x="206.06663" y="198" width="244.88618" height="91" fill="white"/> + <rect x="206.06663" y="198" width="244.88618" height="91" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_27"> + <ellipse cx="255.32134" cy="220.3056" rx="7.54677761079227" ry="7.01564216493942" fill="white"/> + <ellipse cx="255.32134" cy="220.3056" rx="7.54677761079227" ry="7.01564216493942" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_26"> + <ellipse cx="238.52125" cy="245.46008" rx="7.54677761079225" ry="7.01564216493943" fill="white"/> + <ellipse cx="238.52125" cy="245.46008" rx="7.54677761079225" ry="7.01564216493943" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_25"> + <ellipse cx="274.3105" cy="245.46008" rx="7.54677761079228" ry="7.01564216493943" fill="white"/> + <ellipse cx="274.3105" cy="245.46008" rx="7.54677761079228" ry="7.01564216493943" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_24"> + <line x1="250.78322" y1="227.10045" x2="246.65168" y2="233.28653" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_23"> + <line x1="260.26097" y1="226.849" x2="265.4739" y2="233.75445" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_32"> + <ellipse cx="326.89984" cy="220.3056" rx="7.54677761079227" ry="7.01564216493942" fill="white"/> + <ellipse cx="326.89984" cy="220.3056" rx="7.54677761079227" ry="7.01564216493942" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_31"> + <ellipse cx="310.09975" cy="245.46008" rx="7.54677761079224" ry="7.01564216493943" fill="white"/> + <ellipse cx="310.09975" cy="245.46008" rx="7.54677761079224" ry="7.01564216493943" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_30"> + <ellipse cx="345.889" cy="245.46008" rx="7.54677761079227" ry="7.01564216493943" fill="white"/> + <ellipse cx="345.889" cy="245.46008" rx="7.54677761079227" ry="7.01564216493943" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_29"> + <line x1="322.36172" y1="227.10045" x2="318.23018" y2="233.28653" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_28"> + <line x1="331.83947" y1="226.849" x2="337.0524" y2="233.75445" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_34"> + <ellipse cx="364.87816" cy="270.61455" rx="7.54677761079224" ry="7.0156421649394" fill="white"/> + <ellipse cx="364.87816" cy="270.61455" rx="7.54677761079224" ry="7.0156421649394" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_36"> + <line x1="350.82863" y1="252.00347" x2="356.04156" y2="258.90892" marker-end="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + </g> + <g id="Graphic_39"> + <text transform="translate(93.564 173)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="8029133e-19" y="15">Denotation</tspan> + </text> + </g> + </g> + </g> +</svg>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/fig/logic-and-impl.svg Mon May 15 18:42:52 2023 +0900 @@ -0,0 +1,79 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd"> +<svg xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns:xl="http://www.w3.org/1999/xlink" xmlns="http://www.w3.org/2000/svg" viewBox="25.56 100 390.44 217" width="390.44" height="217"> + <defs/> + <g id="Canvas_1" fill-opacity="1" stroke-opacity="1" stroke-dasharray="none" fill="none" stroke="none"> + <title>Canvas 1</title> + <g id="Canvas_1_Layer_1"> + <title>Layer 1</title> + <g id="Graphic_2"> + <text transform="translate(51 105)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="0" y="15">Logic</tspan> + </text> + </g> + <g id="Graphic_3"> + <text transform="translate(381 105)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="0" y="15">C</tspan> + </text> + </g> + <g id="Line_5"> + <line x1="42" y1="138" x2="111.5" y2="138" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_6"> + <line x1="42" y1="315" x2="415" y2="315" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_7"> + <line x1="345.5" y1="138" x2="415" y2="138" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_8"> + <text transform="translate(164.454 109.99998)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="16" fill="black" x="0" y="14">越えられない壁</tspan> + </text> + </g> + <g id="Line_9"> + <line x1="185.704" y1="139" x2="255.204" y2="139" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="8.0,8.0" stroke-width="2"/> + </g> + <g id="Graphic_21"> + <text transform="translate(51 193.5)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="0" y="15">Logic</tspan> + </text> + </g> + <g id="Graphic_20"> + <text transform="translate(381 193.5)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="0" y="15">C</tspan> + </text> + </g> + <g id="Line_19"> + <line x1="42" y1="226.5" x2="111.5" y2="226.5" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_18"> + <line x1="345.5" y1="226.5" x2="415" y2="226.5" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Graphic_17"> + <text transform="translate(163.91 183.5)" fill="black"> + <tspan font-family="Hiragino Sans" font-size="16" fill="black" x="2.664" y="14">Pure function </tspan> + <tspan font-family="Hiragino Sans" font-size="16" fill="black" x="25.768" y="38.000016">languae</tspan> + </text> + </g> + <g id="Line_16"> + <line x1="185.704" y1="227.5" x2="255.204" y2="227.5" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="2"/> + </g> + <g id="Line_23"> + <line x1="120.77808" y1="227.5" x2="183.77808" y2="227.5" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="8.0,8.0" stroke-width="2"/> + </g> + <g id="Line_24"> + <line x1="265.77808" y1="227.5" x2="335.27808" y2="227.5" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="8.0,8.0" stroke-width="2"/> + </g> + <g id="Graphic_32"> + <text transform="translate(30.56 274.5)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="2344791e-19" y="15">GearsAgda</tspan> + </text> + </g> + <g id="Graphic_31"> + <text transform="translate(370.48 274.5)" fill="black"> + <tspan font-family="Helvetica Neue" font-size="16" fill="black" x="27711167e-20" y="15">CbC</tspan> + </text> + </g> + </g> + </g> +</svg>
--- a/presen.ind Sat May 13 16:14:11 2023 +0900 +++ b/presen.ind Mon May 15 18:42:52 2023 +0900 @@ -1,17 +1,60 @@ -title: GearsAgdaによる Red Black Tree の検証 --author: 森逸汰 河野真治 +-author: 森逸汰 河野真治 琉球大学工学部 --証明を用いたOSのアプリケーションの信頼性の保証 - 信頼性は全体的な問題 + 信頼性は全体的な問題 - テストでは限界がある + テストでは限界がある(たとえばrace condition) 記述単位を工夫して、証明しやすくする Gears OS と GearsAgda を使う + +--CbC はそもそも debug しづらい + + stack trace がない + 既存のdebugger は無力 + Unit Test は codeGear 単位 + Automaton に近い + + 別なプログラミング手法が必要 + むしろ、証明とモデル検査相性が良い + + 人に対する読みやすさよりも検証しやすいことを選択 + +--仕様と実装の距離 + +証明は仕様を直接使わずに Invariant を使う + + CbC は実装 + GearsAgda はCbCと平行 + Invariant と仕様の記述は GearsAgda + +通常は、C++/Javaなどの実装の他に別な関数型言語を使う + +<center><img src="fig/logic-and-impl.svg"></center> + +--Specification / Invariant / Denotational Semantics + + Specification relation among data structure + Invariant Spec is unchanged in the loop + Denotational all possible sound data strucutre + +<center><img src="fig/denotation.svg"></center> + +--関数呼び出しの環境が証明やモデル検査には邪魔 + +stack が無駄にモデル検査の探索空間を大きくしてしまう + +普通のプログラムでも関数呼び出しは30段近い + +stack 上に構築するデータ構造のinvariantが必要 + +メモリ使用量と計算が入り混じってしまう + --とりあえずの例題 簡単な while program @@ -31,7 +74,7 @@ metaGear メタ計算(計算の実装、メモリ、CPU、IO)などの記述 context プロセスに相当する codeGear を実行する環境 - CbC Continuation based C 以上を実装する言語 + CbC Continuation based C を実装する言語 --GearsAgda @@ -40,8 +83,8 @@ Agda Pure Functional Language - Curry Howard Isomorphism - dependent types + Curry Howard Isomorphism 証明記述に対応する + dependent types 型を変数に代入できる ZF Set theory も使える (Fairness とか、実数とか) @@ -169,6 +212,8 @@ Sound and complete が Command 依存 証明方法が限定的 +<center><img src="fig/denotation.svg"></center> + --GearsAgda での記述 Command ではなく codeGear をそのまま使える @@ -200,6 +245,12 @@ ? でさぼっても良い (証明をさぼっても、プログラムは動作する +--証明はメタ計算 + +元の codeGear に invariant や condition を meta 計算として追加している + +<center><img src="fig/meta_cg_dg.svg"></center> + --Haskell でやれば? Haskell の方が証明との相性は良い @@ -274,6 +325,18 @@ ここから必要な性質は全部証明できる +--Invariant と仕様の違い + +Invariant あるいは表示的意味論は、ぜんぶを正確に含んでいる + +仕様は、それが満たす性質の一部 + +仕様を列挙しても Invariant に自動的になったりしない + +仕様と実現性は関係しない + +Invariant は実装と密接な関係があるが、実装を保証しない + --Red Black Tree の invariant (leaf / single ) data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → (bd : ℕ) → Set n where @@ -361,6 +424,9 @@ 共有は scheduler level のmetaGearで処理される +<center><img src="fig/model_checking.svg"></center> + + -- Concurrency で証明したいこと redBlackTree の transaction @@ -375,6 +441,8 @@ invariant が決まれば、証明は割と機械的 (AI support?) +--まとめ + @@ -389,5 +457,3 @@ - -