# HG changeset patch # User Yasutaka Higa # Date 1470301862 -32400 # Node ID fa1d602b1676525931e8f7ff0b5c08155a040378 # Parent 02e5ae71c3198aa34dca9cbc450a1301b84eabb8 Add rbtree image diff -r 02e5ae71c319 -r fa1d602b1676 presentation/images/code_segments.graffle --- a/presentation/images/code_segments.graffle Wed Aug 03 17:53:25 2016 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,601 +0,0 @@ - - - - - ActiveLayerIndex - 0 - ApplicationVersion - - com.omnigroup.OmniGraffle6 - 169.17.0.263360 - - AutoAdjust - - BackgroundGraphic - - Bounds - {{0, 0}, {559, 783}} - Class - SolidGraphic - ID - 2 - Style - - stroke - - Draws - NO - - - - BaseZoom - 0 - CanvasOrigin - {0, 0} - ColumnAlign - 1 - ColumnSpacing - 36 - CreationDate - 2012-02-05 20:00:27 +0000 - Creator - Kazuki AKAMINE - DisplayScale - 1 in = 1 in - GraphDocumentVersion - 12 - GraphicsList - - - AllowLabelDrop - - Class - LineGraphic - Head - - ID - 44 - - ID - 45 - Points - - {227.05808893202135, 162.32628729047525} - {274.00441106797865, 156.04871270952472} - - Style - - shadow - - Draws - NO - - stroke - - HeadArrow - FilledArrow - HeadScale - 1.4285709857940674 - Legacy - - TailArrow - 0 - TailScale - 0.5 - - - Tail - - ID - 33 - - - - Bounds - {{274.5, 125.5}, {82, 50}} - Class - ShapedGraphic - ID - 44 - Style - - shadow - - Draws - NO - - - Text - - Text - {\rtf1\ansi\ansicpg1252\cocoartf1348\cocoasubrtf170 -{\fonttbl\f0\fswiss\fcharset0 Helvetica;} -{\colortbl;\red255\green255\blue255;} -\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc - -\f0\fs24 \cf0 Code\ -Segment} - - - - AllowLabelDrop - - Class - LineGraphic - ID - 42 - Points - - {227.04657487753181, 43.603137424407386} - {274.5, 55.875} - - Style - - shadow - - Draws - NO - - stroke - - HeadArrow - FilledArrow - HeadScale - 1.4285709857940674 - Legacy - - TailArrow - 0 - TailScale - 0.5 - - - Tail - - ID - 30 - - - - Bounds - {{274.5, 31.5}, {82, 50}} - Class - ShapedGraphic - ID - 41 - Style - - shadow - - Draws - NO - - - Text - - Text - {\rtf1\ansi\ansicpg1252\cocoartf1348\cocoasubrtf170 -{\fonttbl\f0\fswiss\fcharset0 Helvetica;} -{\colortbl;\red255\green255\blue255;} -\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc - -\f0\fs24 \cf0 Code\ -Segment} - - - - AllowLabelDrop - - Class - LineGraphic - Head - - ID - 38 - - ID - 40 - Points - - {97.098722833775156, 70.504114203612403} - {144.08877716622484, 86.370885796387611} - - Style - - shadow - - Draws - NO - - stroke - - HeadArrow - FilledArrow - HeadScale - 1.4285709857940674 - Legacy - - TailArrow - 0 - TailScale - 0.5 - - - Tail - - ID - 15 - - - - AllowLabelDrop - - Class - LineGraphic - Head - - ID - 33 - - ID - 39 - Points - - {97.120588932021334, 156.04871270952475} - {144.06691106797865, 162.32628729047528} - - Style - - shadow - - Draws - NO - - stroke - - HeadArrow - FilledArrow - HeadScale - 1.4285709857940674 - Legacy - - TailArrow - 0 - TailScale - 0.5 - - - Tail - - ID - 17 - - - - Bounds - {{144.5625, 75.375}, {82, 50}} - Class - ShapedGraphic - ID - 38 - Style - - shadow - - Draws - NO - - - Text - - Text - {\rtf1\ansi\ansicpg1252\cocoartf1348\cocoasubrtf170 -{\fonttbl\f0\fswiss\fcharset0 Helvetica;} -{\colortbl;\red255\green255\blue255;} -\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc - -\f0\fs24 \cf0 Code\ -Segment} - - - - AllowLabelDrop - - Class - LineGraphic - Head - - ID - 30 - - ID - 37 - Points - - {96.625, 58.5} - {144.08204500032224, 44.826501440525568} - - Style - - shadow - - Draws - NO - - stroke - - HeadArrow - FilledArrow - HeadScale - 1.4285709857940674 - Legacy - - TailArrow - 0 - TailScale - 0.5 - - - - - Bounds - {{144.5625, 142.875}, {82, 50}} - Class - ShapedGraphic - ID - 33 - Style - - shadow - - Draws - NO - - - Text - - Text - {\rtf1\ansi\ansicpg1252\cocoartf1348\cocoasubrtf170 -{\fonttbl\f0\fswiss\fcharset0 Helvetica;} -{\colortbl;\red255\green255\blue255;} -\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc - -\f0\fs24 \cf0 Code\ -Segment} - - - - Bounds - {{144.5625, 7.875}, {82, 50}} - Class - ShapedGraphic - ID - 30 - Style - - shadow - - Draws - NO - - - Text - - Text - {\rtf1\ansi\ansicpg1252\cocoartf1348\cocoasubrtf170 -{\fonttbl\f0\fswiss\fcharset0 Helvetica;} -{\colortbl;\red255\green255\blue255;} -\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc - -\f0\fs24 \cf0 Code\ -Segment} - - - - Bounds - {{14.625, 125.5}, {82, 50}} - Class - ShapedGraphic - ID - 17 - Style - - shadow - - Draws - NO - - - Text - - Text - {\rtf1\ansi\ansicpg1252\cocoartf1348\cocoasubrtf170 -{\fonttbl\f0\fswiss\fcharset0 Helvetica;} -{\colortbl;\red255\green255\blue255;} -\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc - -\f0\fs24 \cf0 Code\ -Segment} - - - - Bounds - {{14.625, 31.5}, {82, 50}} - Class - ShapedGraphic - ID - 15 - Style - - shadow - - Draws - NO - - - Text - - Text - {\rtf1\ansi\ansicpg1252\cocoartf1348\cocoasubrtf170 -{\fonttbl\f0\fswiss\fcharset0 Helvetica;} -{\colortbl;\red255\green255\blue255;} -\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\qc - -\f0\fs24 \cf0 Code\ -Segment} - - - - GridInfo - - GuidesLocked - NO - GuidesVisible - YES - HPages - 1 - ImageCounter - 1 - KeepToScale - - Layers - - - Lock - NO - Name - レイヤー 1 - Print - YES - Slices - NO - View - YES - - - LayoutInfo - - Animate - NO - circoMinDist - 18 - circoSeparation - 0.0 - layoutEngine - dot - neatoLineLength - 0.20000000298023224 - neatoSeparation - 0.0 - twopiSeparation - 0.0 - - LinksVisible - NO - MagnetsVisible - NO - MasterSheets - - ModificationDate - 2016-08-02 07:48:28 +0000 - Modifier - atton - NotesVisible - NO - Orientation - 2 - OriginVisible - NO - PageBreaks - YES - PrintInfo - - NSBottomMargin - - float - 41 - - NSHorizonalPagination - - coded - BAtzdHJlYW10eXBlZIHoA4QBQISEhAhOU051bWJlcgCEhAdOU1ZhbHVlAISECE5TT2JqZWN0AIWEASqEhAFxlwCG - - NSLeftMargin - - float - 18 - - NSPaperSize - - size - {595, 842} - - NSPrintReverseOrientation - - coded - BAtzdHJlYW10eXBlZIHoA4QBQISEhAhOU051bWJlcgCEhAdOU1ZhbHVlAISECE5TT2JqZWN0AIWEASqEhAFxlwCG - - NSRightMargin - - float - 18 - - NSTopMargin - - float - 18 - - - PrintOnePage - - ReadOnly - NO - RowAlign - 1 - RowSpacing - 36 - SheetTitle - キャンバス 1 - SmartAlignmentGuidesActive - YES - SmartDistanceGuidesActive - YES - UniqueID - 1 - UseEntirePage - - VPages - 1 - WindowInfo - - CurrentSheet - 0 - Expanded_Canvases - - Frame - {{110, 115}, {1449, 937}} - ShowInfo - - ShowRuler - - Sidebar - - SidebarWidth - 200 - TopSlabHeight - 250 - VisibleRegion - {{-64, 0}, {687.50000000000011, 573.52941176470597}} - Zoom - 1.3599999999999999 - ZoomValues - - - キャンバス 1 - 1.3599999999999999 - 1.3500000000000001 - - - - - diff -r 02e5ae71c319 -r fa1d602b1676 presentation/images/code_segments.pdf Binary file presentation/images/code_segments.pdf has changed diff -r 02e5ae71c319 -r fa1d602b1676 presentation/images/code_segments.svg --- a/presentation/images/code_segments.svg Wed Aug 03 17:53:25 2016 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,217 +0,0 @@ - - diff -r 02e5ae71c319 -r fa1d602b1676 presentation/images/rbtree.graffle Binary file presentation/images/rbtree.graffle has changed diff -r 02e5ae71c319 -r fa1d602b1676 presentation/images/rbtree.pdf Binary file presentation/images/rbtree.pdf has changed diff -r 02e5ae71c319 -r fa1d602b1676 presentation/images/rbtree.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/presentation/images/rbtree.svg Thu Aug 04 18:11:02 2016 +0900 @@ -0,0 +1,103 @@ + + diff -r 02e5ae71c319 -r fa1d602b1676 presentation/slide.md --- a/presentation/slide.md Wed Aug 03 17:53:25 2016 +0900 +++ b/presentation/slide.md Thu Aug 04 18:11:02 2016 +0900 @@ -17,6 +17,8 @@ * 検証の計算システムで実行する(メタ計算) * Java Path Finder, Valgrind * 大規模システムは実行できない + +# ソフトウェアの信頼性向上手法 * アルゴリズムの正しさを証明する * Agda, Coq, Idris といった証明支援系でプログラムを記述する * 極めて難しい @@ -77,6 +79,7 @@ # CbC のメタ計算の実際 * プログラムで使用する Data Segment は Meta Data Segment で全て定義されている + ``` union Data { struct Count { @@ -94,8 +97,10 @@ }; ``` +# CbC のメタ計算の実際 * Meta Code Segment では Data Segment は struct Data という形で一様に処理される * メタ計算と通常の計算は stub と meta によって接続される + ``` __code addTen_stub(struct Context* context) { goto addTen(context, context->data[Count]); @@ -117,6 +122,7 @@ } ``` +# CbC のメタ計算の実際 * デフォルトの meta * meta を変更することで平行計算や例外処理やソフトウェア検証を行なう @@ -185,63 +191,60 @@ * 赤ノードは2つの黒ノードを子として持つ(よって赤ノードが続くことはない) * ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である * 仕様: 最も長い経路は最も短い経路の高々2倍に収まる -* todo 図を入れておこう -# Verification of Red-Black Tree -* どのような順番で要素が挿入されても常に仕様が満たされることを確認する -* 仕様を満たさないような挿入順番があればそれを表示する -* 木への挿入は有限の個数だけ行なわれる +![rbtree](./images/rbtree.svg){:width="35%"} # Verification Library Akasha * 本研究で作成した検証用メタ計算ライブラリ -* 実装コードの ``meta`` を上書きするだけで検証を行なうことができる -* 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙 -* 挿入後の木はきちんとバランスしているかチェックする -* Meta Data Segment に挿入順番や実行履歴を記憶させる +* 実装コードの `meta` を上書きするだけで検証を行なうことができる +* どのような順番で要素が挿入されても常に仕様が満たされることを確認する +* 仕様を満たさない挿入順番があればそれを表示 + * 深さ優先探索で有限個の要素の挿入順番を総当たりで列挙 + * 挿入後の木はきちんとバランスしているかチェックする +* CbC のメタ計算 Akasha では要素数13個までチェックできた +* 実装にわざとバグを入れた場合にはバランスしていない入力例を返した # C Bounded Model Checker -* Carnegie Mellon University で開発されている ANSI-C の記号実行モデルチェッカ +* Carnegie Mellon University で開発されている記号実行モデルチェッカ + * C, C++, Java に対応 * CbC は `__code` を `void` に、`goto` を `return` に変えると C Syntaxになる -* Red-Black Tree を C に変換して検証 + * コードを C に変換して検証 * 挿入順番は非決定的な入力 `nondet_int` を使う +* 関数呼び出しやループは展開される + * 展開可能な最大数まで展開しても赤黒木の仕様を検証できず -# Result of Verification -* CbC のメタ計算 Akasha では要素数13個までチェックできた -* CBMC ではチェックできなかった - -| | akasha | CBMC | -|----------------------------------|:------:|:----:| -| 要素数1個までは仕様を保証 | 可 | 不可 | -| 要素数13個までは仕様を保証 | 可 | 不可 | -| 実装にバグを入れた際に反例を表示 | 可 | 不可 | - +# Conclusion +* 動作するプログラムの記述を変更せず検証を行なえた + * テストケースの自動生成+仕様の反例表示ができた +* CBMC では検証できない範囲の検証を行なうことができた + * 総当たりでチェックしているため # Comparison of tools -| | akasha | cbmc | unit test | Spin | 証明 | JavaPathFinder | valgrind | +| | akasha | cbmc | unit test | Spin | 証明 | JavaPathFinder | valgrind | |------------------------|:----------:|:--------------:|:----------:|:------------:|:------------:|:---------------:|:--------:| -| 検証用に実装の変更 | 必要なし | 必要なし | 必要なし | 必要 | 必要なし | 必要なし | 必要なし | +| 検証用に実装の変更 | 必要なし | 必要なし | 必要なし | 別に記述 | 別に記述 | 必要なし | 必要なし | | 検証用に記述する言語 | 実装と同じ | 実装とほぼ同じ | 実装と同じ | 実装と異なる | 実装と異なる | 必要なし | 必要なし | | 仕様の検証 | 可能 | 可能 | 不可能 | 可能 | 可能 | 不可能 | 不可能 | -| メモリリークなどの検出 | 今は不可能 | 不可能? | 不可能 | | | | 可能 | -| 状態の数え上げ | 可能 | 可能 | 不可能 | 可能 | ものによる | 可能 | | -| 反例の表示 | 可能 | 可能 | 不可能 | | | 不可能 | | +| メモリリークなどの検出 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | 不可能 | 可能 | +| 状態の数え上げ | 可能 | 可能 | 不可能 | 可能 | 不可能 | 可能 | 不可能 | +| 反例の表示 | 可能 | 可能 | 不可能 | 可能 | 不可能 | 不可能 | 不可能 | -# Conclusion and Future Works -* CBMC では検証できない範囲の検証を行なうことができた -* 動作するプログラムの記述を変更することなく検証を行なえた - * テストケースの自動生成+仕様の反例表示ができた -* 今後の課題 - * 挿入だけでなく削除を含む赤黒木の仕様検証 - * 状態の抽象化による探索の効率化 - * ポインタへの不正アクセス検出などの機能 - * 言語処理系に検証を行ないやすくする機構の導入 +# Future Works +* 挿入だけでなく削除を含む赤黒木の仕様検証 +* 状態の抽象化による探索の効率化 +* ポインタへの不正アクセス検出などの機能 +* 言語処理系に検証を行ないやすくする機構の導入 -# TODO: おまけ -* cbmc のバージョン、オプション -* rbtree の行数 -* 実行時間 +# CBMC Informations +* CBMC 5.4 +* 実行オプション + * cbmc --unwind 1 + * cbmc --depth 400 --property verifySpecification.assertion.1 +* 赤黒木のCbC実装 + * 赤黒木部分のみ: 330行 + * スタックやメモリのアロケータなどを含める: 640行