TLA+に再挑戦（2022.2）

development tlaplus

英語のドキュメント を読んだけどあまり理解できてなかったので 日本語 で再挑戦する会。

今回

2022.2 実践TLA+もくもく会 - connpass

  • 「6章 時相論理」を読んだり試したり
  • 次回から第2部、「7章 アルゴリズム」

感想

  • デッカーのアルゴリズム
    • 厳密に交互にとっていく素朴なアルゴリズムを避けて発明された世界初の相互排他アルゴリズムの1つである。
  • スレッド数2の場合にしか成立しない
    • 3つ目のスレッドを追加すると、CSに進入できないスレッドが現れる
    • リソーススタベーション と呼ぶ
  • つまり TLA+/PlusCal でやっているのは、プログラムの実行中に生じる振る舞いをデータフローとして記述して、それをシミュレーションしているのだった

次回

2022.3 実践TLA+もくもく会 - connpass

参考リンク