なぜ動くのか？

書いといてなんだが、実はなぜこれで動くのか納得し難かったりする。もうちょっと安心できる形で正当性を示しときたい。

CPUの立場になって考えてみる。マイクロスレッドの起動から最初に戻って来るまでの手順(すなわちexec()でマイクロスレッドを呼び出し、suspend()で戻る)を書き下してみると次の通り。

1. exec()前のコード(Pとおく)を実行
2. exec()呼び出し
   1. S1〜Smをスタックに保存
   2. PR(exec()からの戻り先)をスタックに保存
   3. ssp初期化
   4. SPとsspをswap
   5. PR = 呼び出し先関数(bar()とする)のアドレス
   6. PRが指すアドレスにジャンプ(これ以降bar()内)
3. bar()先頭から最初のsuspend()呼び出しまでのコード(Qとおく)を実行
4. suspend()呼び出し
   1. S1〜Smをスタックに保存
   2. PR(suspend()からの戻り先；bar()内)をスタックに保存
   3. SPとsspをswap
   4. PRをスタックから復旧
   5. Sm〜S1をスタックから復旧
   6. PRが指すアドレスにジャンプ

ステップ2.3.〜2.4、およびステップ4.3.を(Cが走るまっとうなCPUなら)汎用レジスタのうちS1〜Smを破壊することなく遂行可能なことはすでに示した。
結局、ステップ2.3.〜4.3までの過程で起きる破壊は、次の3種類だけである。

• Type A: マイクロスレッドbar()ローカルな記憶(sspとstk[])の書き換え
• Type B: S1〜Sm以外の汎用レジスタ(RuとRt)の破壊
• Type C: コードQによる大域記憶経由の副作用(もしあれば)

このことを憶えといた上で、最初の手順からステップ2.5.〜4.2.を削除してみると、次のようになる。

1. exec()前のコード(Aとおく)を実行
2. exec()呼び出し
   1. S1〜Smをスタックに保存
   2. PR(exec()からの戻り先)をスタックに保存
   3. ssp初期化
   4. SPとsspをswap
   5. SPとsspをswap
   6. PRをスタックから復旧
   7. Sm〜S1をスタックから復旧
   8. PRが指すアドレスにジャンプ

ステップ2.3.でsspに与える初期値は、この流れの中では使われない。ステップ2.4.と2.5.は互いに効果を打ち消す。また、レジスタについて見るとPRやS1〜Smは単にスタックに出し入れされるだけ。よって、これらを除去してもアルゴリズムとして等価なはず。なので除去すると、次の手順となる。

1. exec()前のコード(Pとおく)を実行
2. exec()呼び出し
   1. PRが指すアドレスにジャンプ

結局、exec()は、呼び出し元のコンテキストから見て、上述の3種類の破壊(Type A〜C)があるものの、他に何もしない関数と等価である。Rt, Ruの破壊(Type B)は、今想定している関数呼び出し規約上は問題ない。つまり上記exec()の呼び出しは正当であり、普通に呼び出し元に戻ってくる。

suspend(), resume()についても同様の手順で正当性を示せるはず。

厳密な証明として、数学的帰納法の適用も、同様の線にそって多分可能、
だといいﾅｱ、、(´Д`)