Linux RCU テストや CBMC 分析用の pthread ラッパー__CPROVER_fence("RRfence", "RWfence");などのプロジェクトで使用されているようなコードを目にします。オンライン ドキュメントを見ましたが、この CBMC 関数に送信された文字列に関するテキストは見つかりませんでした。
に使用できるパラメータは何__CPROVER_fenceですか?
私の見解では、実際の実装によって実行されるバリア/フェンスを示すのは注釈/機能です。つまり、実際の機能の分析スタブです。明らかに、パラメータはバリアのタイプを示していますが、実際のパラメータと対応するバリア タイプへの参照は見つかりませんでした。つまり、「RRFence」は読み取りフェンスです。これは、この時点より前の読み取りが、この時点以降の読み取りの前に完了することを意味します (推測として)。