master-q

= seL4
[2015-11-29 09:39]

<<< seL4

http://sel4.systems/
https://github.com/seL4
http://ssrg.nicta.com.au/projects/seL4/
https://wiki.sel4.systems/FrontPage

master-q

// $ clang++-5.0 -I/usr/lib/llvm-5.0/include -lclang clanglib.c
// $ ./a.out foo.c
#include <cstdio>
#include <iostream>
#include <clang-c/Index.h>
#include <clang-c/Platform.h>


void printDiagnostics(CXTranslationUnit translationUnit);
void printTokenInfo(CXTranslationUnit translationUnit,CXToken currentToken);

master-q

$ sudo apt-get install devscripts wget
$ sudo apt-get build-dep mlton
$ wget http://http.debian.net/debian/pool/main/m/mlton/mlton_20130715-3.dsc
$ wget http://http.debian.net/debian/pool/main/m/mlton/mlton_20130715.orig.tar.gz
$ wget http://http.debian.net/debian/pool/main/m/mlton/mlton_20130715-3.debian.tar.xz
$ dpkg-source -x mlton_20130715-3.dsc
$ ls
mlton-20130715/  mlton_20130715-3.debian.tar.xz  mlton_20130715-3.dsc  mlton_20130715.orig.tar.gz
$ cd mlton-20130715/
$ debuild -us -uc

master-q

= The 3rd French Japanese Meeting on Cybersecurity: 2017, April 24-25
[2017-04-24 09:26]

http://cyber.science-japon.org/

== 総括

インダストリー(営利企業)をまきこんで大学や研究機関が研究成果を持ち寄るのが目的の会議のようだった。

* Gallinaで書かれたMMUとコンテキストスイッチのみを司るkernelの開発と検証

master-q

僕とおきらく組込みプログラミングしたい方は以下のような要項にあてはまれば転職できるらしいです。

---- エンジニア要件 -------------------

■必須
・Linux上でアプリケーション開発した経験が 3年以上ある

■以下の経験があれば尚可
・Linuxデバイスドライバ開発を行った経験がある
・Linux Kernelのポーティング経験がある事

master-q

後半だいぶついていけなくなってしますが、わかった範囲だけコメントさせてください。

* 5ページ目: 口頭で簡単に、domや△のついたイコールなどの数式の意味の説明があると良いと思いました
* 10ページ目: このスライドではCSPは「イベントによる同期型相互作用」のみを扱うと主張しているのでしょうか？
* 13ページ目: 「prefix-choice」というのはAの内どれか1つにだけイベント同期を行なうことを表わしているのでしょうか？
* 14ページ目: □演算子を使ってinとSTOPを結合していますが、STOPを単位元とした□演算子のプロセス代数の結合のイメージが実行モデルとして想像できませんでした
* 22ページ目: プロセス代数における再帰定義は必ず不動点になるのですか？通常のプログラミング言語では停止する再帰を書くために混乱しました
* 30ページ目: 「構成要素の交換」が成立することは自明ではないように思いました
* 35ページ目: 「弱模倣」というはつまり、外部から観測できるイベント列だけを比較してプロセスが同値であることを主張するのでしょうか？これはユニットテストと比較した場合の利点は何でしょうか？
* 40ページ目: guardedfun_exは仕様PNfunSpecと実装PNfunImplが等しいことを証明しているのでしょうか？これは同値性の証明なのでしょうか？それとも弱模倣の証明なのでしょうか？

master-q

$ cat main.c
#include <stdio.h>

#define __infer_assert(E) {  \
  int *s = NULL;             \
  if (!(E)) *s = 0xDEADBEEF; \
}

struct foo {
        char *p;

master-q

$ ~/src/infer-linux64-v0.8.1/infer/bin/infer --version
Infer version v0.8.1
Copyright 2009 - present Facebook. All Rights Reserved.
$ ~/src/infer-linux64-v0.8.1/infer/bin/infer -- gcc -c main.c
Starting analysis (Infer version v0.8.1)
F...
Analyzed 1 file

  No issues found  

master-q

$ gbp buildpackage -us -uc --git-ignore-new --git-verbose
gbp:debug: ['git', 'rev-parse', '--show-cdup']
gbp:debug: ['git', 'rev-parse', '--is-bare-repository']
gbp:debug: /bin/true [] []
gbp:debug: ['git', 'symbolic-ref', 'HEAD']
gbp:debug: ['git', 'show-ref', 'refs/heads/master']
gbp:debug: ['git', 'rev-parse', '--quiet', '--verify', 'HEAD']
gbp:debug: ['git', 'show-ref', 'refs/heads/pristine-tar']
gbp:debug: debuild -i -I ['-us', '-uc'] []
 dpkg-buildpackage -rfakeroot -D -us -uc -i -I

master-q

$ gbp buildpackage -us -uc --git-ignore-new --git-verbose
gbp:debug: ['git', 'rev-parse', '--show-cdup']
gbp:debug: ['git', 'rev-parse', '--is-bare-repository']
gbp:debug: /bin/true [] []
gbp:debug: ['git', 'symbolic-ref', 'HEAD']
gbp:debug: ['git', 'show-ref', 'refs/heads/master']
gbp:debug: ['git', 'rev-parse', '--quiet', '--verify', 'HEAD']
gbp:debug: ['git', 'show-ref', 'refs/heads/pristine-tar']
gbp:debug: debuild -i -I ['-us', '-uc'] []
 dpkg-buildpackage -rfakeroot -D -us -uc -i -I