命題:要求が発生したら常にリソースへのアクセスがそのうちに承認される。ただし、決して2つの要求を同時に承認してはならない。
AG.(要求が発生 U リソースへのアクセスが承認される) U ¬EF.(要求が発生 U リソースへのアクセスが承認される)
メモリリークが目に見えているし、最初の要求しか承認されない(笑)。何秒後とか指定できないよ。承認の解除まで入れたら時相論理が無限後退して破綻するよね。時相論理は命題論理の拡張だから真理値しか扱えない。AGのGとはグローバルな世界ではなくて、根としている世界のみを指すと考えたら簡単だよね(実質どちらで考えても結果は同じ)。強いUntilは「ならば」である。取り返せないセマフォだね。マニホールドを使って、私を欺き不正にセマフォを使うな!
実は私にとって、どんなコンピュータもシングルスレッド動作にしか見えないんだよね。遅いし。何GHzと謳っていようが、Pentium 100MHzから速度は変わってないし。Celeronだとむしろ100MHzより遅い。Core-i3でSSEを使った自作プログラムを実行すると熱暴走した。100回の小さなループをSSEでインライン展開しただけなのに。普段、Core-i7でもApple M4でもベクトル演算してる実感がない。ベクトル演算すると過熱するはずだ。ベクトル演算はArray.map(SISD)で十分だ。GPUがあった方が楽しいかもしれない。でもCirrus LogicのVRAM 1MBでDirectXのDiabloやLaguna Beachが動いた。Windows95 16MBだったけど十分な速度で動いた。解像度は低かったかもしれない。SPsはそこそこの性能で十分だ。失礼、SIMDがないなら、SPsもないね。SP単体ならあってもいいね。解像度とかリフレッシュレートとか条件を付ければ、ソフトウェアレンダリングも速いよ。究極的にはSP単体で、しかも、1を足すインクリメントと条件分岐しかなくても、チューリング完全なコンピュータができるよ。1を引くデクリメントは255回インクリメントしてオーバーフローすればいいから。それでいいじゃん。性能が低い方が道義的には安全だし。ビット反転と加算器を組み合わせてデクリメントを実装してもいいけどね。
半加算器と全加算器はわかるけど、予測機能付きの加算器なんて作れるわけないし。それこそ非自明な分岐だよね。そういうのは予測に失敗した時のペナルティーが大きいものだよ。回路のサイズが大きくなるのに性能が高くなるというのは分からないな。電力を相当犠牲にしている。32bitアドレス=4GBで十分だよ。メモリにマップするのに4GB以上のHDDやSSDにアクセスできるのは変だね。PAEとTLBとを相互に呼ぶことで無理やり拡張してるのだろう。使用した感覚としては64bit OSより32bit OSの方が速い。シングルスレッドのCPUでもPARCのAltoはメッセージループでGUIを実現した。AppleはAltoの技術を盗み、MSはAppleの技術を盗んだ。メッセージループで擬似マルチタスクできるから素晴らしい。あとはメッセージループにメッセージを挿入できるタイマーがあれば良い。タイマーはメッセージループのプログラム自体が空いたスロットにTESTメッセージを挿入し続けて、OSの時間カウンタを参照する。時間カウンタが設定した値を超えていれば、タイマーが発火する。メッセージループにプログラムもOSもドライバも全て詰め込めば良い。メッセージループは1つあれば良い。どんな計算機もそれしかできない。リング0は計算コストが高すぎる。一般的に仮想レイヤーを1つ追加すると性能は10分の1になると言われている。リングはもちろん再帰しても構わない。最も小さいリングはスピンロックと呼ばれる。
話は戻ってセマフォを立てたり下ろしたりできないなら、割り込みタイマーはウソだ。すると、プリエンプティブマルチタスクもウソになるよね。私が非自明な分岐が嫌いな理由がわかったかな?CTLでハードウェアの動作を検証してる。FDIVバグを教訓としているインテルみたいに。魔法は要らない。PromiseとかMaybeもこの命題と同型だよね。やっぱりコールバック地獄は解決できない。
時相論理はPrologと同じバックトラッキングである。バックトラッキングは消去法に等しい。消去法の計算量はO(nn)であり、バックトラッキングで減らせてもせいぜいO(nn-1)までである。自明だから言っておくけど、全て計算したら完璧に終わりだよね。どんどんコンピュータを使うといいよ