How concurrecy works: A visual guide | Waqas Younas’ blog を読んだ
- 並行プログラミングの視覚化により理解を促す記事である
- 単純な3行のコードを例に用いている
- 単独プロセスのプログラムの状態を変数の値と実行行番号で表わす
- 2つのプロセスP,Qのプログラムの状態を変数の値とPの実行行番号、Qの実行行番号であらわす
- このよう状態空間を定義すると数十プロセスは指数関数的に複雑になる
- モデルチェッカー(SPINやTLA+)では線形時相論理を利用することができる