リサーチ
プログラミング言語とツールラボ
Memory Fairness
弱いメモリ設定では無限実行をどのように制限するべきなのか？その設定で並行プログラムはいつ終了するのか？私たちのプロジェクトはこのような質問に回答することを目的としています。
シーケンシャルの一貫性においては、終了などのもっとも単純な共有メモリの並行プログラムでさえも、活性プロパティは通常スケジュラーについてある程度の公平性を前提とすることを必要とします。弱いメモリモデルでは、スレッドの公平性の標準概念は不十分であり、追加の公平性プロパティ、メモリ公平性が必要です。このプロジェクトでは、SC、x86-TSO、RA、および StrongCOH などの演算型および宣言型メモリモデルの設定でメモリの公平性を定義することを提案し、低レベルの同期化を行う並行プログラムのモデルチェックと終了チェックの使用箇所を調査します。