Monthly Archives: 2月 2011

「SPINモデル検査入門」第5回(2月25日)

Posted on by 0 comment

参加者 沼田(読み手)、今井(記)
範囲 pp. 42 – 58

第3章 並行性

  • 3.6 干渉の問題:再考
  • 3.7 文の決定性実行
  • 3.8 表明を用いた検証
    • p.46 ~ p.47の実行結果
      • 最初に動いたプロセスが 2 p だから、2行目のp(1):tempが0は、p(2):tempが0ではないか? (または、最初に動いたプロセスが2 Pではなく1 Pではないか)
      • 最後の行
        0 :init 16 _nr_pr==1
        の16は17の間違い?ソースコード3.5(p.43)では、(_nr_pr == 1) -> はline 17。
  • 3.9 保護領域の問題
    • p.51
      spin: line 23 “cs.pml”, Error: assertion violated
      の、line 23 は line 22 の間違い?ソースコード3.8で assert (critical <= 1);は、line 22。

第4章 同期機構

  • 4.1 一時停止による同期
    • p.54
      ソースコード 4.1 はデッドロックする可能性があるけど、そのことには触れていないね。
      → ソースコード 4.2のキャプションが、「デッドロックのある同期」になっているので、4.2触れているのでは?
  • 4.2 文の実行性
    • デッドロックの件、触れてなかった。この後の節で触れる?

「SPINモデル検査入門」第4回(2月22日)

Posted on by 0 comment

参加者 今井(読み手)、青木、沼田(記)
範囲 pp. 31 – 42

第3章 並行性

  • 並行と並列
    • 原書を見ると、タイトルのConcurrencyは平行性、第一段落末尾のconcurrent programmingは並列プログラミングと訳されているようです。
    • 並行/並列/分散といった用語については、ASCII.jpキャリアに掲載されている今さら聞けないIT英語の中に、データ処理に関するIT英語「concurrent」「parallel」「distributed」、という記事がありました。
  • 3.1 インタリーブ実行
    • p.33 の表の下に書かれている出力
      上段:計算1、計算2、計算3、下段:計算4、計算5、計算6の順に並んでいるとすると、計算3と計算6が間違っている?計算3は「Process P, n = 2」に、計算6は「Process P, n = 1」になるのでは?
      Errataに計算3については記載されています(Page 31, line 3)。
    • 3.1.1 計算の表示
      • jSpin
        下から3行目の実行され式のソースコード は 実行されでは?
      • コマンドライン
        下から3行目のprintf(Q)は printf(P)の誤植?
  • 3.2 原子性
  • 3.3 対話的シミュレーション
  • 3.4 プロセス間干渉
  • 3.5 複数プロセス群

「SPINモデル検査入門」第3回(2月18日)

Posted on by 0 comment

参加者 沼田(読み手)、青木(記)
範囲 pp. 16 – 30

第1章 Promela逐次モデル記述

  • 1.7 繰り返し
    • 1.7.1 カウントループ
  • 1.8 ジャンプ文*

第2章 逐次モデルの検証

  • 2.1 表明
  • 2.2 SPINによる検証
    • 2.2.1 ガイド付きシミュレーション
    • 2.2.2 実行状況の表示

「SPINモデル検査入門」第2回(2月15日)

Posted on by 0 comment

参加者 青木(読み手)、沼田、今井(記)
範囲 pp. 6 – 16

第1章 Promela逐次モデル記述

  • 1.3 データタイプ
    • 1.3.1 タイプ変換
      • p.6
        321(10) = 141(16), 41(16) = 65(10)
  • 1.4 オペレータと式
    • 1.4.1 局所変数
      • p.8
        間違いやすそう。暗黙のうちにプロセスの最初に移されるより、プロセス途中の変数宣言は明示的にエラーにしてもらうほうが嬉しいかも。
    • 1.4.2 値の記号化
  • 1.5 制御文
  • 1.6 分岐選択文
    • p.12 ソースコード 1.4 の、b * b – 4 * a * c の意味
      ax2 + bx + c = 0x について解くと x = (-b ± √(b2 – 4ac)) / 2a
      b2 – 4ac が、
      < 0 の時は、2乗して負になる値なので実数ではない(虚数)
      = 0 の時は、x = -b / 2a で一つ
      > 0 の時は、x = (-b + √(b2 – 4ac)) / 2a, (-b – √(b2 – 4ac)) / 2a で二つ
    • 1.6.1 条件式

「SPINモデル検査入門」第1回(2月8日)

Posted on by 0 comment

参加者 今井(読み手)、沼田、青木(記)
範囲 pp. iii – 6

日本語版発行によせて
・上梓:文字を版木に刻むこと。また、書物を出版すること。(Yahoo!辞書 大辞林 (国語辞書)より)
・ACM:Association for Computing Machineryの略。アメリカ合衆国の情報工学分野の学会(ウィキペディアより)。

監訳者前書き

序言

前書き

目次

第1章 Promela逐次モデル記述

  • 1.1 最初のPromelaモデル記述
  • 1.2 ランダムシミュレーション
  • 1.3 データタイプ

「Java並行処理プログラミング」第36回(2月4日)

Posted on by 0 comment

参加者 沼田(読み手)、今井(記)
範囲 pp. 388 – 402

第IV部 高度な話題

第16章 Javaのメモリモデル

  • 16-2 公開
  • 16-2-1 安全でない公開
  • 16-2-2 安全な公開
  • 16-2-3 安全な初期化の慣用句(イディオム)
  • 16-2-4 ダブルチェックロッキング
  • 16-3 初期化の安全性
  • まとめ

付録A 並行処理のためのアノテーション

  • A-1 クラスのアノテーション
  • A-2 フィールドとメソッドのアノテーション
    • p.398 l.7
      ステート変数を加えて → ステート変数を加えて

訳者あとがき

————————

「Java並行処理プログラミング」読了。
次回から「SPINモデル検査入門」を読みます。

「Java並行処理プログラミング」第35回(2月1日)

Posted on by 0 comment

参加者 今井(読み手)、沼田(記)
範囲 pp. 381 – 388

第IV部 高度な話題

第16章 Javaのメモリモデル

  • 16-1 メモリモデルとは何か?なぜ必要か?
    • 16-1-2 順序変え
    • 16-1-3 Javaのメモリモデルを2000字以内で説明する
      • p.384 プログラム順序のルールは、データフローの関連のあるアクションがあれば順に実行されるということ?
    • 16-1-4 同期化の相乗り