| # 参考文献 | |
| ## 事例系 | |
| [By Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby Murray, Gernot Heiser | |
| Communications of the ACM, October 2018, Vol. 61 No. 10, Pages 68-77 | |
| Formally Verified Software in the Real World | |
| ### 要約 | |
| ボーイング社の軍用ヘリでの事例。seL4ベースにどうシステムをセキュリティを担保したかという話。重要なこととして、 |
| #ifndef _GNU_SOURCE | |
| #define _GNU_SOURCE | |
| #endif | |
| #include <atomic> | |
| #include <cstdio> | |
| #include <linux/futex.h> | |
| #include <sys/syscall.h> | |
| #include <sys/types.h> | |
| #include <thread> | |
| #include <unistd.h> |
| // The template for writing concurrent program to experiment | |
| #include <atomic> | |
| #include <cstdio> | |
| #include <thread> | |
| #include <vector> | |
| const static unsigned int producer = 1; | |
| const static unsigned int consumer = 2; | |
| static std::atomic<int> val(0); |
ロックフリーアルゴリズムとは，正確には進行性が保証されるアルゴリズムのことをいう．Compare and Swap命令(CAS)を主軸として実装する．
ロックフリーアルゴリズムにおいて，有名な問題としてABA問題がある．ABA問題の解決方法はいくつかあり，それぞれに特徴がある．今回は，タグ付きポインタとload-link/store-conditional(ll/sc)バージョンでのCASといった2つの解決方法について検証する．
最初に，ロックフリーアルゴリズムのなかで最も基本的なロックフリースタックをC言語で実装する．そして，それをPromelaでSPINのモデルとして記述する．
| diff --git a/scripts/Makefile.build b/scripts/Makefile.build | |
| index 0d434d0afc0b..63eb7ab3e06a 100644 | |
| --- a/scripts/Makefile.build | |
| +++ b/scripts/Makefile.build | |
| @@ -458,7 +458,7 @@ endif | |
| # module is turned into a multi object module, $^ will contain header file | |
| # dependencies recorded in the .*.cmd file. | |
| quiet_cmd_link_multi-m = LD [M] $@ | |
| - cmd_link_multi-m = $(LD) $(ld_flags) -r -o $@ $(filter %.o,$^) | |
| + cmd_link_multi-m = $(LD) $(ld_flags) -r -o $@ $(filter %.o %.a,$^) |
HotOS 2019 で Microsoft Research からの論文である．Unixの代表的なシステムコールであるfork()についての問題点を挙げている．
fork()は最も基本的なシステムコールといっても良く，新しいプロセスを作るときに使われる．今回の論文の主張はfork()は1970年代のマシンではハックと呼べるものだったが，現代では過去の負債となっているというものでおり，カーネルから完全に取り除くべきであるというものである．ただし，ここでいうカーネルとはLinuxカーネルのことを直接指しているのではなく，著者の先行研究でのOSの実装のことを指している．
面白いのは，fork()は研究者にとっては研究を阻害するといったことや，教育者は歴史としては教えるべきだが最初に教わるべきプロセス作成の仕組みとしてはふさわしくないといった中々過激なことを言っているところである．
現代的なコンピュータシステムにおける問題点として次のようなことが挙げられている．
PMEM as RAMがマージされた．not entirely happy らしいが，将来的な開発も含めてのことのよう．
PMEMがrepeat instructionsでエラーを起こしやすいのはブート時にRAMのようにscrubbedの必要がないから(scrubすれば良いような気もするが，memory modeだと多分されるような気がする，予想)
どうやらmcsafeを常に使ってpmemを読むらしい．ということは，System RAMだとしてもpmemがSystem ramとして登録されているということをカーネルは認識しているということになる．認識しているならmemcpy_mcsafe()が呼ばれるのはdrives/nvdimm/pmem.cから分かる．
結局memcpy_mcsafe()が遅いっていうところがannoyingということなんだろうか．それだけだったようには思えないが？
Merge tag 'devdax-for-5.1' of git://git.kernel.org/pub/scm/linux/kernel/git/nvdimm/nvdimm