やったこと #

大学院の講義の課題 #

cafeobjでMutexプロトコルの動作のシミュレーターを作った。 字面だけ聞くと凄そうだが以下の様に全部丁寧な手作り状態遷移という感じ。 lockedの操作もAtomicなものではない。 全てのプロセスは共有リソースを使わないRemainder Sectionとロックの値を変更するModifying Sectionと共有リソースを使うCritical Sectionの３つの状態を遷移し、Critical Sectionなプロセスは同時に１つしかありえないという当たり前といば当たり前なプロトコルがMutexである。（ハズ…) cafeobjという代数仕様言語で実際に記述することで、Mutexに対する脳内等式推論が少し体験できた。

eq trans((locked: true,pc1: rs, pc2: L2, pc3: L3, pc4: L4),t1)
= (locked: true,pc1: rs, pc2: L2, pc3: L3, pc4: L4) .
eq trans((locked: false,pc1: rs,pc2: L2, pc3: L3, pc4: L4),t1)
= (locked: false,pc1: ms,pc2: L2, pc3: L3, pc4: L4) .
eq trans((locked: B,pc1: ms, pc2: L2, pc3: L3, pc4: L4),t1)
= (locked: true,pc1: cs, pc2: L2, pc3: L3, pc4: L4) .
eq trans((locked: B,pc1: cs, pc2: L2, pc3: L3, pc4: L4),t1)
= (locked: false,pc1: rs,pc2: L2, pc3: L3, pc4: L4) .

学び #

読書 #

数学的考え方が全然できないので、問題解決のための「アルゴリズム×数学」が基礎からしっかり身につく本を読んでいる。

今日は包除原理を具体的にコードにした。 実際の提出コード

要は

|P∪Q| = |P| + |Q| - |P∩Q|

なので理解が難しい原理というわけではないが、この原理が問題に使えると気づくのはできないんだよな… 後Google日本語入力で「わしゅうごう」で変換すると∪、「せきしゅうごう」で変換すると∩が出てきて気分が良かった。