メモリコンシステンシモデルとリトマステストについて (2. リトマステストについて)

メモリコンシステンシモデルの続き。続いてリトマステストについて調査する。

---

どうやってメモリコンシステンシモデルをテストするのか？

メモリコンシステンシをテストするためにはリトマステストというものを使用する。リトマステストは非常に小さなプログラムで複数コアの間でメモリアクセスをテストするものだ。リトマステストはまさに上記のxとyへの書き込みテストのようなものを実行し、その実行結果（つまりの値と の値）を想定する値と一致するか比較する。当然、ハードウェアの状態によって結果は異なるのだが、結果は以下の3つに分類されるはずだ。

• 絶対にPassしないパタン
• 時々Passするパタン
• 常にPassするパタン

例えば上記の例において、r0とr1の値がr0=0, r1=0となるのはシーケンシャルコンシステンシでのモデルの場合はあり得ない。しかし、x86のメモリコンシステンシモデルではこのような状況が発生するケースがある。

リトマステストでは、メモリコンシステンシモデルとを比較するために、

• で絶対にPassしないが、では時々Passする

というケースを探索する。コンパイラによる最適化の問題を探索するためには、

• 最適化前のプログラムと最適化後のプログラムで同じプログラムを実行し、その結果が異なるケースを探す。

そしてこれらの要求を満たすようなリトマステストを、自動制約ソルバーによって探せばよいわけでがそれは簡単な話ではない。問題なのは「～の結果が決して発生しない」というものをどうやって証明するかということだ。これは非常に難しい。

百聞は一見に如かず：litmus-tests-riscvに見るリトマステスト

では、litmus-tests-riscvリポジトリ生成されるリトマステストを観察して実際にどのようにテストを行っているのかチェックしよう。

RISC-Vのリトマステストを生成すると、hw-tests-srcに大量のテストソースコードが現れる。大量にあってどれを見ればよいのか分からなくなりそうだが、run.cがメインのファイルでそこに大量のテストが関数として呼ばれるようになっている。

• litmus-tests-riscv/hw-tests-src/run.c

/* Run all tests */
static void run(int argc,char **argv,FILE *out) {
  my_date(out);
  LB_2B_amoadd_2D_data_2D_amoadd_2E_rl_2B_amoadd_2E_aq_2D_data_2D_amoadd(argc,argv,out);
  LB_2B_amoadd_2D_data_2D_amoadds(argc,argv,out);
  LB_2B_amoadds(argc,argv,out);
...
    
int main(int argc,char **argv) {
  run(argc,argv,stdout);
  return 0;
}

ISA01というやつが簡単そうかもしれない。どんなテストを実行しているんだろう？

• litmus-tests-riscv/hw-tests-src/ISA01.c

int ISA01(int argc, char **argv, FILE *out) {
  cpus_t *def_all_cpus = read_force_affinity(AVAIL,0);
  if (def_all_cpus->sz < N) {
    cpus_free(def_all_cpus);
    return EXIT_SUCCESS;
  }
  cmd_t def = { 0, NUMBER_OF_RUN, SIZE_OF_TEST, STRIDE, AVAIL, 0, 0, aff_incr, 0, 1, AFF_INCR, def_all_cpus, NULL, -1, MAX_LOOP, NULL, NULL, -1, -1, -1, 0, 1};
  cmd_t cmd = def;
  parse_cmd(argc,argv,&def,&cmd);
  run(&cmd,def_all_cpus,out);
  if (def_all_cpus != cmd.aff_cpus) cpus_free(def_all_cpus);
  return EXIT_SUCCESS;
}

run()が実際にテストを実行する部分。テストコードはCPU0とCPU1で以下のように分けられている。

static void prelude(FILE *out) {
  fprintf(out,"%s\n","%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%");
  fprintf(out,"%s\n","% Results for tests/non-mixed-size/HAND/ISA01.litmus %");
  fprintf(out,"%s\n","%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%");
  fprintf(out,"%s\n","RISCV ISA01");
  fprintf(out,"%s\n","{0:x8=x; 1:x8=x;}");
  fprintf(out,"%s\n"," P0           | P1           ;");
  fprintf(out,"%s\n"," ori x6,x0,1  | ori x29,x0,4 ;");
  fprintf(out,"%s\n"," sw x6,0(x8)  | sw x29,0(x8) ;");
  fprintf(out,"%s\n"," ori x7,x0,2  | ori x30,x0,5 ;");
  fprintf(out,"%s\n"," sw x7,0(x8)  | sw x30,0(x8) ;");
  fprintf(out,"%s\n"," lw x10,0(x8) |              ;");
  fprintf(out,"%s\n"," ori x28,x0,3 |              ;");
  fprintf(out,"%s\n"," sw x28,0(x8) |              ;");
  fprintf(out,"%s\n","");
  fprintf(out,"%s\n","forall (0:x10=2 \\/ 0:x10=4 \\/ 0:x10=5)");
  fprintf(out,"Generated assembler\n");
  ass(out);
}

図に書き起こしてみよう。こんな感じ。

ではr0が取りうる値は何か？答えは簡単。2 / 4 / 5のいずれかとなる。

リトマステストでは、これを何回も実行し、想定する解になっているかをテストしているのだ。実行する回数はコマンド引数max_runによって設定される。

inline static int final_cond(int _out_0_x10) {
  switch (_out_0_x10) {
  case 5: case 4: case 2:
    return 1;
  default:
    return 0;
  }
}

inline static int final_ok(int cond) {
  return !cond;
}

static void run(cmd_t *cmd,cpus_t *def_all_cpus,FILE *out) {
  if (cmd->prelude) prelude(out);
  tsc_t start = timeofday();
  param_t prm ;
/* Set some parameters */
  prm.verbose = cmd->verbose;
  prm.size_of_test = cmd->size_of_test;
  prm.max_run = cmd->max_run;    // 最大繰り返し実行回数

このように、リトマステストはセルフチェックテストの形で実行される。あとは、パタンを切り替えながらひたすら繰り返し実行していくということになる。なかなか時間のかかりそうなテストだということが分かった。