Papers/2021/ikkun-master: poster/poster.html comparison

comparison poster/poster.html @ 4:3139ed741e26

fix

author	ikkun <ikkun@cr.ie.u-ryukyu.ac.jp>
date	Mon, 15 Feb 2021 13:56:04 +0900
parents	1b34d9710a84
children	4c39c90d1b1b

comparison

equal deleted inserted replaced

-:1b34d9710a84
+:3139ed741e26
 */div#p>svg>foreignObject>section .octicon{display:inline-block;fill:currentColor;vertical-align:text-bottom}div#p>svg>foreignObject>section .anchor{float:left;line-height:1;margin-left:-20px;padding-right:4px}div#p>svg>foreignObject>section .anchor:focus{outline:none}div#p>svg>foreignObject>section h1 .octicon-link,div#p>svg>foreignObject>section h2 .octicon-link,div#p>svg>foreignObject>section h3 .octicon-link,div#p>svg>foreignObject>section h4 .octicon-link,div#p>svg>foreignObject>section h5 .octicon-link,div#p>svg>foreignObject>section h6 .octicon-link{color:#1b1f23;vertical-align:middle;visibility:hidden}div#p>svg>foreignObject>section h1:hover .anchor,div#p>svg>foreignObject>section h2:hover .anchor,div#p>svg>foreignObject>section h3:hover .anchor,div#p>svg>foreignObject>section h4:hover .anchor,div#p>svg>foreignObject>section h5:hover .anchor,div#p>svg>foreignObject>section h6:hover .anchor{text-decoration:none}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link{visibility:visible}div#p>svg>foreignObject>section h1:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h2:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h3:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h4:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h5:hover .anchor .octicon-link:before,div#p>svg>foreignObject>section h6:hover .anchor .octicon-link:before{width:16px;height:16px;content:" ";display:inline-block;background-image:url("data:image/svg+xml;charset=utf-8,%3Csvg xmlns='http://www.w3.org/2000/svg' width='16' height='16' aria-hidden='true'%3E%3Cpath fill-rule='evenodd' d='M4 9h1v1H4c-1.5 0-3-1.69-3-3.5S2.55 3 4 3h4c1.45 0 3 1.69 3 3.5 0 1.41-.91 2.72-2 3.25V8.59c.58-.45 1-1.27 1-2.09C10 5.22 8.98 4 8 4H4c-.98 0-2 1.22-2 2.5S3 9 4 9zm9-3h-1v1h1c1 0 2 1.22 2 2.5S13.98 12 13 12H9c-.98 0-2-1.22-2-2.5 0-.83.42-1.64 1-2.09V6.25c-1.09.53-2 1.84-2 3.25C6 11.31 7.55 13 9 13h4c1.45 0 3-1.69 3-3.5S14.5 6 13 6z'/%3E%3C/svg%3E")}div#p>svg>foreignObject>section{-ms-text-size-adjust:100%;-webkit-text-size-adjust:100%;color:#24292e;font-family:-apple-system,BlinkMacSystemFont,Segoe UI,Helvetica,Arial,sans-serif,Apple Color Emoji,Segoe UI Emoji;font-size:16px;line-height:1.5;word-wrap:break-word}div#p>svg>foreignObject>section details{display:block}div#p>svg>foreignObject>section summary{display:list-item}div#p>svg>foreignObject>section a{background-color:initial}div#p>svg>foreignObject>section a:active,div#p>svg>foreignObject>section a:hover{outline-width:0}div#p>svg>foreignObject>section strong{font-weight:inherit;font-weight:bolder}div#p>svg>foreignObject>section h1{margin:.67em 0}div#p>svg>foreignObject>section img{border-style:none}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section kbd,div#p>svg>foreignObject>section pre{font-family:monospace,monospace;font-size:1em}div#p>svg>foreignObject>section hr{box-sizing:initial;overflow:visible}div#p>svg>foreignObject>section input{font:inherit;margin:0;overflow:visible}div#p>svg>foreignObject>section [type=checkbox]{padding:0}div#p>svg>foreignObject>section *,div#p>svg>foreignObject>section [type=checkbox]{box-sizing:border-box}div#p>svg>foreignObject>section input{font-family:inherit;font-size:inherit;line-height:inherit}div#p>svg>foreignObject>section a{color:#0366d6;text-decoration:none}div#p>svg>foreignObject>section a:hover{text-decoration:underline}div#p>svg>foreignObject>section strong{font-weight:600}div#p>svg>foreignObject>section hr{height:0;margin:15px 0;overflow:hidden;background:transparent;border-bottom:1px solid #dfe2e5}div#p>svg>foreignObject>section hr:after,div#p>svg>foreignObject>section hr:before{display:table;content:""}div#p>svg>foreignObject>section hr:after{clear:both}div#p>svg>foreignObject>section table{border-spacing:0;border-collapse:collapse}div#p>svg>foreignObject>section td,div#p>svg>foreignObject>section th{padding:0}div#p>svg>foreignObject>section details summary{cursor:pointer}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2,div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4,div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{margin-top:0;margin-bottom:0}div#p>svg>foreignObject>section h1{font-size:32px}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{font-weight:600}div#p>svg>foreignObject>section h2{font-size:24px}div#p>svg>foreignObject>section h3{font-size:20px}div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4{font-weight:600}div#p>svg>foreignObject>section h4{font-size:16px}div#p>svg>foreignObject>section h5{font-size:14px}div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{font-weight:600}div#p>svg>foreignObject>section h6{font-size:12px}div#p>svg>foreignObject>section p{margin-top:0;margin-bottom:10px}div#p>svg>foreignObject>section blockquote{margin:0}div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section ul{padding-left:0;margin-top:0;margin-bottom:0}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ul ol{list-style-type:lower-roman}div#p>svg>foreignObject>section ol ol ol,div#p>svg>foreignObject>section ol ul ol,div#p>svg>foreignObject>section ul ol ol,div#p>svg>foreignObject>section ul ul ol{list-style-type:lower-alpha}div#p>svg>foreignObject>section dd{margin-left:0}div#p>svg>foreignObject>section code,div#p>svg>foreignObject>section pre{font-family:SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;font-size:12px}div#p>svg>foreignObject>section pre{margin-top:0;margin-bottom:0}div#p>svg>foreignObject>section input::-webkit-inner-spin-button,div#p>svg>foreignObject>section input::-webkit-outer-spin-button{margin:0;-webkit-appearance:none;appearance:none}div#p>svg>foreignObject>section :checked+.radio-label{position:relative;z-index:1;border-color:#0366d6}div#p>svg>foreignObject>section .border{border:1px solid #e1e4e8!important}div#p>svg>foreignObject>section .border-0{border:0!important}div#p>svg>foreignObject>section .border-bottom{border-bottom:1px solid #e1e4e8!important}div#p>svg>foreignObject>section .rounded-1{border-radius:3px!important}div#p>svg>foreignObject>section .bg-white{background-color:#fff!important}div#p>svg>foreignObject>section .bg-gray-light{background-color:#fafbfc!important}div#p>svg>foreignObject>section .text-gray-light{color:#6a737d!important}div#p>svg>foreignObject>section .pl-3,div#p>svg>foreignObject>section .px-3{padding-left:16px!important}div#p>svg>foreignObject>section .px-3{padding-right:16px!important}div#p>svg>foreignObject>section .f6{font-size:12px!important}div#p>svg>foreignObject>section .lh-condensed{line-height:1.25!important}div#p>svg>foreignObject>section .text-bold{font-weight:600!important}div#p>svg>foreignObject>section .pl-c{color:#6a737d}div#p>svg>foreignObject>section .pl-c1,div#p>svg>foreignObject>section .pl-s .pl-v{color:#005cc5}div#p>svg>foreignObject>section .pl-e,div#p>svg>foreignObject>section .pl-en{color:#6f42c1}div#p>svg>foreignObject>section .pl-s .pl-s1,div#p>svg>foreignObject>section .pl-smi{color:#24292e}div#p>svg>foreignObject>section .pl-ent{color:#22863a}div#p>svg>foreignObject>section .pl-k{color:#d73a49}div#p>svg>foreignObject>section .pl-pds,div#p>svg>foreignObject>section .pl-s,div#p>svg>foreignObject>section .pl-s .pl-pse .pl-s1,div#p>svg>foreignObject>section .pl-sr,div#p>svg>foreignObject>section .pl-sr .pl-cce,div#p>svg>foreignObject>section .pl-sr .pl-sra,div#p>svg>foreignObject>section .pl-sr .pl-sre{color:#032f62}div#p>svg>foreignObject>section .pl-smw,div#p>svg>foreignObject>section .pl-v{color:#e36209}div#p>svg>foreignObject>section .pl-bu{color:#b31d28}div#p>svg>foreignObject>section .pl-ii{color:#fafbfc;background-color:#b31d28}div#p>svg>foreignObject>section .pl-c2{color:#fafbfc;background-color:#d73a49}div#p>svg>foreignObject>section .pl-c2:before{content:"^M"}div#p>svg>foreignObject>section .pl-sr .pl-cce{font-weight:700;color:#22863a}div#p>svg>foreignObject>section .pl-ml{color:#735c0f}div#p>svg>foreignObject>section .pl-mh,div#p>svg>foreignObject>section .pl-mh .pl-en,div#p>svg>foreignObject>section .pl-ms{font-weight:700;color:#005cc5}div#p>svg>foreignObject>section .pl-mi{font-style:italic;color:#24292e}div#p>svg>foreignObject>section .pl-mb{font-weight:700;color:#24292e}div#p>svg>foreignObject>section .pl-md{color:#b31d28;background-color:#ffeef0}div#p>svg>foreignObject>section .pl-mi1{color:#22863a;background-color:#f0fff4}div#p>svg>foreignObject>section .pl-mc{color:#e36209;background-color:#ffebda}div#p>svg>foreignObject>section .pl-mi2{color:#f6f8fa;background-color:#005cc5}div#p>svg>foreignObject>section .pl-mdr{font-weight:700;color:#6f42c1}div#p>svg>foreignObject>section .pl-ba{color:#586069}div#p>svg>foreignObject>section .pl-sg{color:#959da5}div#p>svg>foreignObject>section .pl-corl{text-decoration:underline;color:#032f62}div#p>svg>foreignObject>section .mb-0{margin-bottom:0!important}div#p>svg>foreignObject>section .my-2{margin-bottom:8px!important;margin-top:8px!important}div#p>svg>foreignObject>section .pl-0{padding-left:0!important}div#p>svg>foreignObject>section .py-0{padding-top:0!important;padding-bottom:0!important}div#p>svg>foreignObject>section .pl-1{padding-left:4px!important}div#p>svg>foreignObject>section .pl-2{padding-left:8px!important}div#p>svg>foreignObject>section .py-2{padding-top:8px!important;padding-bottom:8px!important}div#p>svg>foreignObject>section .pl-3{padding-left:16px!important}div#p>svg>foreignObject>section .pl-4{padding-left:24px!important}div#p>svg>foreignObject>section .pl-5{padding-left:32px!important}div#p>svg>foreignObject>section .pl-6{padding-left:40px!important}div#p>svg>foreignObject>section .pl-7{padding-left:48px!important}div#p>svg>foreignObject>section .pl-8{padding-left:64px!important}div#p>svg>foreignObject>section .pl-9{padding-left:80px!important}div#p>svg>foreignObject>section .pl-10{padding-left:96px!important}div#p>svg>foreignObject>section .pl-11{padding-left:112px!important}div#p>svg>foreignObject>section .pl-12{padding-left:128px!important}div#p>svg>foreignObject>section hr{border-bottom-color:#eee}div#p>svg>foreignObject>section kbd{display:inline-block;padding:3px 5px;font:11px SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;line-height:10px;color:#444d56;vertical-align:middle;background-color:#fafbfc;border:1px solid #d1d5da;border-radius:3px;box-shadow:inset 0 -1px 0 #d1d5da}div#p>svg>foreignObject>section:after,div#p>svg>foreignObject>section:before{display:table
 /* content:""; */}div#p>svg>foreignObject>section:after{clear:both}div#p>svg>foreignObject>section>:first-child{margin-top:0!important}div#p>svg>foreignObject>section>:last-child{margin-bottom:0!important}div#p>svg>foreignObject>section a:not([href]){color:inherit;text-decoration:none}div#p>svg>foreignObject>section blockquote,div#p>svg>foreignObject>section details,div#p>svg>foreignObject>section dl,div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section p,div#p>svg>foreignObject>section pre,div#p>svg>foreignObject>section table,div#p>svg>foreignObject>section ul{margin-top:0;margin-bottom:16px}div#p>svg>foreignObject>section hr{height:.25em;padding:0;margin:24px 0;background-color:#e1e4e8;border:0}div#p>svg>foreignObject>section blockquote{padding:0 1em;color:#6a737d;border-left:.25em solid #dfe2e5}div#p>svg>foreignObject>section blockquote>:first-child{margin-top:0}div#p>svg>foreignObject>section blockquote>:last-child{margin-bottom:0}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2,div#p>svg>foreignObject>section h3,div#p>svg>foreignObject>section h4,div#p>svg>foreignObject>section h5,div#p>svg>foreignObject>section h6{margin-top:24px;margin-bottom:16px;font-weight:600;line-height:1.25}div#p>svg>foreignObject>section h1{font-size:2em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{padding-bottom:.3em;border-bottom:1px solid #eaecef}div#p>svg>foreignObject>section h2{font-size:1.5em}div#p>svg>foreignObject>section h3{font-size:1.25em}div#p>svg>foreignObject>section h4{font-size:1em}div#p>svg>foreignObject>section h5{font-size:.875em}div#p>svg>foreignObject>section h6{font-size:.85em;color:#6a737d}div#p>svg>foreignObject>section ol,div#p>svg>foreignObject>section ul{padding-left:2em}div#p>svg>foreignObject>section ol ol,div#p>svg>foreignObject>section ol ul,div#p>svg>foreignObject>section ul ol,div#p>svg>foreignObject>section ul ul{margin-top:0;margin-bottom:0}div#p>svg>foreignObject>section li{word-wrap:break-all}div#p>svg>foreignObject>section li>p{margin-top:16px}div#p>svg>foreignObject>section li+li{margin-top:.25em}div#p>svg>foreignObject>section dl{padding:0}div#p>svg>foreignObject>section dl dt{padding:0;margin-top:16px;font-size:1em;font-style:italic;font-weight:600}div#p>svg>foreignObject>section dl dd{padding:0 16px;margin-bottom:16px}div#p>svg>foreignObject>section table{display:block;width:100%;overflow:auto}div#p>svg>foreignObject>section table th{font-weight:600}div#p>svg>foreignObject>section table td,div#p>svg>foreignObject>section table th{padding:6px 13px;border:1px solid #dfe2e5}div#p>svg>foreignObject>section table tr{background-color:#fff;border-top:1px solid #c6cbd1}div#p>svg>foreignObject>section table tr:nth-child(2n){background-color:#f6f8fa}div#p>svg>foreignObject>section img{max-width:100%;box-sizing:initial;background-color:#fff}div#p>svg>foreignObject>section img[align=right]{padding-left:20px}div#p>svg>foreignObject>section img[align=left]{padding-right:20px}div#p>svg>foreignObject>section code{padding:.2em .4em;margin:0;font-size:85%;background-color:rgba(27,31,35,.05);border-radius:3px}div#p>svg>foreignObject>section pre{word-wrap:normal}div#p>svg>foreignObject>section pre>code{padding:0;margin:0;font-size:100%;word-break:normal;white-space:pre;background:transparent;border:0}div#p>svg>foreignObject>section .highlight{margin-bottom:16px}div#p>svg>foreignObject>section .highlight pre{margin-bottom:0;word-break:normal}div#p>svg>foreignObject>section pre{padding:16px;overflow:auto;font-size:85%;line-height:1.45;background-color:#f6f8fa;border-radius:3px}div#p>svg>foreignObject>section pre code{display:inline;max-width:auto;padding:0;margin:0;overflow:visible;line-height:inherit;word-wrap:normal;background-color:initial;border:0}div#p>svg>foreignObject>section .commit-tease-sha{display:inline-block;font-family:SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;font-size:90%;color:#444d56}div#p>svg>foreignObject>section .full-commit .btn-outline:not(:disabled):hover{color:#005cc5;border-color:#005cc5}div#p>svg>foreignObject>section .blob-wrapper{overflow-x:auto;overflow-y:hidden}div#p>svg>foreignObject>section .blob-wrapper-embedded{max-height:240px;overflow-y:auto}div#p>svg>foreignObject>section .blob-num{width:1%;min-width:50px;padding-right:10px;padding-left:10px;font-family:SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;font-size:12px;line-height:20px;color:rgba(27,31,35,.3);text-align:right;white-space:nowrap;vertical-align:top;cursor:pointer;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none}div#p>svg>foreignObject>section .blob-num:hover{color:rgba(27,31,35,.6)}div#p>svg>foreignObject>section .blob-num:before{content:attr(data-line-number)}div#p>svg>foreignObject>section .blob-code{position:relative;padding-right:10px;padding-left:10px;line-height:20px;vertical-align:top}div#p>svg>foreignObject>section .blob-code-inner{overflow:visible;font-family:SFMono-Regular,Consolas,Liberation Mono,Menlo,monospace;font-size:12px;color:#24292e;word-wrap:normal;white-space:pre}div#p>svg>foreignObject>section .pl-token.active,div#p>svg>foreignObject>section .pl-token:hover{cursor:pointer;background:#ffea7f}div#p>svg>foreignObject>section .tab-size[data-tab-size="1"]{-moz-tab-size:1;-o-tab-size:1;tab-size:1}div#p>svg>foreignObject>section .tab-size[data-tab-size="2"]{-moz-tab-size:2;-o-tab-size:2;tab-size:2}div#p>svg>foreignObject>section .tab-size[data-tab-size="3"]{-moz-tab-size:3;-o-tab-size:3;tab-size:3}div#p>svg>foreignObject>section .tab-size[data-tab-size="4"]{-moz-tab-size:4;-o-tab-size:4;tab-size:4}div#p>svg>foreignObject>section .tab-size[data-tab-size="5"]{-moz-tab-size:5;-o-tab-size:5;tab-size:5}div#p>svg>foreignObject>section .tab-size[data-tab-size="6"]{-moz-tab-size:6;-o-tab-size:6;tab-size:6}div#p>svg>foreignObject>section .tab-size[data-tab-size="7"]{-moz-tab-size:7;-o-tab-size:7;tab-size:7}div#p>svg>foreignObject>section .tab-size[data-tab-size="8"]{-moz-tab-size:8;-o-tab-size:8;tab-size:8}div#p>svg>foreignObject>section .tab-size[data-tab-size="9"]{-moz-tab-size:9;-o-tab-size:9;tab-size:9}div#p>svg>foreignObject>section .tab-size[data-tab-size="10"]{-moz-tab-size:10;-o-tab-size:10;tab-size:10}div#p>svg>foreignObject>section .tab-size[data-tab-size="11"]{-moz-tab-size:11;-o-tab-size:11;tab-size:11}div#p>svg>foreignObject>section .tab-size[data-tab-size="12"]{-moz-tab-size:12;-o-tab-size:12;tab-size:12}div#p>svg>foreignObject>section .task-list-item{list-style-type:none}div#p>svg>foreignObject>section .task-list-item+.task-list-item{margin-top:3px}div#p>svg>foreignObject>section .task-list-item input{margin:0 .2em .25em -1.6em;vertical-align:middle}div#p>svg>foreignObject>section .hljs{display:block;background:#fff;padding:.5em;color:#333;overflow-x:auto}div#p>svg>foreignObject>section .hljs-comment,div#p>svg>foreignObject>section .hljs-meta{color:#969896}div#p>svg>foreignObject>section .hljs-emphasis,div#p>svg>foreignObject>section .hljs-quote,div#p>svg>foreignObject>section .hljs-strong,div#p>svg>foreignObject>section .hljs-template-variable,div#p>svg>foreignObject>section .hljs-variable{color:#df5000}div#p>svg>foreignObject>section .hljs-keyword,div#p>svg>foreignObject>section .hljs-selector-tag,div#p>svg>foreignObject>section .hljs-type{color:#d73a49}div#p>svg>foreignObject>section .hljs-attribute,div#p>svg>foreignObject>section .hljs-bullet,div#p>svg>foreignObject>section .hljs-literal,div#p>svg>foreignObject>section .hljs-symbol{color:#0086b3}div#p>svg>foreignObject>section .hljs-name,div#p>svg>foreignObject>section .hljs-section{color:#63a35c}div#p>svg>foreignObject>section .hljs-tag{color:#333}div#p>svg>foreignObject>section .hljs-attr,div#p>svg>foreignObject>section .hljs-selector-attr,div#p>svg>foreignObject>section .hljs-selector-class,div#p>svg>foreignObject>section .hljs-selector-id,div#p>svg>foreignObject>section .hljs-selector-pseudo,div#p>svg>foreignObject>section .hljs-title{color:#6f42c1}div#p>svg>foreignObject>section .hljs-addition{color:#55a532;background-color:#eaffea}div#p>svg>foreignObject>section .hljs-deletion{color:#bd2c00;background-color:#ffecec}div#p>svg>foreignObject>section .hljs-link{text-decoration:underline}div#p>svg>foreignObject>section .hljs-number{color:#005cc5}div#p>svg>foreignObject>section .hljs-string{color:#032f62}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{max-height:563px}div#p>svg>foreignObject>section h1{color:#246;font-size:1.6em}div#p>svg>foreignObject>section h1,div#p>svg>foreignObject>section h2{border-bottom:none}div#p>svg>foreignObject>section h2{font-size:1.3em}div#p>svg>foreignObject>section h3{font-size:1.1em}div#p>svg>foreignObject>section h4{font-size:1.05em}div#p>svg>foreignObject>section h5{font-size:1em}div#p>svg>foreignObject>section h6{font-size:.9em}div#p>svg>foreignObject>section h1 strong,div#p>svg>foreignObject>section h2 strong,div#p>svg>foreignObject>section h3 strong,div#p>svg>foreignObject>section h4 strong,div#p>svg>foreignObject>section h5 strong,div#p>svg>foreignObject>section h6 strong{font-weight:inherit;color:#48c}div#p>svg>foreignObject>section hr{height:0;padding-top:.25em}div#p>svg>foreignObject>section pre{border:1px solid #999;line-height:1.15;overflow:visible}div#p>svg>foreignObject>section pre code svg[data-marp-fitting=svg]{max-height:529px}div#p>svg>foreignObject>section footer,div#p>svg>foreignObject>section header{margin:0;position:absolute;left:30px;color:hsla(0,0%,40%,.75);font-size:18px}div#p>svg>foreignObject>section header{top:21px}div#p>svg>foreignObject>section footer{bottom:21px}div#p>svg>foreignObject>section{align-items:stretch;background:#fff;display:flex;flex-direction:column;flex-wrap:nowrap;font-size:29px;height:720px;justify-content:center;padding:78.5px;width:1280px}div#p>svg>foreignObject>section>:last-child,div#p>svg>foreignObject>section[data-footer]>:nth-last-child(2){margin-bottom:0}div#p>svg>foreignObject>section>:first-child,div#p>svg>foreignObject>section>header:first-child+*{margin-top:0}div#p>svg>foreignObject>section:after{position:absolute;padding:0;right:30px;bottom:21px;font-size:24px;color:#777}div#p>svg>foreignObject>section.invert{background-color:#222;color:#e6eaf0}div#p>svg>foreignObject>section.invert:after{color:#999}div#p>svg>foreignObject>section.invert img{background-color:transparent}div#p>svg>foreignObject>section.invert a{color:#50b3ff}div#p>svg>foreignObject>section.invert h1{color:#a3c5e7}div#p>svg>foreignObject>section.invert h2,div#p>svg>foreignObject>section.invert h3,div#p>svg>foreignObject>section.invert h4,div#p>svg>foreignObject>section.invert h5{color:#ebeff5}div#p>svg>foreignObject>section.invert blockquote,div#p>svg>foreignObject>section.invert h6{border-color:#3d3f43;color:#939699}div#p>svg>foreignObject>section.invert h1 strong,div#p>svg>foreignObject>section.invert h2 strong,div#p>svg>foreignObject>section.invert h3 strong,div#p>svg>foreignObject>section.invert h4 strong,div#p>svg>foreignObject>section.invert h5 strong,div#p>svg>foreignObject>section.invert h6 strong{color:#7bf}div#p>svg>foreignObject>section.invert hr{background-color:#3d3f43}div#p>svg>foreignObject>section.invert footer,div#p>svg>foreignObject>section.invert header{color:hsla(0,0%,60%,.75)}div#p>svg>foreignObject>section.invert code,div#p>svg>foreignObject>section.invert kbd{background-color:#111}div#p>svg>foreignObject>section.invert kbd{border-color:#666;box-shadow:inset 0 -1px 0 #555;color:#e6eaf0}div#p>svg>foreignObject>section.invert table tr{background-color:#12181d;border-color:#60657b}div#p>svg>foreignObject>section.invert table tr:nth-child(2n){background-color:#1b2024}div#p>svg>foreignObject>section.invert table td,div#p>svg>foreignObject>section.invert table th{border-color:#5b5e61}div#p>svg>foreignObject>section.invert pre{background-color:#0a0e12;border-color:#777}div#p>svg>foreignObject>section.invert pre code{background-color:transparent}div#p>svg>foreignObject>section[data-color] h1,div#p>svg>foreignObject>section[data-color] h2,div#p>svg>foreignObject>section[data-color] h3,div#p>svg>foreignObject>section[data-color] h4,div#p>svg>foreignObject>section[data-color] h5,div#p>svg>foreignObject>section[data-color] h6{color:currentColor}div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{display:block;height:auto;width:100%}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg]{position:static}}div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{content:""}@supports (-ms-ime-align:auto){div#p>svg>foreignObject>section svg[data-marp-fitting=svg].__reflow__{position:relative}}div#p>svg>foreignObject>section [data-marp-fitting-svg-content]{display:table;white-space:nowrap}div#p>svg>foreignObject>section [data-marp-fitting-svg-content-wrap]{white-space:pre}div#p>svg>foreignObject>section img[data-marp-twemoji]{background:transparent;height:1em;margin:0 .05em 0 .1em;vertical-align:-.1em;width:1em}
 /* @theme example */div#p>svg>foreignObject>section{background-image:url("assets/logo.svg");background-position:right 3% bottom 2%;background-repeat:no-repeat;background-attachment:5%;background-size:20% auto}
-/* @theme acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="1" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+/* @theme vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr */div#p>svg>foreignObject>section[data-marpit-advanced-background=background]{display:block!important;padding:0!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=background]:before,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:after,div#p>svg>foreignObject>section[data-marpit-advanced-background=content]:before{display:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]{all:initial;display:flex;flex-direction:row;height:100%;overflow:hidden;width:100%}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container][data-marpit-advanced-background-direction=vertical]{flex-direction:column}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split]>div[data-marpit-advanced-background-container]{width:var(--marpit-advanced-background-split,50%)}div#p>svg>foreignObject>section[data-marpit-advanced-background=background][data-marpit-advanced-background-split=right]>div[data-marpit-advanced-background-container]{margin-left:calc(100% - var(--marpit-advanced-background-split, 50%))}div#p>svg>foreignObject>section[data-marpit-advanced-background=background]>div[data-marpit-advanced-background-container]>figure{all:initial;background-position:center;background-repeat:no-repeat;background-size:cover;flex:auto;margin:0}div#p>svg>foreignObject>section[data-marpit-advanced-background=content],div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo]{background:transparent!important}div#p>svg>foreignObject>section[data-marpit-advanced-background=pseudo],div#p>svg[data-marpit-svg]>foreignObject[data-marpit-advanced-background=pseudo]{pointer-events:none!important}div#p>svg>foreignObject>section[data-marpit-advanced-background-split]{width:100%;height:100%}</style></head><body><div class="bespoke-marp-osc"><button data-bespoke-marp-osc="prev" tabindex="-1" title="Previous slide">Previous slide</button><span data-bespoke-marp-osc="page"></span><button data-bespoke-marp-osc="next" tabindex="-1" title="Next slide">Next slide</button><button data-bespoke-marp-osc="fullscreen" tabindex="-1" title="Toggle fullscreen (f)">Toggle fullscreen</button><button data-bespoke-marp-osc="presenter" tabindex="-1" title="Open presenter view (p)">Open presenter view</button></div><div id="p"><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="1" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="1" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1><svg data-marp-fitting="svg"><foreignObject><span data-marp-fitting-svg-content> Gears OSでモデル検査を実現する手法について</span></foreignObject></svg></h1>
 <ul>
 <li>東恩納 琢偉
 <ul>
 <li>琉球大学理工学研究科 情報工学専攻</li>
 </ul>
 </li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="2" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="2" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="2" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>研究目的</h1>
 <ul>
 <li>OS上ではさまざまなアプリケーションやサービスが提供されるが、予期しないエラーが起こる。</li>
 <li>本研究室で開発している GearsOS ではアプリケーションやサービスの信頼性の保証をOSの機能として行うことを目指しており、本研究ではモデル検査をもちいた手法について発表する。</li>
 <li>また GearsOS そのものを GearsOS 上でモデル検査する手法についても考察する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="3" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="3" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="3" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>Gears OS</h1>
 <ul>
 <li>Continuation based C によって記述されている。</li>
 <li>信頼性を保証する手法として、モデル検査による検証や、定理証明によるアプローチも行っている。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="4" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="4" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="4" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>Continution based C (CbC)</h1>
 <ul>
 <li>Gear という単位で分割され、goto 文によって遷移する。</li>
 <li>codeGear は プログラムにおける処理記述になっている。</li>
 <li>また 変数や構造体といったデータは dataGear に保管される。</li>
 }
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="5" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="5" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="5" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>goto</h1>
 <ul>
 <li>CbC での遷移は軽量継続といいgoto 文を用いる。</li>
 <li>これは関数呼び出しと異なり、stackや環境を隠して持つことがありません。</li>
 <li>CbC において、処理を行うのは codeGear であるため、プログラムの状態の変化は codeGear によって決まる。</li>
 <li>よって CbC での遷移記述をそのまま状態記述とすることが出来る。</li>
 </ul>
 <center><img src="./pic/goto.svg" alt="" width="80%" height="80%" /></center>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="6" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="6" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="6" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>メタ計算</h1>
 <ul>
 <li>軽量継続である CbC は遷移する際に別の処理を挟む事が可能で、この処理をメタ計算という。</li>
 <li>メタ計算は meta codeGear で行われ、ここに検証用の処理を入れる事が出来る。</li>
 </ul>
 <center><img src="./pic/meta_gear2.svg" alt="" width="90%" height="90%" /></center>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="7" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="7" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="7" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>data Gear と meta dataGear</h1>
 <ul>
 <li>CbC における入力は dataGear と呼ばれる構造体になっており、ノーマルレベル<br />
 とメタレベルがある。</li>
 <li>メタレベルには計算を行うCPUやメモリ、計算に関するノーマルレベルのdataGearもcontext に格納されている。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="8" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="8" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="8" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>stub CodeGear (メタレベルからノーマルレベルへの橋渡し)</h1>
 <ul>
 <li>メタレベルから見ると、code Gearの入力はcontext ただ1つである。</li>
 <li>ノーマルレベルからメタレベルの context を直接参照してしまうことはできない。</li>
 <li>context から必要なノーマルレベルのdata Gearを取り出して、ノーマルレベルのcodeGearを呼び出し渡す処理を行う仲介役として、メタレベルの stub codeGearを用意する。</li>
 enum Code next = <span class="hljs-constructor">Gearef(<span class="hljs-params">context</span>, Stack)</span>-&gt;next;
 goto clear<span class="hljs-constructor">SingleLinkedStack(<span class="hljs-params">context</span>, <span class="hljs-params">stack</span>, <span class="hljs-params">next</span>)</span>;
 }
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="9" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="9" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="9" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>プロセスであるcontext の並べ替えによる並列実行</h1>
 <ul>
 <li>プログラムの非決定的な実行は、入力あるいは並列実行の非決定性から生じる。</li>
 <li>並列実行の非決定性は、実行される codeGear の並び替えを生成し、contextの状態を数え上げる。</li>
 <li>これがモデル検査になる。</li>
 <li>並び替えの数(プログラム全体の可能な状態)はとても巨大になる場合がある。</li>
 <li>状態はデータベースに格納する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="10" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="10" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="10" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>codeGearのatomicity</h1>
 <ul>
 <li>codeGear は処理の基本単位であり、並列処理などにより割り込まれることなく記述された通りに実行される必要がある。</li>
 <li>一般的には、他の codeGear が共有されたdataGearに競合的に書き込んだり、割り込みにより処理が中断したりする。</li>
 <li>GearsOS においては codeGear が正しくatomicに実行されるように実装する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="11" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="11" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="11" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>モデル検査する仕様の記述法</h1>
 <ul>
 <li>
 <p>検証したい内容を時様相論理式 p をつくり、対象のシステムの初期状態 s のモデル M があるとき、M,s |= p(M,s が p を満たすか)をモデル検査器を用いて調べることによって信頼性を保証する手法である。</p>
 </li>
 <li>
 <p>時相論理式にはCTL(Computation Tree Logic) や LTTL(Linear Time Temporal Logic)といったものがあり、それぞれ計算木と線形時相論理式と言われるものである。</p>
 </li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="12" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="12" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="12" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>他のモデル検査実装例</h1>
 <ul>
 <li>
 <p>SPIN<br />
 Promela (Process Meta Language)で仕様と実装を記述する。</p>
 CMU で開発されたモデル検査器<br />
 SAT solver</p>
 </li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="13" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="13" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="13" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>Geras OS のモデル検査</h1>
 <ul>
 <li>CbC によって記述されており、CbC の記述そのものを状態遷移として落とし込む。</li>
 <li>par goto により複数スレッドの並行実行する。</li>
 <li>メタ計算によって並行実行のモデル検査を行う。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="14" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="14" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="14" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
-<h1>Gears OS におけるモデル検査</h1>
+<h1>Gears OS におけるモデル検査の実装手順</h1>
 <ol>
 <li>GearsOS におけるモデル検査はcode gear 単位の順列組み合わせによって行われる。</li>
 <li>codegear 実行後の状態を、データベースに格納する。</li>
 <li>新しい状態が生成されなくなった時モデル検査が終了する。</li>
 <li>哲学者５人が次の状態に進めなくなった時をデッドロックとして検出する。</li>
 <li>これにより状態数を下げることができる。</li>
 <li>問題に合わせたメタ計算により、モデル検査の状態数を下げることができる。</li>
 <li>GearsOS による検証用プログラムとして Dining Philosohers Ploblem (DPP）を用いる。</li>
 </ol>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="15" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="15" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="15" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>DPP</h1>
 <p><right><img src="./pic/dpp_image.svg" alt="" height="90%" /></right></p>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="16" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="16" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="16" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>DPP(dining philosohers ploblem)</h1>
 <ul>
 <li>5人の哲学者が円卓についており、各々スパゲティーの皿が目の前に用意され、スパゲティーは絡まっている為２つのフォーク使わなければ食べれない。</li>
 <li>フォークは皿の間に１本ずつの計5本しかないため、すべての哲学者が同時に食事することはできず、また全員がフォークを1本ずつ持ってしまった場合、誰も食事することは出来ない。この状態をデッドロックとする。<br />
 -DPPは次の6つの状態からなる。<br />
 <code>Pickup Right fork</code> <code> Pickup Left fork</code> <code>eating</code> <code> Put Right fork</code> <code>Put Left fork</code> <code>Thinking</code></li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="17" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="17" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="17" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>GearsOS におけるDPP実装(1/2)</h1>
 <ul>
 <li>マルチスレッドでのデータの一貫性を保証する手法としてCheck and Set (CAS) を用いる。</li>
 <li>CAS を用いて値の比較、更新をアトミックに行う。</li>
 <li>CAS は書き込みの際に、書き込む MetaCodeGear に更新前と更新後の値を渡し、更新前の値が保存されているメモリ番地の値と比較し同じデータがであれば書き込みを行う。異なる場合はほかからの書き込みがあったとみなし、値の更新に失敗し、もう一度CASを行う。</li>
 <li>DPPの例題ではフォークがスレッドで共有されるデータにあたるので、CAS を用いることによってスレッド間での同期を行う。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="18" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="18" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="18" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>GearsOS におけるDPP実装(2/2)</h1>
 <ul>
 <li>5つのスレッドで行われる処理の状態は6つあり、それぞれを状態変数で表される。</li>
 <li>この状態遷移は goto next によって遷移し、metaCodeGear を 挟みメタレベルで各スレッドの状態を 各スレッドごとに用意した Memory Tree に保存する。</li>
 <li>Memory Tree はstateDBによってまとめられ、同じ状態は共有される。</li>
 <li>またDPPにおける状態遷移は無限ループであるため、stateDBを用いて同じ状態を検索することで、終了判定を行う。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="19" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="19" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="19" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <center><img src="./pic/model_checking.svg" width="50%" /></center>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="20" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="20" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="20" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>GearsOS でのモデル検査を実現する方法について</h1>
 <ul>
 <li>DPP をGearsOS 上のアプリケーションとして実装する。</li>
-<li>DPP を codeGear のシャッフルの１つとして実行する。</li>
+<li>DPP を codeGear の１つとしてシャッフル実行する。</li>
 <li>可能な実行を生成する iterator</li>
 <li>状態を記録する memory Tree と stateDB を作成する。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="21" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="21" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="21" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>モデル検査器の現状</h1>
 <ul>
 <li>GearsOS 上での導出木の生成</li>
 <li>生成した木のマーキングによる時相論理の検証</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="22" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="22" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="22" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>Metaの入れ替え</h1>
 <ul>
 <li>perl script を用いて、遷移先のmetaを置き換える事が可能となっている。</li>
 <li>遷移先のmetaを切り替えることによって、ノーマルレベルで走るプログラムを書き換える事なく、mcMeta によるシングルスレッド実行と並列実行ようのランダム実行を行う事が出来る。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="23" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="23" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="23" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>モデル検査のフラグ管理</h1>
 <ul>
 <li>モデル検査を行う際に全ての状態を網羅的に実行していく、この時実行した状態にフラグを立てていくことによって走った状態を記録しておく。</li>
 <li>フラグはeating のt_eating と、¬◇ eating　の f_F_eating フラグの2種類で、食事中といつか食事できないを表している。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="24" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="24" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="24" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
-<h1>DPP　のメタ計算</h1>
+<h1>DPP のメタ計算</h1>
 <ul>
 <li>導出木を作る時にはノーマルレベルの putdown_lfrok は　putdown_lforkPhilsImpl となり、context に代入を行うマクロである Gearef を使いCaS を行う。<br />
 その後 mcMeta に以降することで導出木の作成を行う</li>
 </ul>
 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>__code putdown<span class="hljs-constructor">_lfork(<span class="hljs-params">struct</span> PhilsImpl<span class="hljs-operator">*</span> <span class="hljs-params">phils</span>, <span class="hljs-params">__code</span> <span class="hljs-params">next</span>(<span class="hljs-operator">...</span>)</span>) {
 <span class="hljs-constructor">Gearef(<span class="hljs-params">context</span>, AtomicT_int)</span>-&gt;next = C_thinkingPhilsImpl;
 goto mc<span class="hljs-constructor">Meta(<span class="hljs-params">context</span>, <span class="hljs-params">left_fork</span>-&gt;<span class="hljs-params">set</span>)</span>;
 }
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="25" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="25" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="25" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>mcDPP</h1>
 <ul>
 <li>フラグを確認しモデル検査を行っている。</li>
 </ul>
 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap>void mcDPP(struct MCTaskManagerImpl* mcti, struct MCWorker* mcWorker, StateDB now,StateDB next, int check) {
 }
 }
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="26" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="26" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="26" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1><a href="http://meta.pm">meta.pm</a></h1>
 <pre><code><svg data-marp-fitting="svg" data-marp-fitting-code><foreignObject><span data-marp-fitting-svg-content><span data-marp-fitting-svg-content-wrap><span class="hljs-function"><span class="hljs-keyword">sub</span> <span class="hljs-title">replaceMeta</span> </span>{
 <span class="hljs-keyword">return</span> (
 [<span class="hljs-regexp">qr/PhilsImpl/</span> =&gt; \&amp;generateMcMeta],
 );
 }
 <span class="hljs-number">1</span>;
 </span></span></foreignObject></svg></code></pre>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="27" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="27" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="27" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="27" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>まとめ</h1>
 <ul>
 <li>
 <p>GearsOS上でDPPからの導出木を生成した。</p>
 </li>
 <li>
 <p>GeearsOS で汎用モデル検査器を作ることができた。</p>
 </li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="28" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="28" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="28" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
-<h1>モデル検査における問題点</h1>
-<ul>
-<li>他のアプリケーションと違い、OS の記述はそれ自体が メタレベルのものであるため、それをemulationする方法を考える必要がある。</li>
-<li>TLB(Translation Lookaside Buffer ) という仮想記憶を物理アドレスに変換する際に使われるキャッシュ機能があり、これのemulation に工夫が必要となる。</li>
-<li>検証内容によってこれらのemulation の方法をチューニングするため、未知のメタ計算、またはバグに対する検証方法が必要となる。<br />
--ユーザーcontext が単純であっても OS は膨大な状態数を有するので、その全てを探索するのが厳しいと考えられる。</li>
-</ul>
-</section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="29" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="29" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
 <h1>今後の展開</h1>
 <ul>
 <li>
 <p>網羅的にプログラムを走破し、状態を展開して行くため同じ状態の組み合わせが出てくる。これらの組み合わせは抽象化し、状態数が増えすぎる事を抑える必要がある。</p>
 </li>
 <li>
 <p>モデル検査でメモリの状態を保管していたiterator は実行履歴として、trace によって遡る事が可能であるため、これを利用することによってmcMeta にdebugger  を埋め込むことが可能であると考える。</p>
 </li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="30" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="30" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="29" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="29" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
 <h1>GearsOS の GearsOS によるモデル検査</h1>
 <ul>
 <li>GerasOS そのものも codeGear で記述されている。</li>
 <li>CPU毎の C.context、共有するkernel のK.context、ユーザープログラムのU.context と考えることができ、これらはmeta dataGear であるK.context に含まれている。</li>
 <li>U.context がDPPのような単純なものならば、OS全体のcontext も複雑にはならないため、これらをGearsOSで実行することが可能になる。</li>
 <li>GearsOS を含む codeGear のシャッフル実行を行う事ができれば、DPPと同じようにモデル検査を行う事ができる。</li>
 <li>検査する codeGear と検査される codeGear は同じものであるが、実行する meta codeGear を異なる。。</li>
 <li>異なるmeta codeGear を指定してコンパイル出来る。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="31" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="31" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="30" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="30" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
-<h1>OS 自体のモデル検査</h1>
+<h1>OS のモデル検査における問題点</h1>
 <ul>
-<li>
+<li>他のアプリケーションと違い、OS の記述はそれ自体が メタレベルのものであるため、それをemulationする方法を考える必要がある。</li>
-<p>Gears OS は CbC で書かれている。そのため OS の動作であってもメタ計算を挟む事が可能である。</p>
+<li>TLB(Translation Lookaside Buffer ) という仮想記憶を物理アドレスに変換する際に使われるキャッシュ機能があり、これのemulation に工夫が必要となる。</li>
-</li>
+<li>検証内容によってこれらのemulation の方法をチューニングするため、未知のメタ計算、またはバグに対する検証方法が必要となる。<br />
-<li>
+-ユーザーcontext が単純であっても OS は膨大な状態数を有するので、その全てを探索するのが厳しいと考えられる。</li>
-<p>CPU や kernel また ユーザープログラムのcontext として考える事によって、OS から独立しているものとして考える。</p>
+</ul>
-</li>
+</section>
-<li>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="31" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="31" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;">
-<p>またユーザーのcontext が単純なものであれば、OS 全体も複雑にはならないためDPPのようにシャッフル実行を行う事で、検証が可能であると考えられる。</p>
-</li>
-</ul>
-</section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="32" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="32" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;">
 <h1>OS のモデル検査</h1>
 <ul>
 <li>OS の全体を検証するのではなく、部分的な検証であればモデル検査出来ると考えられる。</li>
 <li>また小林らによって高次元プログラムの最悪時間計算量がｋ階の場合にｋ重指数完全であった高階モデル検査についての高速化手法が研究されている。</li>
 </ul>
 </section>
-</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="33" data-paginate="true" data-theme="acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit" data-marpit-pagination="33" data-marpit-pagination-total="33" style="--paginate:true;--theme:acn9kdsownv3qktq5ia9i2bs7upcykbh3dw5lzikit;"></section>
+</foreignObject></svg><svg data-marpit-svg="" viewBox="0 0 1280 720"><foreignObject width="1280" height="720"><section id="32" data-paginate="true" data-theme="vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr" data-marpit-pagination="32" data-marpit-pagination-total="32" style="--paginate:true;--theme:vygowizw7jkc3o2t6dqw8a8i743ms7eq75s99my3yr;"></section>
 <script>!function(){"use strict";function t(t){Array.from(document.getElementsByTagName("svg"),e=>{if(e.hasAttribute("data-marpit-svg")){const{clientHeight:r,clientWidth:a}=e;e.style.transform||(e.style.transform="translateZ(0)");const o=t||e.currentScale||1,i=e.viewBox.baseVal.width/o,n=e.viewBox.baseVal.height/o,s=Math.min(r/n,a/i);Array.from(e.querySelectorAll(":scope > foreignObject"),t=>{const e=t.x.baseVal.value,o=t.y.baseVal.value;Array.from(t.querySelectorAll(":scope > section"),t=>{t.style.transformOrigin||(t.style.transformOrigin="0 0");const l=(a-s*i)/2-e,c=(r-s*n)/2-o;t.style.transform=`translate3d(${l}px,${c}px,0) scale(${s}) translate(${e}px,${o}px)`})})}})}const e=(t,e,r)=>{if(t.getAttribute(e)!==r)return t.setAttribute(e,r),!0};function r(a=!0){for(const e of"Apple Computer, Inc."===navigator.vendor?[t]:[])e();Array.from(document.querySelectorAll('svg[data-marp-fitting="svg"]'),t=>{const r=t.firstChild,a=r.firstChild,{scrollWidth:o,scrollHeight:i}=a;let n,s=1;if(t.hasAttribute("data-marp-fitting-code")&&(n=t.parentElement.parentElement),t.hasAttribute("data-marp-fitting-math")&&(n=t.parentElement),n){const t=getComputedStyle(n),e=Math.ceil(n.clientWidth-parseFloat(t.paddingLeft)-parseFloat(t.paddingRight));e&&(s=e)}const l=Math.max(o,s),c=Math.max(i,1),p=`0 0 ${l} ${c}`;e(r,"width",""+l),e(r,"height",""+c),e(t,"preserveAspectRatio",getComputedStyle(t).getPropertyValue("--preserve-aspect-ratio")||"xMinYMin meet"),e(t,"viewBox",p)&&t.classList.toggle("__reflow__")}),a&&window.requestAnimationFrame(()=>r(a))}!function(){if("undefined"==typeof window)throw new Error("Marp Core's browser script is valid only in browser context.");window.marpCoreBrowserScript?console.warn("Marp Core's browser script has already executed."):(Object.defineProperty(window,"marpCoreBrowserScript",{value:!0}),r())}()}();
 </script></foreignObject></svg></div><script>!function(){"use strict";var e=function(e,t){var n,r=1===(e.parent||e).nodeType?e.parent||e:document.querySelector(e.parent||e),s=[].filter.call("string"==typeof e.slides?r.querySelectorAll(e.slides):e.slides||r.children,(function(e){return"SCRIPT"!==e.nodeName})),a={},o=function(e,t){return(t=t||{}).index=s.indexOf(e),t.slide=e,t},i=function(e,t){a[e]=(a[e]||[]).filter((function(e){return e!==t}))},l=function(e,t){return(a[e]||[]).reduce((function(e,n){return e&&!1!==n(t)}),!0)},c=function(e,t){s[e]&&(n&&l("deactivate",o(n,t)),n=s[e],l("activate",o(n,t)))},d=function(e,t){var r=s.indexOf(n)+e;l(e>0?"next":"prev",o(n,t))&&c(r,t)},u={off:i,on:function(e,t){return(a[e]||(a[e]=[])).push(t),i.bind(null,e,t)},fire:l,slide:function(e,t){if(!arguments.length)return s.indexOf(n);l("slide",o(s[e],t))&&c(e,t)},next:d.bind(null,1),prev:d.bind(null,-1),parent:r,slides:s,destroy:function(e){l("destroy",o(n,e)),a={}}};return(t||[]).forEach((function(e){e(u)})),n||c(0),u};function t(e){e.parent.classList.add("bespoke-marp-parent"),e.slides.map(e=>e.classList.add("bespoke-marp-slide")),e.on("activate",t=>{e.slides.map(e=>e.classList.remove("bespoke-marp-active")),t.slide.classList.add("bespoke-marp-active")})}function n(e=2e3){return t=>{let n;function r(){n&&clearTimeout(n),n=setTimeout(()=>{t.parent.classList.add("bespoke-marp-inactive")},e),t.parent.classList.remove("bespoke-marp-inactive")}document.addEventListener("mousedown",r),document.addEventListener("mousemove",r),document.addEventListener("touchend",r),setTimeout(r,0)}}const r=["AUDIO","BUTTON","INPUT","SELECT","TEXTAREA","VIDEO"];function s(e){e.parent.addEventListener("keydown",e=>{if(!e.target)return;const t=e.target;(r.includes(t.nodeName)||"true"===t.contentEditable)&&e.stopPropagation()})}function a(e){window.addEventListener("load",()=>{for(const t of e.slides){const e=t.querySelector("[data-marp-fitting]")?"":"hideable";t.setAttribute("data-bespoke-marp-load",e)}})}function o(e){let t=0,n=0;Object.defineProperty(e,"fragments",{enumerable:!0,value:e.slides.map(e=>[null,...e.querySelectorAll("[data-marpit-fragment]")])});const r=r=>void 0!==e.fragments[t][n+r],s=(r,s)=>{t=r,n=s,e.fragments.forEach((e,t)=>{e.forEach((e,n)=>{if(null==e)return;const a=t<r||t===r&&n<=s;e.setAttribute("data-bespoke-marp-fragment",a?"active":"inactive"),t===r&&n===s?e.setAttribute("data-bespoke-marp-current-fragment","current"):e.removeAttribute("data-bespoke-marp-current-fragment")})}),e.fragmentIndex=s;const a={slide:e.slides[r],index:r,fragments:e.fragments[r],fragmentIndex:s};e.fire("fragment",a)};e.on("next",()=>{if(r(1))return s(t,n+1),!1;const a=t+1;e.fragments[a]&&s(a,0)}),e.on("prev",()=>{if(r(-1))return s(t,n-1),!1;const a=t-1;e.fragments[a]&&s(a,e.fragments[a].length-1)}),e.on("slide",({index:t,fragment:n})=>{let r=0;if(void 0!==n){const s=e.fragments[t];if(s){const{length:e}=s;r=-1===n?e-1:Math.min(Math.max(n,0),e-1)}}s(t,r)}),s(0,0)}var i,l=function(e,t){return e(t={exports:{}},t.exports),t.exports}((function(e){
 /*!
 * screenfull
 * v5.0.2 - 2020-02-13

Mercurial > hg > Papers > 2021 > ikkun-master

comparison poster/poster.html @ 4:3139ed741e26