Skip to content

Instantly share code, notes, and snippets.

View 4ge32's full-sized avatar

Fumiya Shigemitsu 4ge32

17 followers · 13 following
  • Japan
View GitHub Profile
@4ge32
4ge32 / 形式検証ネタサーベイ
Last active February 16, 2021 13:32
# 参考文献
## 事例系
[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ベースにどうシステムをセキュリティを担保したかという話。重要なこととして、
@4ge32
4ge32 / futex.cpp
Created November 9, 2020 11:16
#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>
@4ge32
4ge32 / concurrent_template.cpp
Created November 5, 2020 13:22
// 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);
@4ge32
4ge32 / lfstack.md
Created October 8, 2020 13:05

SPINを用いてABA問題を検証する

概要

ロックフリーアルゴリズムとは，正確には進行性が保証されるアルゴリズムのことをいう．Compare and Swap命令(CAS)を主軸として実装する．

ロックフリーアルゴリズムにおいて，有名な問題としてABA問題がある．ABA問題の解決方法はいくつかあり，それぞれに特徴がある．今回は，タグ付きポインタとload-link/store-conditional(ll/sc)バージョンでのCASといった2つの解決方法について検証する．

最初に，ロックフリーアルゴリズムのなかで最も基本的なロックフリースタックをC言語で実装する．そして，それをPromelaでSPINのモデルとして記述する．

@4ge32
4ge32 / LinuxKernelBuild.md
Last active August 11, 2020 14:29

Run the Linux kernel and Busybox on QEMU

AArch64

Build Linux kernel

make ARCH=aarch64 menuconfig
make CROSS_COMPILE=aarch64-linux-gnu- -j8

Build Busybox

@4ge32
4ge32 / Linuxシグナルハンドリング.md
Created February 26, 2020 03:07

シグナル

Call tree

  • pthread_kill(3)などはtgkill(2)を用いて実装されている

シグナル生成&配送

SYSCALL_DEFINE(tgkill)
- do_tkill
@4ge32
4ge32 / Makefile.patch
Created August 30, 2019 11:39
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,$^)
@4ge32
4ge32 / A fork() in the road を読んで.md
Created April 22, 2019 10:57

A fork() in the road を読んで

HotOS 2019 で Microsoft Research からの論文である．Unixの代表的なシステムコールであるfork()についての問題点を挙げている．

概要

fork()は最も基本的なシステムコールといっても良く，新しいプロセスを作るときに使われる．今回の論文の主張はfork()は1970年代のマシンではハックと呼べるものだったが，現代では過去の負債となっているというものでおり，カーネルから完全に取り除くべきであるというものである．ただし，ここでいうカーネルとはLinuxカーネルのことを直接指しているのではなく，著者の先行研究でのOSの実装のことを指している．

面白いのは，fork()は研究者にとっては研究を阻害するといったことや，教育者は歴史としては教えるべきだが最初に教わるべきプロセス作成の仕組みとしてはふさわしくないといった中々過激なことを言っているところである．

問題点

現代的なコンピュータシステムにおける問題点として次のようなことが挙げられている．

  • かつてはシンプルであったが，最早そうではない
  • 25もの特別なケースが親プロセスの状態を子プロセスにコピーするときに存在する．例えば，ファイルロック，タイマー，非同期IOやトレーシングなど．また，コピー後のメモリマッピングに関して，madvice()に与えるフラグも非常に多いものとなっている．
@4ge32
4ge32 / pmem_as_systemram-memo.md
Last active March 17, 2019 18:20

  • 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

@4ge32
4ge32 / README-ja.md
Last active February 20, 2019 08:56
環境の作り方とAEONの試し方

前提条件

基本的にはFedora28以上を入れておくのが一番簡単かと思います． Linuxカーネルはバージョンが4.17.19以上である必要があります． Linuxカーネルは以下のコンフィグが有効になっている必要があります． 最近の一般的なディストリビューションだと有効になっていることが多いとは思いますが， 自前でカーネルをビルドする場合や機能が有効にならない場合は有効化・確認をする必要があります．

CONFIG_BLK_DEV_RAM_DAX=y
CONFIG_FS_DAX=y
CONFIG_X86_PMEM_LEGACY=y