RustでHello, World!

環境構築

実験用のOSはUbuntu 20.10、x86_64を想定します。

まず、Rustの環境を整えます。Rustの環境はrustupで構築できるので簡単です。Rustには大きく分けてstableとnightlyがあるのですが、今回はnightlyを利用します。具体的には以下のようにコマンドを入力するとインストールできます。

$ curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | \
  sh -s -- --default-toolchain nightly-2021-03-06 \
  --component clippy rust-src llvm-tools-preview rustfmt rls rust-analysis rustdoc -y

インストール後はenvファイルを読み込んで環境変数を設定します。

$ source $HOME/.cargo/env

次に、必要なソフトウェアをaptからインストールします。

$ sudo apt update
$ sudo apt upgrade
$ sudo apt install build-essential zsh git curl libncurses5-dev libtinfo5 clang lld fakeroot xz-utils libssl-dev bc flex libelf-dev bison llvm cpio qemu-system

Linuxカーネルコンパイル

次に、Linuxカーネルソースコードを取得します。今回は、linux-nextという次世代Linux向けの実験的なソースコードを使います。

$ git clone --depth 1 git://git.kernel.org/pub/scm/linux/kernel/git/next/linux-next.git

続いて、Linuxカーネルコンフィグを設定します。

$ cd linux-next
$ make menuconfig

設定項目は、以下の通りです。General setup ---> Rust support ---> yesと、Device Drivers ---> Character devices ---> Rust Example ---> yesは必ずオンにしておきましょう。他の項目は、以下にチェックがあれば問題ないと思います。様々なオプションをオンにしたままだと、コンパイルに時間がかかるので最小オプションにしておきましょう。

64-bit kernel ---> yes
General setup ---> Rust support ---> yes
General setup ---> Initial RAM filesystem and RAM disk (initramfs/initrd) support ---> yes
General setup ---> Configure standard kernel features ---> Enable support for printk ---> yes
Executable file formats / Emulations ---> Kernel support for ELF binaries ---> yes
Executable file formats / Emulations ---> Kernel support for scripts starting with #! ---> yes
Device Drivers ---> Generic Driver Options ---> Maintain a devtmpfs filesystem to mount at /dev ---> yes
Device Drivers ---> Generic Driver Options ---> Automount devtmpfs at /dev, after the kernel mounted the rootfs ---> yes
Device Drivers ---> Character devices ---> Rust Example ---> yes
Device Drivers ---> Character devices ---> Enable TTY ---> yes
Device Drivers ---> Character devices ---> Serial drivers ---> 8250/16550 and compatible serial support ---> yes
Device Drivers ---> Character devices ---> Serial drivers ---> Console on 8250/16550 and compatible serial port ---> yes
File systems ---> Pseudo filesystems ---> /proc file system support ---> yes
File systems ---> Pseudo filesystems ---> sysfs file system support ---> yes

つづいて、Hello Worldを出力するようにします。

./drivers/char/rust_example.rsを修正して、Hello Worldを出力するように修正します。

$ cat ./drivers/char/rust_example.rs

修正箇所は、FileOperationsの実装にTO_USEを設定し、read関数を追加します。read関数内でHello, World!を出力するようにします。具体的な修正箇所は以下の通りです。そのほかの部分は修正しなくても大丈夫です。

use kernel::{
    chrdev, condvar_init, cstr,
    file_operations::{FileOperations, File, ToUse},
    user_ptr::UserSlicePtrWriter,
    miscdev, mutex_init, spinlock_init,
    sync::{CondVar, Mutex, SpinLock},
};


impl FileOperations for RustFile {
    type Wrapper = Box<Self>;

    const TO_USE: ToUse = ToUse {
        read: true, // read関数を有効化
        write: false,
        seek: false,
        ioctl: false,
        compat_ioctl: false,
        fsync: false,
    };

    fn read(&self, file: &File, data: &mut UserSlicePtrWriter, _offset: u64) -> KernelResult { // read関数を定義
        println!("rust file: read, pos = {}", file.pos());
        if file.pos() == 0 {
            let hello = b"Hello, World!\n";
            data.write_slice(hello)?;
            Ok(())
        } else {
            Ok(())
        }
    }

    fn open() -> KernelResult<Self::Wrapper> {
        println!("rust file was opened!");
        Ok(Box::try_new(Self)?)
    }
}

コンパイルします。

$ make -j 8

busyboxコンパイル

次にbusyboxソースコードを取得します。

$ git clone git://busybox.net/busybox.git

設定します。

$ cd busybox
$ make defconfig
$ make menuconfig

設定では以下のように静的リンクのオプションをチェックします。他の設定は触らなくて大丈夫です。

Settings ---> Build Options ---> Build static binary (no shared libs) ---> yes

コンパイルしinitial RAMディスクを作成します。initial RAMディスクはlinux-nextにおいておきましょう。

$ make -j 8
$ make install
$ cd _install
$ mkdir dev proc sys
$ find . | cpio --quiet -H newc -o | gzip > ../../linux-next/initrd.img

Qemuで実行

最後に仕上げとして、Qemuで実行します。

$ cd linux-next
$ qemu-system-x86_64 -m 128M -kernel arch/x86_64/boot/bzImage -append "console=ttyS0 rdinit=/bin/sh root=/dev/ram0" -initrd initrd.img -nographic

QemuLinux起動後は、devtmpfsをマウントします。

# mount -t devtmpfs devtmpfs /dev

最後に、/dev/rust_miscdevファイルをcatして、Hello, World!を出力します。

# cat /dev/rust_miscdev
[ 4362.809581] rust file was opened!
[ 4362.809787] rust file: read, pos = 0
Hello, World!
[ 4362.810056] rust file: read, pos = 14

素晴らしい!Rustで無事にHello, World!を出力することが出来ました。

シン・エヴァンゲリオン劇場版を視聴した(ネタバレあり感想)

最近、眉をしかめることがあった。研究室には事務作業をしてくれる事務の方が居るが、自分で取ってきた研究費を用いた物品調達は研究室事務に依頼するのを禁止された。ボスの研究費のみ依頼可能らしい。なるほど。まあいいだろう。これぐらいのハラスメントは日常茶飯事だ。見るがいい、これがアカデミアだ。

そんなもやもやを抱えながら、シン・エヴァンゲリオン劇場版を観に行った。エヴァとは付き合いが長い。もうかれこれ25年ぐらいだ。当時の友人が筋金入りのオタクで、その友人宅でエヴァを見た。すぐにはまった。旧劇を見るために、午前4時から映画館に並んだ。当時はインターネット予約といった先進的なシステムは無く、並んでチケットを買ったものだ。映画のチケットを買うとレイかアスカのテレフォンカードを購入できるのだが、迷わずレイを選んだ。友人は当然のごとくチケットを2毎購入し、レイとアスカの両方を手に入れていた。どっちつかずの八方美人はいけない。本命に絞って購入するのが男だ。Airは良い。アスカの覚醒シーンは最高の一言だ。まごころを、君には良くわからなかった。しかし、納得できないという気持ちの一方、やっぱりエヴァだったなという安心感もあった。エヴァはこうでなくては。

序、破も最高に面白い。これがエンターテインメントだ。シン・ゴジラも良かった。アニメの監督がここまで面白い実写映画をつくれるとは思ってもみなかった。しかしQは何だ。意味不明だ。ヴンダーとは?いきなりの艦隊戦はエヴァとは違うのではいか?そんな思いが巡ったが、その一方で、やはりエヴァだなと妙に納得している自分もいた。エヴァはやはりこうで無いといけない。普通の終わり方などあり得ない。これこそがエヴァお家芸で、これだからこそこれだけ長く愛されているのだ。完全に調教済みである。

シン・エヴァンゲリオン劇場版を観に行った。エヴァが終わると聞いていたが、にわかには信じられなかった。エヴァが終わる?本当に?あのエヴァだぞ。そう思いながらIMAXシアターの席に座っていた。映画が始まる。冒頭のシーンはAmazon Prime Videoで視聴済みだ。前日、前々日に序・破・Qも再履修した。

シーンが移り変わり、綾波が農作業していた。あの綾波が。私は人形じゃ無いと言っていた、どう見ても人形の綾波が、おはよう、おやすみ、こんにちは、さようならとあいさつをしている。綾波は魔法の言葉を覚えていた。あいさつするたび、ともだちが増えていっていた。なんと言うことだ、あの綾波がここまでの成長をみせている。もうこの時点で涙腺は駄目になっていた。これが尊い?信仰に近い感動を表す言葉。初めての気持ち。綾波は様々な感情を学び、自分は尊いを学んだ。色々あった現実世界のもやもやなど既に忘れていた。しかし、まだ映画の前半だ。エヴァがこのまま平和に終わるわけが無い。先のことを考えると暗澹たる気分になった。

映画は続き、いよいよ終盤にさしかかる。もしかして、本当に、本当の本当におわるのか?そんな考えが頭によぎった。エヴァが終わる。それが確信に変わったとき、奇妙な感動が押し寄せる。庵野秀明監督、お疲れ様でした。そういう思いやら何やらが色々まざりあい、変な感動が押し寄せる。作品自体の面白さとか、そういう客観的な判断を下すのは既に不可能となっていた。実際、序・破・Qから見た新規の客に受ける内容かはわからない。アスカ、ゲンドウ、それぞれのキャラクターが救済されていく。輪廻転生の輪から解脱していく。ああ終わるんだな、そう思わせてからの、渚指令。さすがエヴァだ。これだよ。エヴァはこうでなくっちゃ。納得のいかない終盤シーンに、妙に納得していた。

帰り際、近くの本屋に寄った。その本屋の科学雑誌コーナーには、日経サイエンスニュートンが売られており、その間にムーが鎮座していた。綾波も成長するんだ、ムーだって成長する。そう感じた。

BLisp言語のドキュメントを作成しcrates.ioに登録してみた

BLispはRust言語で実装されたベアメタル環境で動作するシェル、API定義言語として現在研究・開発をすすめています。動機は2つあります。1つが、せっかく静的型付けで型安全なRust言語を使っているのだから、Rustと協調動作するスクリプト言語でも静的型付けで型安全になってほしいというもの。もう1つは、副作用をエフェクトシステムで分離したいというものです。後者については過去に記事を書いていますので、そちらをご覧ください。

ytakano.hatenablog.com

せっかく作ったのだから、そのドキュメントを作成しておこうと思い、簡単なものを作成しました。ドキュメントはまず英語で書いて、それをDeepLで日本語で翻訳して多少手直ししています。DeepLすごいですね。

BLisp: Lispっぽい静的型付け言語

BLisp: A Statically Typed Lisp Like Language

crates.ioへの登録

せっかくなのでcrates.ioへも登録してみようと思い、こちらにも登録してみました。

https://crates.io/crates/blisp

Cargoでは、Cargo.tomlに依存ライブラリを記述すると、crates.ioからダウンロードするのですが、このcrates.ioへの登録も非常に簡単にできることがわかりました。実は、crates.ioとgithubは連携しているのかなと勝手に想像していたのですが、全くそういうことは無く、crates.ioへパッケージを登録するのだという気づきがありました。何事もやってみるものですね。

機能アップデート

機能アップデートとしては、map、foldの基本的な関数と、OptionとResult型を内部的な関数・型として追加しています。また、多倍長整数をサポートしましたので、ベアメタルで巨大な数も扱えるようになります。

ところで、実装には、Rustのbig-integerを使ってみたのですが、ベアメタル環境にもかかわらず、Display部分でfmod関数を呼び出しているようなので、そこを回避する必要がありました。llvmのコード生成時にfmodを呼び出していそうなのですが、定かではありません。

動作としては以下のような感じとなります。no_stdで動くので、WASMでも動くのではと思っており、いずれチャレンジしてみたいところです。それでは皆さん、良いRust生活を。

f:id:ytakano:20210221155657g:plain

ベアメタルで動くBLisp

【読書メモ】哲学とは何か、ゴルギアス・テーゼ

いま、「哲学とは何か」という本を読んでいるのだが、この前半部分に出てくるゴルギアス・テーゼについて理解が難しかったので、自分なりの解釈をメモしておこうと思う。実は、「哲学とは何か」はまだ前半部分しか読んでいないが、ゴルギアス・テーゼを理解しないことには先に進めなそうなので、少し考察してみる。

 

哲学とは何か NHKブックス

哲学とは何か NHKブックス

 

 

ゴルギアス・テーゼ

ゴルギアス・テーゼとは以下の3つが成り立つという主張のことである。

  1. 何物も存在しない
  2. 何かが存在したとしても、それを認識できない
  3. 何かを認識できたとしても、それを言語化できない

これの意味することは明らかだが、これの証明(と言われているもの)は不明瞭で、本書でも詳細は語られていない。Webを検索してもいまいちな説明しか無いため、もう少し形式化して考えてみようと思う。

形式化

まず、ゴルギアス・テーゼの形式化を考えてみる。おそらく以下のようになると思う。

E(x): xは存在する

R(x): xは認識できる

L(x): xは言語化できる

  1.  \forall x\ \neg E(x)
  2.  \forall x (E(x) \rightarrow \neg R(x))
  3.  \forall x (R(x) \rightarrow \neg L(x))

述語を決めて、限量子で量化しているだけである。

何物も存在しない

1のテーゼの否定を仮定する。つまり、次を真と仮定する。

 \neg \forall x\ \neg E(x) = \exists x E(x)

何かが存在するとする。その何かは無から生まれたか、別の何かから生まれたかのどちらかである。無からは何も生まれないので、無から生まれたのは誤り。別の何かから生まれたとすると、その別の何かの誕生を証明しないといけない。別の何かの、そのまた別の何かのという論法は無限遡行と言って、これは論理的な誤りであるとされる。というわけで仮定は誤り。背理法よりテーゼ1は真となる。

無限遡行はいろいろな場所に出てくる。例えば因果律の説明で、因果律を認めるためには、物事の因果の因果の、そのまた因果をたどることが出来る必要があるが、これは無限遡行に陥る。あるいは、ある地点では原因が無くても結果が起きる必要がある。よって、因果律は認められない。

何かが存在したとしても、それを認識できない

次に2のテーゼを証明してみる。

 \forall x (E(x) \rightarrow \neg R(x))

なので、この否定が真であると仮定する。つまり、

 \neg \forall x (E(x) \rightarrow \neg R(x)) = \exists x\ \neg (E(x) \rightarrow \neg R(x)) = \exists x (E(x) \land R(x))

となる。しかし、テーゼ1より何物も存在しないのでこれは誤り。よって、背理法よりテーゼ2は正しいと証明された。テーゼ3もほぼ同じように証明される。

梵我一如

ゴルギアス古代ギリシアの哲学者であるが、古代インドのウパニシャッド哲学の梵我一如も大体同じようなことを言っている。梵(ブラフマン)は宇宙の普遍的な実在で、我々には認知できない。我(アートマン)は自身の中心的な実在であり、我々自身では認識できない。結論だけ言うと、梵と我は同じであるというのが梵我一如の教えとなる。

ギリシアとインド、全く違う土地だが、同じような結論に至っているのは面白い。ただ、どちらも我々のような凡夫にはよくわからないというのが大きな特徴である。

宇宙は無限か存在しない

無限遡行が問題なのは、この世が有限だからという前提があるからのように思える。我々の宇宙が誕生したのは138億年前と言われているが、ではこの宇宙は何から生まれて、その何かは何から生まれたかのという疑問が残る。つまり、何物かが存在する、あるいは因果律が成立するためには、多元宇宙論的な宇宙が存在して、さらにそれが無限に続く存在でなければ説明がつかない。

因果律はともかく、何物も存在しないというテーゼは受け入れがたい。我々が存在するという証明を残したのは、かの有名な「我思う、故に我あり」を残したデカルトだが、少なくともデカルトの言うように何物かが存在するならば、宇宙は無限ということになる。

以上、つらつらと書いたが単なる感想なので笑い飛ばしていただければと思う。ソワカ

2020年まとめ

コロナで大変だった。以上。

今年はずっと文章を書いていた気がする。ただそれも終盤に差し掛かってきているため、来年の頭ぐらいには終わらせたい。特に、コロナで自粛しており自宅待機が多かったため、時間的な余裕が取れて文章が進んだのが大きかった。また、文章を書いている途中で、面白いことができそうだなと思いつき、OSと言語処理系を実装して国内研究会へ発表した。こちらは手をつけ始めたばかりなので、来年にはもう少し発展させたい。

学生も研究する時間がいっぱい取れただろうなと思いきや、思いの外に進んでいなかったようだ。聞くところによると、ゲームばかりしていたか、今年はオンライン講義が多かったために課題が例年の1.5倍あったためらしい。やはり、普段と違う生活になってしまうと、色々と問題が起きるようである。

自分的には家の方が作業しやすくて、文章や研究も進むのだが、多くの人にとっては大学や、あるいは職場ではないと作業が進まないのだろうと感じる。一応、自粛期間中でもオンラインでのミーティングを行ったのだが、やはり研究指導は対面の方がやりやすい。一方、講義の方はオンラインの方が好評であったと思う。対面とオンラインの両方選択できるようにはしているが、対面に来る学生は、1〜3名だけであった。

というわけで、今年の研究成果は以下の通りとなった。

  1. Akinori Kawachi, Atsuko Miyaji, Kazuhisa Nakasho, Yiying Qi, and Yuuki Takano, "Secure primitive for big data utilization", In Atsuko Miyaji and Tomoaki Mimoto, editors, "Security Infrastructure Technology for Integrated Utilization of Big Data - Applied to the Living Safety and Medical Fields", pp. 35–63. Springer, 2020.

国際会議

  1. Seitaro Mishima, Kazuhisa Nakasho, Kousuke Takeuchi, Naohiro Hayaishi, Yuuki Takano, Atsuko Miyaji, "Development and Application of Privacy-preserving Distributed Medical Data Integration System", 2020 IEEE International Conference on Consumer Electronics-Taiwan (ICCE-Taiwan), pp. 1-2.

国内研究会

  1. Sai Veerya Mahadevan, Yuuki Takano, Atsuko Miyaji 、"PRSafe: Primitive Recursive Function Based Domain Specific Programming Language Using LLVM"、情報処理学会 コンピュータセキュリティシンポジウム 2020 (CSS 2020) 論文集、pp. 94-100、2020年10月
  2. 高野 祐輝、金谷 延幸、津田 侑、"Make TrustZone Great Again"、情報処理学会 コンピュータセキュリティシンポジウム 2020 (CSS 2020) 論文集、pp. 422-429、2020年10月
  3. 細谷 昂平、高野 祐輝、宮地 充子、"F*言語を用いたネットワークファンクションの設計と実装"、Computer Security Group (CSEC2020-03)、2020年3月
  4. 岡 大貴、高野 祐輝、鄭 振牟、宮地 充子、"ZoKratesのドメイン固有言語に対するLispベースの拡張とVariant型の提案"、Computer Security Group (CSEC2020-03)、2020年3月
  5. 西口 朋哉、宮地 充子、高野 祐輝、"セッション型を用いたアクセス制御システムの評価"、第50回情報通信システムセキュリティ研究会 (ICSS)、2020年3月
  6. 竹中 幹、高野 祐輝、宮地 充子、"XDPを用いたネットワーク型欺瞞的防御システムの設計と実装"、SCIS 2020、2020年1月
  7. 西口 朋哉、高野 祐輝、宮地 充子、"セッション型を用いたアクセスコントロール機構の設計と実装"、SCIS 2020、2020年1月

本当なら、国際会議がもう少し多く、今頃はジャーナルぐらいは行けるかなと思っていたのだが、思わぬ誤算であった。ただ、今月に学生の書いた国際会議論文がアクセプトされて来年頭に発表があり、別の国際会議論文も来年頭には投稿予定なので、来年こそは発表を増やしていきたいところである。

それでは皆さん、良いお年を。

大学でRustを教えた話

このブログ記事は、Advent Calender 2020, Rust 3、23日目の記事となります。自分は現在大学で教員をしていまして、セキュリティ系の研究室に所属しています。現在はセキュリティの講義を担当しており、そこでRust言語を教えているため、その内容を紹介しようと思います。

はじめに

皆さんご存知のようにソフトウェアの脆弱性は今でも大きな問題となっていますが、それを完全ではないにしろ根本から解決するための技術的手法として型システムが注目されています。型システムの考え自体は古くからありますが、最近ではRust言語が登場し、OSなどいわゆる低レイヤーなソフトウェアも型システムの恩恵を預かることができるようになってきました。SMTソルバや定理証明などと言った難しい(かつ面白い)手法でC言語C++言語で書かれたソフトウェアを解析する方法もありますが、セキュアソフトウェアを語る上では、現在では、まず型安全なプログラミング言語を利用するのが先決だという信念から、セキュリティの講義でRust言語を教えました。

講義の受講者は、大阪大学京都大学北陸先端科学技術大学院大学奈良先端科学技術大学院大学らの大学院生と社会人学生となっており、基本的に情報系の大学院生と社会人を対象としています。大学院の講義なので、単なるHow toを教えるのではなく、Rust言語の裏側にある理論的背景から説明するように心がけました。逆にいうと、理論的なことは教えるのですが、データコンテナやCargoなどの使い方は自習が求められる構成となっているため、ある程度は自分で調べる必要があります。

講義の内容

Rustに関する講義は以下の通りとなっています。いずれも1回90分の講義となっています。

  1. ソフトウェア技術についての概要説明(GC、型システム、様々なバグ)
  2. Rust言語について
  3. 線形論理と線形型システム
  4. 線形型システムの実装
  5. 並行プログラミングとRust
ソフトウェア技術について

まずはじめに、ソフトウェアとソフトウェアテストに関する技術について概要を説明し、以降で説明するRust言語についての立ち位置を明確にするように心がけました。この文章を読んでいる方はRust言語の存在は当たり前に知っているとは思いますが、Rust言語はまだまだマイナーな言語で、その存在すら知らなかったという学生や社会人の方も多くいらっしゃいました。その中で、他にもいろいろなプログラミング言語があるのに、何故Rustというマイナー言語を新たに学ぶ必要があるのかという手厳しい質問も頂戴しました。

これは難しい質問で、確かに、他にもOCamlHaskellと言った先駆者があり、それら言語であればRustの借用と言った複雑な機能に煩わされることも無いのは確かです(Haskellモナドが借用より簡単かと言えば難しいところですが)。ですが、現状の流れを見ると、OCamlHaskellが主流になることはしばらくは無さそうですが、RustがCやC++の代替となる可能性は十分にあり得ます。ICTインフラがますます普及し、ソフトウェアが我々の命までも支えるようになってきた昨今では、C、C++をRust等のメモリ安全な言語で置き換えることは、ソフトウェア業界の最重要課題と言っても過言ではありません。このような状況を鑑み、本講義ではRust言語を選択しました。

Rust言語の説明

ソフトウェア技術の概要を説明した後は、Rust言語についてざっと説明しました。この回で基本的な構文や、借用について説明し、コンパイルの仕方も簡単に説明しました。2回目の講義レポートでは、AArch64アセンブリの簡易版エミュレータをRust言語で実装してもらいました。簡易版ですので、命令セットは四則演算と、条件分岐だけという簡素なものですが、この課題でenum型やパターンマッチ、moveセマンティクスなどの諸概念について体感してもらいます。

実際のレポート課題としては、以下のようなアセンブリファイルを読み込んで実行するようなものとなります。エミュレータと言っても、機械語ではなくアセンブリ言語をそのまま解釈するためスクリプト言語処理系と言った方が正確かもしれません。

f:id:ytakano:20201213154920p:plain

AArch64アセンブリの課題
線形型システム

次に、線形型システムについて説明しました。ここでは、Rust言語の理論的背景的にある線形型システムについて(実際はアフィン型ですが)、線形型言語をもとに説明しました。内容的にはATTaPL (*1) の線形型言語にいくつか改良を行ったものを用いました。型付け規則から説明して、型付け規則を用いた証明まで行うため、何故Rust言語でuse after freeやdouble freeが防げるのかを、理論的な側面から理解できるようになります。

この講義のレポートでは、次のような型付けに関する証明を行ってもらいましたが、多くの学生がしっかりと証明できていました。正直、ATTaPLを独習して証明までできるようになる人は多くはいないと思うのですが、本講義を90分受講して課題にとりくむと証明できるようになっていますので、これは凄いことだと思います。

f:id:ytakano:20201213154955p:plain

線形型システムの証明

その後、線形型言語の型検査アルゴリズムを、Rustを用いて実装してもらいました。アフィン型の言語であるRustを用いて、線形型システムを実装することで、Rust言語自体がよりよくわかるようになるという寸法です。この講義よりも前に初学者にRust言語を教えたことがあるのですが、moveセマンティクスの理解に時間がかかるようでしたが、これら課題を行うと完璧に理解できます。

(*1) ATTaPL: Advanced Topics in Types and Programming Language

並行プログラミング

この講義はつい先ほど行ったものですが、ここではRustでの並行プログラミングについて説明しました。Rustは並行プログラミングについても非常によく設計されております。その実現には、借用とトレイト制約が重要な役割を果たしていますが、それらについて講義をしました。ここではRustだけではなく、クリティカルセクションやレースコンディションなどの一般的な諸概念と、アトミック命令を用いたスピンロックアルゴリズムの紹介も行います。この回でRustに関する講義は終わりになるのですが、続く回ではモデル検査機のAlloyを用いてスピンロックやRWロックアルゴリズムの検証を行っていく予定です。

以上が講義の内容となります。回数自体は多くありませんが、Rustの基礎的なところや何故Rustなのかぐらいは分かる内容ではと思います。

まとめ

本講義ではRust言語とその理論的背景となる型システムまで教えましたが、自分はプログラミング言語理論は専門ではなく、どちらかというと、OSやネットワークなどのシステムソフトウェア、並行プログラミングの実装などが専門となります。そのため、線形型などの理論をどう教えたものかと大変悩みましたが、結果的には理論と実装をバランス良く扱うことができたかなと思います。本当はOSやネットワークスタックをRustで実装するような内容にしたいのですが、しょうがありません。

世間では、「大学では古い技術しか教えていない。トヨタなどで使っている最新鋭の技術を教えるべきだ」、などと言ったご意見もありますが、本講義のように、トヨタでも少数の人しか使っていないであろう、そこそこ最新の技術も多少は教えられているのではと思います。

それでは皆さん、メリークリスマス。

Rust言語によるOSと言語処理系ができるまで

タイムライン

Rust言語で簡単なファームウェア、OS、言語処理系を作成したが、そのタイムラインはだいたい以下のようなものであった。もともとは、Rustでどの程度できるか検証するために始めた実装で、OSを作る予定ではなかったのだが、やっていくうちに面白そうなことができそうなので、どんどん作っていったら、そこそこ動くものが出来上がった。

2020年

2月13日:cargoでリポジトリ作成してgithubに登録

2月16日:シリアルコンソールへ出力

3月9日:MMUの有効化に成功

3月15日:同期処理コードを追加

3月29日:slab allocator有効化

4月2日:言語処理系の設計・実装開始

4月10日:FF7リメイク発売のためしばらく停滞

6月7日:言語処理系の実装終了

7月5日:Pine64+へ移植

8月5日:電源周りの実装開始

8月28日:電源周りの実装が一段落

9月2日:セキュアワールドとノーマルワールドのコンテキストスイッチを実装

9月16日:buddy allocator実装

所感

作ってみると、Rustにはスライスがあるため、unsafeであってもメモリの保護はかなり強力に出来るというのがわかった。また、代数的データ型もあるため、unsafeなコードであってもエラーハンドリングを忘れづらいというのも良い。ただし、グローバル変数にアクセスすると、レースコンディション関係は正真正銘unsafeとなるので、注意する必要がある。

Rust自体の難しさはそれほどなかったが、MMUや電源周りの仕様などを読み解くほうが苦労した。あとは、GICを制御できれば基本的な機能はできるはずなので、その後に隔離機構の設計・実装を行っていきたい。また、現在は、基本がCのコードで、Rustの機能をフルに活かしているとは言い難いため、そちらも改良していきたいと思っている。

ただ、いまは別の仕事をしているため、まずはそれを仕上げてからかなと思う。こちらもRustをふんだんに使っているので、仕上がったらまた公開したい。

この研究は現在は完全に個人研究で行っており、そろそろ研究予算をとってこないと色々とつらいため、何とかしたいところである。