食事する哲学者 6/3　6/10
===
19:50まで

- [x] デッドロック回避方法
- [ ] UML / Promelaのモデル
- [ ] UML
- [ ] Promela
- モデル検査の実施内容
- デッドロックの検知のみ
- 動作デモ
- [ ] javascriptをデモ　Promelaはコードのみ説明

- 苦労したこと、学んだこと
-　

---

他の観点でのテスト

- 公平性
- それぞれの哲学者が最低1回たべられること

- ライブロック
- 拡張性
- リアルタイムの哲学者増減
-

- 連続運転
- モデル検査で不安をとれる

- 他の検査について考える
- 検査方法をindex.jsに追加

- 通信系・組み込み系
- ディレイがある
- モデルの詳細化が必要になる
- クリアの仕方を考える
- この演習では通信の間でなにかあるかも

-　モデル検査が実際の現場でつかわれるか
-　沢山はないが、設計モデル検証で事例を紹介
-　AWSでの事例も公開されている
-　モデル検査よりよい方法はある？
1.　テクニック的にはツール周り使いやすくなっている
-　CPUパワーの向上によるもの
-　状態数を増やせる
2. 勉強によってツールを使わなくても気づきが得られるようになる
- 考え方が身につく
- 東証の改修対象システムの検査
- 石川先生
- モデル検査に精通する人のテストは？
- 並列/平行の観点でテストしてくれる
- プログラマが嫌がるポイントを押さえたテストができる
- パラレルの違い？
- 平行と並列の違いは
- マルチコア(パラレル)
- 真の並列操作のため、バグがふえた
-
- シングルコア(コンカレント)
- コンテキストスイッチ(プログラムの切り替え)の発生
- 真の意味での並列動作はしない

進行性検査
1 /*
2 * TOPSE-MC-20XX
3 * Dining Philosophers
4 */
5 #define PHIL_NUM (2)
6 mtype = {THINKING, HUNGRY, EATING}; /* 哲学者：思考中, 空腹, 食事中 */
7 mtype = {FORK_IN_USE, FORK_VACANT}; /* フォーク：フォーク使用中, フォーク未使用 */
8 mtype = {HAND_HOLDING, HAND_EMPTY}; /* 手：（フォークを）握っている, 空 */
9 mtype fork[PHIL_NUM]; /* フォークの状態 */
10 proctype Philosopher(int no) {
11 mtype phil = THINKING; /* 哲学者の状態の初期化 */
12 mtype hand_r = HAND_EMPTY; /* 右手状態の初期化 */
13 mtype hand_l = HAND_EMPTY; /* 左手状態の初期化 */
14 do
15 ::(phil == THINKING) -> /* 思考中 */
16 if
17 ::true -> phil = HUNGRY;
18 ::true -> skip;
19 fi;
20 ::(phil == HUNGRY) -> /* 空腹 */
21 if
22 ::(fork[no % PHIL_NUM] == FORK_VACANT) ->
23 hand_r = HAND_HOLDING;
24 fork[no % PHIL_NUM] = FORK_IN_USE;
25 fi;
26 if
27 ::(fork[(no + 1) % PHIL_NUM] == FORK_VACANT) ->
28 hand_l = HAND_HOLDING;
29 fork[(no + 1) % PHIL_NUM] = FORK_IN_USE;
30 phil = EATING;
31 :: else ->
32 hand_r = HAND_EMPTY;
33 fork[no % PHIL_NUM] = FORK_VACANT;
34 fi;
35
36 ::(phil == EATING) -> /* 食事中 */
37 if
38 ::true -> hand_r = HAND_EMPTY;
39 progress:
40 hand_l = HAND_EMPTY;
41 fork[no % PHIL_NUM] = FORK_VACANT;
42 fork[(no + 1) % PHIL_NUM] = FORK_VACANT;
43 phil = THINKING;
44 ::true -> skip;
45 fi;
46 ::true -> skip;
47 od;
48 }
49 init {
50 int i;
51 for(i in fork) {
52 fork[i] = FORK_VACANT;
53 }
54 atomic {
55 for(i in fork) {
56 run Philosopher(i);
57 }
58 }
59 }

--- 正解

/*
* TOPSE-MC-20XX
* Dining Philosophers
*/

#define PHIL_NUM (2)

mtype = {THINKING, HUNGRY, EATING}; /* 哲学者：思考中, 空腹, 食事中 */
mtype = {FORK_IN_USE, FORK_VACANT}; /* フォーク：フォーク使用中, フォーク未使用 */
mtype = {HAND_HOLDING, HAND_EMPTY}; /* 手：（フォークを）握っている, 空 */

mtype fork[PHIL_NUM]; /* フォークの状態 */

proctype Philosopher(int no) {
mtype phil = THINKING; /* 哲学者の状態の初期化 */
mtype hand_r = HAND_EMPTY; /* 右手状態の初期化 */
mtype hand_l = HAND_EMPTY; /* 左手状態の初期化 */

do
::(phil == THINKING) -> /* 思考中 */
if
::true -> phil = HUNGRY;
::true -> skip;
fi;
::(phil == HUNGRY) -> /* 空腹 */
if
::(fork[no % PHIL_NUM] == FORK_VACANT) ->
hand_r = HAND_HOLDING;
fork[no % PHIL_NUM] = FORK_IN_USE;
fi;
if
::(fork[(no + 1) % PHIL_NUM] == FORK_VACANT) ->
hand_l = HAND_HOLDING;
fork[(no + 1) % PHIL_NUM] = FORK_IN_USE;
phil = EATING;
:: else ->
hand_r = HAND_EMPTY;
fork[no % PHIL_NUM] = FORK_VACANT;
fi;

::(phil == EATING) -> /* 食事中 */
if
::true -> hand_r = HAND_EMPTY;
hand_l = HAND_EMPTY;
fork[no % PHIL_NUM] = FORK_VACANT;
fork[(no + 1) % PHIL_NUM] = FORK_VACANT;
phil = THINKING;
::true -> skip;
fi;
::true -> skip;
od;
}

init {
int i;
for(i in fork) {
fork[i] = FORK_VACANT;
}
atomic {
for(i in fork) {
run Philosopher(i);
}
}
}

---

/**
* モデル検査入門Ⅱ Spin演習用プログラム
* @file 食事する哲学者問題の食事する哲学者
* @author M. Usami
*/
const redis = require('redis');
const util = require('util');
const crypto = require('crypto');

/** redisクライアント
* @constant
* @default
*/
const client = redis.createClient();

/**
* redisクライアント同期処理向け関数定義
*/
client.getAsync = util.promisify(client.get);
client.setAsync = util.promisify(client.set);
client.setnxAsync = util.promisify(client.setnx);
client.delAsync = util.promisify(client.del);

/** 右手
* @constant
* @type {Boolean}
* @default
*/
const RIGHT = true;
/** 左手
* @constant
* @type {Boolean}
* @default
*/
const LEFT = false;
/** 右手
* @constant
* @type {String}
* @default
*/
const RIGHT_HAND = 'Right Hand';
/** 左手
* @constant
* @type {String}
* @default
*/
const LEFT_HAND = 'Left Hand';

const STATUS = {
THINKING: 0,
HUNGRY: 1,
EATING: 2,
};

let countEating = 0

/**
* 同期スリープ関数
* await sleep(xxx) とawaitとセットで使用する
* @param {Number} msec スリープする時間（ミリ秒）
* @returns Promise
*/
const sleep = (msec) => new Promise(resolve => setTimeout(resolve, msec));

/**
* 引数の取得処理
* 引数が不正の場合はUsageを表示してプログラムを終了する
* @returns no,max no=哲学者の番号 max=哲学者の人数
*/
const init = () => {
let no = -1;
let max = -1;
if (process.argv.length >= 4) {
no = Number(process.argv[2]);
max = Number(process.argv[3]);
console.log(`Philosopher No:${no} Number of philosophers:${max}\n`);
if ((no < max) && (no >= 0 && no < 5) && (max > 1 && max <= 5)) {
return { no, max };
}
}
console.log("Usage: node index.js [no] [max]");
console.log(" no: Philosopher No (0 ~ 4)");
console.log(" max: Number of philosophers (2 ~ 5)");
process.exit(1);
}

/**
* RedisのKey-Valueを利用したロック処理
* @param {Number} no 哲学者No.
* @param {Number} val ロックのための乱数
* @returns val:成功 -1:失敗
*/
const lock = async (no, val) => {
return await client.setnxAsync(`lock-${no}`, `${val}`)
.then((val)=>{return val;})
.catch((err)=>{return -1;});
}

/**
* RedisKey-Valueを利用したアンロック処理
* @param {Number} no 哲学者No.
* @param {Number} val ロックのための乱数
* @returns 1:成功 -1:失敗
*/
const unlock = async (no, val) => {
if (val === await client.getAsync(`lock-${no}`)) {
return await client.delAsync(`lock-${no}`);
}
return -1;
}

/**
* プログラムのシャットダウン処理
* 使用したRedis内のKeyを全て削除する
* 3秒後に全てのキーを削除し、5秒後にプロセスを終了
*/
const shutdown = () => {
Philosopher.doing = false;
console.log("Start shutdown process");
for(let i = 0; i < 5; i++) {
setTimeout(() => {
client.del(`lock-${i}`);
}, 3000);
}
setTimeout(() => {
client.quit();
console.log("Completed shutdown process");
process.exit(0)
}, 5000);
}

/**
* 終了処理 SIGINT
*/
process.on('SIGINT', () => {
shutdown();
});

/**
* 終了処理 SIGTERM
*/
process.on('SIGTERM', () => {
shutdown();
});

/**
* 腕（手）
*/
class Hand {
/** ロック状態チェック周期時間(ミリ秒)
* @static
*/
static INTERVAL = 10;

/**
* コンストラクタ
* @param {Number} no 哲学者No.
* @param {Number} max 哲学者の人数
* @param {Boolean} side true=右手/false=左手
*/
constructor(no, max, side) {
this.side = side; // true=右手, false=左手
this.rnd = 0;
if (side === RIGHT) {
this.no = no % max;
this.str = RIGHT_HAND;
}
else {
this.no = (no + 1) % max;
this.str = LEFT_HAND;
}
}

/**
* フォークを1度だけ取得し、結果を返す
* @param {*} status
* @returns boolean | undefined
*/
async getOnce(status){
this.rnd = crypto.randomBytes(8).toString("hex");
if(status) {
return 1 === await lock(this.no, this.rnd)
}
}

/**
* フォーク取得
* @param {動作状態} status true=実行中/false=終了処理中
*/
async get(status) {
this.rnd = crypto.randomBytes(8).toString("hex");
while(status) {
if (1 === await lock(this.no, this.rnd)) {
console.log(` ${this.str} Fork acquisition => Succeeded : no=${this.no}`);
return;
}
console.log(` ${this.str} Fork acquisition => Failed : no=${this.no}`);
await sleep(Hand.INTERVAL);
}
}

/**
* フォーク解放
* @param {動作状態} status true=実行中/false=終了処理中
*/
async release(status) {
while(status) {
if (1 === await unlock(this.no, this.rnd)) {
console.log(` ${this.str} Fork release => Succeeded : no=${this.no}`);
return;
}
console.log(` ${this.str} Fork release => Failed : no=${this.no}`);
await sleep(Hand.INTERVAL);
}
}
}

/**
* 食事する哲学者クラス
*/
class Philosopher {
/** 動作状態（true=実行中/false=終了処理中）
* @static
*/
static doing = true;

/**
* コンストラクタ
* @param {Number} no 哲学者No.
* @param {Number} max 哲学者の人数
*/
constructor(no, max) {
this.no = no;
this.max = max;
this.status = STATUS.THINKING;
this.handRight = new Hand(no, max, RIGHT);
this.handLeft = new Hand(no, max, LEFT);
}

/**
* 思考中処理
*/
async think() {
console.log(`Philosopher ${this.no} Thinking`);
await sleep(crypto.randomInt(20) );
this.status = STATUS.HUNGRY;
}

/**
* 空腹中処理
*/
async hungry() {
console.log(`Philosopher ${this.no} Hungry`);
await sleep(crypto.randomInt(20) );

// if (Math.random() > 0.5) {
// await this.handRight.get(Philosopher.doing);
// await this.handLeft.get(Philosopher.doing);
// }
// else {
// await this.handLeft.get(Philosopher.doing);
// await this.handRight.get(Philosopher.doing);
// }

let successR = await this.handRight.getOnce(Philosopher.doing);
if(successR){
let successL = await this.handLeft.getOnce(Philosopher.doing);
if(successL){
this.status = STATUS.EATING;
}else{
await this.handRight.release(Philosopher.doing);
}
}
}

/**
* 食事中処理
*/
async eat() {
console.log(`Philosopher ${this.no} Eating ${countEating++}`);
await sleep(crypto.randomInt(20) );

await this.handRight.release(Philosopher.doing);
await this.handLeft.release(Philosopher.doing);

// if (Math.random() > 0.5) {
// await this.handRight.release(Philosopher.doing);
// await this.handLeft.release(Philosopher.doing);
// }
// else {
// await this.handLeft.release(Philosopher.doing);
// await this.handRight.release(Philosopher.doing);
// }
this.status = STATUS.THINKING;
}

/**
* 食事処理
* @param {Number} no 哲学者No.
* @param {Number} max 哲学者の人数
*/
async main() {
while(Philosopher.doing) {
switch(this.status) {
case STATUS.THINKING:
await this.think();
break;
case STATUS.HUNGRY:
await this.hungry();
break;
case STATUS.EATING:
await this.eat();
break;
}
}
}
};

let { no, max } = init();
phil = new Philosopher(no, max);
phil.main(no, max);