# HG changeset patch
# User anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
# Date 1588219839 -32400
# Node ID 8f1d03a81516a8e727115d01cac278ce4972d244
# Parent  a916d03dd4c55c8b264b89bb95dd8d3fc52549e1
add md2tex

diff -r a916d03dd4c5 -r 8f1d03a81516 paper/Makefile
--- a/paper/Makefile	Wed Apr 29 16:21:45 2020 +0900
+++ b/paper/Makefile	Thu Apr 30 13:10:39 2020 +0900
@@ -11,7 +11,10 @@
 #DVIPSOPT   = -D 720 -mode esphi -O 0mm,0mm -N0 
 
 #  Suffixes definitions
-.SUFFIXES: .tex .dvi .pdf
+.SUFFIXES: .md .tex .dvi .pdf
+
+.md.tex:
+	perl md2tex.pl $(TARGET).md > $(TARGET).tex
 
 .tex.dvi:
 	$(LATEX) $<
diff -r a916d03dd4c5 -r 8f1d03a81516 paper/anatofuz-sigos.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/anatofuz-sigos.md	Thu Apr 30 13:10:39 2020 +0900
@@ -0,0 +1,21 @@
+# OSの信頼性
+様々なアプリケーションはOSの上で動作するのが当たり前になってきた。
+アプリケーションの信頼性を向上させるのはもとより、 土台となるOS自体の信頼性は高く保証されていなければならない。
+OSそのものも巨大なプログラムであるため、 テストコードを用いた方法で信頼性を確保する事が可能である。
+しかし並列並行処理などに起因する動かしてみないと発見できないバグなどが存在するため、 テストで完全にバグを発見するのは困難である。
+また、OSを構成する処理も巨大であるため、 これら全てをテスト仕切るのも困難である。
+テスト以外の方法でOSの信頼性を高めたい。
+
+数学的な背景に基づく形式手法を用いてOSの信頼性を向上させることを検討する。
+OSを構成する要素をモデル検査してデッドロックなどを検知する方法や、 定理証明支援系を利用した証明ベースでの信頼性の確保などの手法が考えられる。
+形式手法で信頼性を確保するには、 まずOSの処理を証明などがしやすい形に変換して実装し直す必要がある。
+これに適した形として、 状態遷移モデルが挙げられる。
+OSの内部処理の状態を明確にし、 状態遷移モデルに落とし込むことでモデル検査などを通して信頼性を向上させたい。
+既存のOSはそのままに処理を状態遷移モデルに落とし込む為には、 まず既存のOSの処理中の状態遷移を分析する必要がある。
+分析の結果を定理証明支援系などによって証明を行うか、 仕様記述言語で再実装することで仕様の整合性を検証する事が可能である。
+しかしこれらの方法では、 実際に動くOSと検証用の実装が別の物となってしまうために、 C言語などの実装の段階で発生するバグを取り除くことができない。
+実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
+
+実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。
+現在小さなunixであるxv6 kernelを状態遷移を基本とした単位でのプログラミングに適した言語、 Continuation Based Cを用いて再実装している。
+再実装の為には、 既存のxv6 kernelの処理の状態遷移を、継続を用いたプログラムに変換していく必要がある。
diff -r a916d03dd4c5 -r 8f1d03a81516 paper/anatofuz-sigos.pdf
Binary file paper/anatofuz-sigos.pdf has changed
diff -r a916d03dd4c5 -r 8f1d03a81516 paper/md2tex.pl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/md2tex.pl	Thu Apr 30 13:10:39 2020 +0900
@@ -0,0 +1,30 @@
+#!/usr/bin/env perl
+use strict;
+use warnings;
+
+{
+  open my $fh, '<', 'md2tex/first.tex';
+  while (my $line = <$fh> ) {
+    print "$line";
+  }
+  close $fh;
+}
+
+open my $fh, '<', 'anatofuz-sigos.md';
+while (my $line = <$fh>) {
+  if ($line =~/^#/) {
+    $line =~ s/# (.*)/\\section{$1}/;
+  }
+  print $line;
+}
+close $fh;
+
+print <<'EOF';
+
+\nocite{*}
+\bibliographystyle{ipsjunsrt}
+\bibliography{anatofuz-bib}
+
+
+\end{document}
+EOF
diff -r a916d03dd4c5 -r 8f1d03a81516 paper/md2tex/first.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/md2tex/first.tex	Thu Apr 30 13:10:39 2020 +0900
@@ -0,0 +1,52 @@
+%%
+%% 研究報告用スイッチ
+%% [techrep]
+%%
+%% 欧文表記無しのスイッチ(etitle,eabstractは任意)
+%% [noauthor]
+%%
+
+%\documentclass[submit,techrep]{ipsj}
+\documentclass[submit,techrep,noauthor]{ipsj}
+
+
+
+\usepackage[dvips]{graphicx}
+\usepackage{latexsym}
+
+\def\Underline{\setbox0\hbox\bgroup\let\\\endUnderline}
+\def\endUnderline{\vphantom{y}\egroup\smash{\underline{\box0}}\\}
+\def\|{\verb|}
+%
+
+%\setcounter{巻数}{59}%vol59=2018
+%\setcounter{号数}{10}
+%\setcounter{page}{1}
+
+
+\begin{document}
+
+
+\title{xv6の構成要素の継続の分析}
+
+%\etitle{How to Prepare Your Paper for IPSJ SIG Technical Report \\ (version 2018/10/29)}
+
+\affiliate{KIE}{琉球大学大学院理工学研究科情報工学専攻}
+\affiliate{IE}{琉球大学工学部工学科知能情報コース}
+
+
+\author{清水 隆博}{Shimizu Takahiro}{KIE}[anatofuz@cr.ie.u-ryukyu.ac.jp]
+\author{河野 真治}{Shinji Kono}{IE}[kono@ie.u-ryukyu.ac.jp]
+
+\begin{abstract}
+OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。
+テストを利用して信頼性を高めるのではなく、 OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高めたい。
+
+状態遷移単位での記述に適した言語であるCbCを用いて、小さなunixであるxv6 kernelの書き換えを行っている。
+このためには現状のxv6 kernelの処理がどのような状態遷移を行うのかを分析し、継続ベースでのプログラミングに変換していく必要がある。
+本稿ではxv6kernelの構成要素の一部に着目し、状態遷移系の分析と状態遷移系を元に継続ベースでxv6の再実装を行う。
+\end{abstract}
+
+
+\maketitle
+