umedaikiti

#include<linux/module.h>
#include<linux/kernel.h>
#include<linux/blkdev.h>

//ブロックデバイスを作ってみたくて試行錯誤しながら書いた
//とりあえず動作することを目標にしたので中身はいい加減

#define MODNAME "blkdevtest"

#define CAPACITY_SECTOR 1024

umedaikiti

#試すときは
#sudo ruby fusefstest.rb <mountpoint>
#ls, mkdir, rmdir, cat, mv, vi, nanoとかは多分使える
#終わったら sudo umount <mountpoint>

#エラーのときにどうすればいいかわからない
#raise Errno::E*** は意味無さそう

#タイムスタンプやパーミッションの扱い方はわからない
#今のところtouchやchmod, chownなどのコマンドは使えない

umedaikiti

all: fusetest

fusetest: fusetest.c
	gcc -Wall fusetest.c `PKG_CONFIG_PATH=/usr/lib/i386-linux-gnu/pkgconfig/ pkg-config fuse --cflags --libs` -o fusetest

.PHONY: clean
clean:
	rm -f fusetest

umedaikiti

ifneq ($(KERNELRELEASE),)
obj-m := my_vfs.o
my_vfs-objs := my_vfs_module.o
else
KVER = $(shell uname -r)
KDIR = /lib/modules/$(KVER)/build

modules::
	$(MAKE) -C $(KDIR) M=$(shell pwd) modules

umedaikiti

obj-m = proctest.o
KVERSION = $(shell uname -r)
all:
	make -C /lib/modules/$(KVERSION)/build M=$(PWD) modules
clean:
	make -C /lib/modules/$(KVERSION)/build M=$(PWD) clean

umedaikiti

Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros.
  apply H0.
  apply H.
Qed.

umedaikiti

Coqタクティックサンプル集

• インデントは雑
• 証明を終わらせていないものもある

umedaikiti

Linux-PAM

PAMとは

• Pluggable Authentication Module
• 認証処理を行うモジュール群とそれを利用するためのAPIからなるユーザー認証システム
• http://www.linux-pam.org/ のドキュメントでは認証処理を行うモジュールをLinux-PAM Module、APIを利用するアプリケーションをLinux-PAM Applicationと呼んでいる

モジュールの例

Chapter 6. A reference guide for available modules

pam_unix

linuxでログインするとき/etc/passwdや/etc/shadowを見て認証を行う

umedaikiti

Require Import Relations Setoid Morphisms.
Require Import ssreflect seq fintype.

Section Automaton.

Variable char : finType.
Definition word := seq char.

Definition RightInvariant (R : relation word) : Prop :=
  equiv word R /\ forall (x y : word), R x y -> forall z : word, R (x++z) (y++z).

umedaikiti

kmp: kmp.c
	gcc kmp.c -o kmp