annotate prepaper/pre.tex @ 18:e8a0f9380734

paper fix
author okud
date Mon, 15 Feb 2021 21:10:15 +0900
parents 7aa7bb77556c
children 0dd66a59256b
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
9
okud
parents:
diff changeset
1 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
okud
parents:
diff changeset
2 \usepackage[dvipdfmx]{graphicx}
okud
parents:
diff changeset
3 \usepackage{picins}
okud
parents:
diff changeset
4 \usepackage{fancyhdr}
okud
parents:
diff changeset
5 \usepackage{abstract}
okud
parents:
diff changeset
6 \usepackage{here}
okud
parents:
diff changeset
7 \usepackage{url}
okud
parents:
diff changeset
8 \usepackage{listings,jlisting}
okud
parents:
diff changeset
9 %\pagestyle{fancy}
okud
parents:
diff changeset
10 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{pic/emblem-bitmap.pdf}}琉球大学主催 工学部工学科知能情報コース 卒業研究発表会}
okud
parents:
diff changeset
11 \rhead{}
okud
parents:
diff changeset
12 \cfoot{}
okud
parents:
diff changeset
13
okud
parents:
diff changeset
14 \setlength{\topmargin}{-1in \addtolength{\topmargin}{15mm}}
okud
parents:
diff changeset
15 \setlength{\headheight}{0mm}
okud
parents:
diff changeset
16 \setlength{\headsep}{5mm}
okud
parents:
diff changeset
17 \setlength{\oddsidemargin}{-1in \addtolength{\oddsidemargin}{11mm}}
okud
parents:
diff changeset
18 \setlength{\evensidemargin}{-1in \addtolength{\evensidemargin}{21mm}}
okud
parents:
diff changeset
19 \setlength{\textwidth}{181mm}
okud
parents:
diff changeset
20 \setlength{\textheight}{261mm}
okud
parents:
diff changeset
21 \setlength{\footskip}{0mm}
okud
parents:
diff changeset
22 \pagestyle{empty}
okud
parents:
diff changeset
23
okud
parents:
diff changeset
24 \renewcommand{\abstractname}{Abstract}
okud
parents:
diff changeset
25 \begin{document}
17
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
26 \title{GearsOSのBootに関する研究}
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
27 \author{175733E 氏名 {奥田光希}\\ 指導教員 : {河野 真治} }
9
okud
parents:
diff changeset
28 \date{}
okud
parents:
diff changeset
29 \twocolumn [
okud
parents:
diff changeset
30 \maketitle
okud
parents:
diff changeset
31 \begin{onecolabstract}
17
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
32 We are proposing GearsOS, which uses Meta-calculus to improve reliability in our lab.
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
33 We are implementing GearsOS on Raspberry Pi based on x.v6.
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
34 Currently, GearsOS is booted from BIOS, and we would like to migrate it to UEFI.
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
35 If we can migrate to UEFI, we can avoid dependencies on CPU and other devices.
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
36 GearsOS is written in CbC (Continuation based C), so it is not affected by CPU or device.
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
37 This will make it possible to apply GearsOS to a variety of embedded systems.
9
okud
parents:
diff changeset
38 \end{onecolabstract}]
okud
parents:
diff changeset
39 \thispagestyle{fancy}
okud
parents:
diff changeset
40
okud
parents:
diff changeset
41 \section{はじめ}
17
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
42 2017年、Intel社は2020年までにLegacy BIOSとUEFIへの互換を非推奨とし、互換モジュールのCSMを削除すると発表した。\cite{IntelNews}
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
43 Legacy BIOSはPCの進化に伴い、致命的な問題点が発生する。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
44 問題点の一つとして、拡張性がないことがあげられる。EthernetやUSBにつながるディスクなど、新たにブートデバイスが追加されるたびに,
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
45 OSのブートローダを変更しなければならない。またマザーボードごとに、ファームウェアをアセンブラで開発する必要がある。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
46 また、1MBのメモリ制限により、セキュリティを含めたシステム機能の強化が困難であるためセキュリティにも問題がある。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
47 これらの問題を解決するためにUEFIが開発された。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
48 UEFIは、2TBを超える大きなディスクからブートでき、高速にブートできる。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
49 CPUに依存しないアーキテクチャとドライバを持ちネットワークも使用可能な柔軟なプレOS環境が利用できる。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
50 今後、Legacy BIOSからUEFIへの移行が急速に進むだろう。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
51 また、UEFIはApplicationを持っていて、それはC言語などの高級言語で記述可能なので個人で開発がしやすい。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
52
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
53 当研究室では、信頼性と拡張性をテーマにGearsOSを開発している。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
54 GearsOSはContinuation based C(CbC)によってアプリケーションとOSそのものを記述している。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
55 現在、CbCで証明可能なOSを実装するために、xv6のCbCの書き換えを行っている。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
56 xv6は Legacy OSなため、UEFIから起動することができない。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
57 UEFIからxv6を起動させることができれば、拡張性が大きく広がる。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
58 さらに、UEFIは接続されているデバイスの認識を持てるので、マウスやキーボードを使えるように
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
59 UEFI Applicationを使い、デバイスドライバを作れる。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
60 これにより、利便性もよくなる。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
61 本研究では、ARMで動くシングルコンピュータであるRaspberryPi上にUEFIからGearsOSをブートさせることにより
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
62 様々な組み込みシステムに対してGearsOSを応用できる様にすることである。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
63
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
64 \section{Continuation based C(CbC)}
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
65 Continuation based C(CbC)\cite{CbC}は、当研究室で開発を行っているプログラミング言語である。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
66 CbCは、C言語の下位言語であり、関数呼び出しではなく継続を導入している。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
67 CbCでは、関数の代わりにCodeGearという単位でプログラミングを行う。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
68 CodeGearは入力と出力を持ち、CbCでは引数が入出力になっている。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
69 CodeGearから次のCodeGearへとgotoによる継続で遷移して処理を行い、引数として出力を与える。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
70
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
71
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
72 \subsection{CbC GCC ARM CrossCompile}
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
73 GCC上で実装されたCbCのARM CrossCompile環境をSingularity\cite{singularity}で構築した。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
74 CrossCompileは、Compilerが動作している以外のプラットフォーム向けに
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
75 実行ファイルを生成する機能を持ったCompile手法である。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
76 これにより、CbCで実装されたプログラムをRaspberry Pi上で実装ができる様になった。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
77
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
78 \section{GearsOS}
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
79 GearsOS\cite{Gears}は当研究室で信頼性と拡張性をテーマに開発を行っているOSである。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
80 GearsOSはContinuation based C(CbC)によって記述されている。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
81 当研究室では、GearsOSの信頼性とCbCの有効性を示すために、基本的な機能を揃えたOSであるxv6\cite{xv6}をCbCで置き換えを行っている。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
82 これにより、OSの個々のシステムコールが持つ状態を明確にすることができると考えている。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
83 CbCで書き換えられたxv6をRaspberry Pi\cite{raspi}に搭載することでハードウェア上でのメタレベルの計算や並列実行を行える様になる。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
84
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
85
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
86 \section{UEFI}
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
87 UEFI\cite{uefi}は、OSとプラットフォームファームウェアの間のソフトウェアインタフェースを定義する仕様である。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
88 UEFIは、インタフェース仕様であるため、特定のプロセッサに依存しない。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
89 C言語などの高級言語で実装することができ、個人でも開発の難易度が低い。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
90
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
91
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
92 UEFIにはApplicationがあり、UEFI Applicationは開発を行うマシンのOSやアーキテクチャに左右されることなく、
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
93 高級言語から直接生成することができる。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
94 UEFI Applicationを自作することにより、xv6をUEFIでBootさせるBootLoaderを作ったり、xv6のデバイスドライバを作れる様になる。
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
95
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
96 \section{BootLoader}
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
97
9
okud
parents:
diff changeset
98
okud
parents:
diff changeset
99
okud
parents:
diff changeset
100 \begin{thebibliography}{9}
17
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
101 \bibitem{IntelNews} Intel/Unified EFI Forum, https://www.uefi.org ,2017/11/3.
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
102 \bibitem{CbC} 清水隆博,河野慎治..xv6の構成要素の継続の分析.情報処理学会研究報告,2020.
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
103 \bibitem{singularity} https://sylabs.io/singularity
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
104 \bibitem{Gears} 東恩納 琢偉,河野真治.Gears OSでモデル検査を実現する手法について.情報処理学会研究報告2020
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
105 \bibitem{xv6} Russ Cox, M Frans Kaashoek, and Robert Morris. Xv6, a simple unix-like teaching operating system,2012.
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
106 \bibitem{raspi} https://www.raspberrypi.org
7aa7bb77556c pre slide add
okud
parents: 9
diff changeset
107 \bibitem{uefi} https://wiki.osdev.org/UEFI
9
okud
parents:
diff changeset
108 \end{thebibliography}
okud
parents:
diff changeset
109
okud
parents:
diff changeset
110
okud
parents:
diff changeset
111
okud
parents:
diff changeset
112 \nocite{*}
okud
parents:
diff changeset
113 \bibliographystyle{junsrt}
okud
parents:
diff changeset
114 \bibliography{reference}
okud
parents:
diff changeset
115 \end{document}