MY GOAL: Save generated executions from Herd7 against a specific memory model for further learning.


背景介绍

这个是我当前在做的事情之一，里头需要得到一个小 program 在某个特定的 relaxed memory models 下的所有 executions / traces.

经过调研，Herd7 是能够做到我想要的事情的。之前我还帮老板准备了一个使用 herd7 来体验不同的 RMM 的 lab, 写在另一篇博客里了。Herd7 能够输出以下边这样的图片的格式输出 executions: 显然在生成的过程中肯定会存有每幅图对应的中间状态，我的目标就是把这些中间状态打印到一个文件里存起来。

在这一篇博客里，我大致记录了整个实验、扩展的流程，对于想要了解 herd7 工具的实现的同学应该是会有一点帮助的吧，仅此而已了。除此之外的一点点干货可能就是 OCaml 的一点配置经验了吧。不知道会不会有人认真看完全文呢 😂

herd7 的代码可以在这里可以找到，我自己 fork 后修改的版本在这里。

这里我基于的是 v7.43 的版本。其实我原本还尝试过 diy v5.99 （diy 是旧版本的名字，v7 改名了）里的代码的，因为觉得旧版本的代码可能会更短小、更方便理解。但是我在旧版本下好像 make 一下就自动 build + install 了.. 不方便调试，也没有找到生成的中间文件路径用于 merlin-mode 的代码解析（这个真的很关键！！），所以就算了。而且我随便对比了两个版本下的几个文件，比如 top/top_herd, mem/mem, 好像并没有特别大的变化。反正最后也基本满足目标了呗 😁。

OCaml 开发环境配置

Herd7 是用 OCaml 写的，所以我得先学习一下 OCaml 这门语言。在12年听 coursera 上的 PL 课的时候学过一点点的 Standard ML, 除此之外对 OCaml 就没什么了解了。不过上手起来还是挺快的，我一直以来给自己的要求都是「3天之内能够上手任何一门新语言」。为了熟悉 OCaml,

  1. 看了 TryOCaml 的所有
  2. 看了 OCaml 官网上列出来的所有 tutorials
  3. 然后做了做 tutorials 里头的 99 problems 的一些题目。我发现这其实就是「算法题 in OCaml」嘛。。

这些果然就基本足够了。除了后来为了看懂 Herd7 里的一些 module / functor 的高级写法，又看了看 Real World OCaml 这本书。然后语言上就很熟悉了。

关于开发环境，我并没有找到 OCaml 的什么大型 IDE, 部分原因是 Emacs + Merlin-mode 就已经很强力了！！虽然这次我还没有怎么尝试 debugger, 光 printf 就做完了.. 不得不说，merlin mode 真的是超棒的！帮了大忙了。我最常用的两个功能是 jump to definition 和 show type information.

关于 merlin mode 以及 emacs 的设置，在这里有更加详细的介绍，我的 .emacs 里也有设置好的部分可供参考。

下边是一些 emacs 里使用 OCaml 相关的一些常用快捷键：（启用）

  • ctrl+c, ctrl+l：jump to definition. 在看代码的时候，这个几乎是最常用的了！
    • 要用这个的话，需要先配置好 ocaml-merlin
    • 我还自己添加了一个 .merlin 的配置文件（放在项目根目录下），描述哪些文件夹下有 source code, 哪些有 compiled binary file, 然后真的就脱胎换骨，效果拔群了！！感觉没有设置这个的话其实 merlin mode 也提供不了多大的好处..
  • ctrl+c, &: 回到刚才 jump to definition 之前的位置..
  • ctrl+t: 这个可以看选中部分（或者当前光标所在位置）的 type info, 有时候需要再按一次 ctrl+t 来显示完整的 type info.

代码理解

  1. 从 herd.ml 文件开始，在 let () = ... 那里开始是整个程序的 entry point,

    1. 先是读取命令行参数设置各种环境变量，放在 Opts 和 Model 这两个 module 内
    2. 然后从 from_file 函数开始解析，这个函数实际上是去调用 ParseTest.Top 这个 module, 其会根据配置好的 env 和 filename 来从这个 litmus test 文件中开始执行。
    3. 它会把所有在命令行参数中传入的 files 都这么去做一遍

  2. 所以下一步的重点是 parseTest.ml 文件中的 ParseTest.Top.from_file 函数，它会进一步调用内部的 do_from_file 函数：

    1. 先调用 Splitter 去解析 input litmus test program, 分出 initial state / program / final condition 等等不同的 section.
    2. 这个 Splitter module 似乎是个在其它地方也有用到的公用代码，反正具体实现我并不关心 😓
    3. 然后就可以根据 splitter 得到的 architecture 信息，调用不同的具体的 parser 来解析这个 litmus test 了。
      1. 这些 arch 有：PPC / ARM / AArch64 / X86 / MIPS / C / CPP / LISA
      2. 看起来，这些 litmus test 是一定要有一个 architecture 的，或许是因为不同的 architecture 有着各自的 keyword, 不同平台的就别混起来了！所以只有他们自己可以解析。

  3. 在 parseTest.ml parse 了 litmus test 的 syntax, 得到其 semantics 之后，会调用同一个文件里的 Top.Make 这个 module 调用其 run 函数，在这个 run 函数里，先生成了 Test_herd module (test_herd.ml), 应该只是定义了其内部的 state 包含哪些内容；然后通过 Top_herd module (top_herd.ml) 的 run 函数去真正执行——execute test according to model!

  4. 在 top_herd.ml 文件里可以看到，这里的 run 函数就是剩下的所有 generate + output 部分了。在一开始就调用了 mem.ml 中的 glommed_event_structures 函数：

    1. glommed_event_structures 的输出是一个 record, 里头的 too_far (bool) 说是可以丢弃一些 events, 我暂时不关心。重点是其中的第一个 field:
      1. event_structures : (int * S.M.VC.cnstrnts * S.event_structure) list ;
      2. 这里是 xxx list 所以已经是把所有可能的 execution graph 都给输出来了吧！！
      3. 第一个 int 我还不知道是啥，难道是在这个 list 中的编号？？
      4. 第二个 S.M.VC.cnstrnts, 唉，你们为啥不写全名呢 = =
      5. 第三个 S.event_structure 展开来是
        1. Sem.Semantics.event_structure
        2. 而 Sem.Semantics 会☞到 SemExtra.S 里头
        3. 而那里头的 event_structure 又会☞到 Event.S.event_structure 那里
        4. 所以这么一路下来最终要到 event.ml (~line160) 里头看每个 event structure graph 里头到底放了什么东西 = =
          1. procs
          2. events (set)
          3. intra_causality_data (relation) 类似于 data dependency 吧
          4. intra_causality_control (relation) 类似于 control dependency 吧
          5. control (relation) 似乎指的是 if 这种的
          6. data_ports (event set) 这个没太懂：Wvents that lead to the data port of a W. 所以是所有可能的 Write??
          7. output (event set) 应该是最终外界 visible 的那些 events 吧
        5. 而每个 event 是有一个 eeid 最为唯一标识的
    2. 不过，在这个 glommed_event_structures 里得到的 event structures 里似乎仅仅是 events 为主呀，像是给 event 编个号啊、一些最最基本的信息等等。在 SemExtra 中有一个更大的数据结构 —— concrete, 这个里头应该才是所有 output 的总集合，里头包括了：
      1. event structure, 这里是 Event 里头的 event_structure, 所以就是每个具体的 graph 有一个 concrete 咯
      2. rf map
        1. rfmap 的类型有点奇怪，是一个 write_to → read_from 的 map?!
        2. 其实 write_to 表示的是 “the event” to write to, 一个 write_to 是 to final (no further read) or another Load. 对应的，read_from 表示的是 “the event” to read from. 所以呀，这其实就是类似于俩 event 而已。
        3. 然后 write_to 作为 key, 其实就是 load event 作为 key, 因此是一个 rf-map 并非 wt-map 嘛
      3. final states
      4. po + iico
      5. po-same location
      6. pco: 似乎是 co 的 precursor
      7. store-load relation: 这里下边这4个是 deduced from rfmaps
      8. init-load relation
      9. last store relation
      10. atomic load / store relation
    3. 所以 很多函数里的 conc 参数原来说的就是 concrete 咯！
    4. 这个 concrete 我去搜了下（搜 S.concrete 或者 conc 关键字），它至少用在下边这么几个地方的：
      1. pretty.ml 这个就是输出到 .dot file 了
      2. XXXMem.ml 这个应该是用各个 architecture 的信息来 examine entire state, 看里头东西到底对不对，可以继续转到 Minimal / CAV12 / MachModelChecker 里去。
      3. 还有一个 kont function 马上就会说到了

  5. 然后，top_herd.ml 文件里在生成了 event_structure 之后，会通过 iter_rfms 函数去 generate and process rfmap. 这里才是真正真正得到 relation 的部分吧？！那个 kont 就是这里用的！

    1. 这个 iter_rfms 函数内部调用了 mem.ml 里的 calculate_rf_with_cnstrnts 函数，那个是有带着详细注释的，难得啊！甚至还有对于 kont 函数的描述，说是对于每个生成的 concrete event structures 都会调用一下 kont。就是在这里头 generate / process rfmap 的吧，里头会有 solve 等等的函数似乎可以决定具体的 rf relations.
      1. 所谓的 event structures 其实还是比较 abstract 的，因为：some values and even memory locations in them are variables
    2. 在 calculate_rf_with_cnstrnts 函数中会传入 kont 函数作为参数（传进来的是临时定义的 call_model），在这个函数里头：
      1. 当成功 solve constraints 的时候，会调用 fold_mem_finals 函数，在里头构建一个个 concrete instance!! 用 fold_cross 这个函数应该是用来一下生成多种不同的结果的吧。这里就是我想要关心的东西了呀！等下会说到，把这个生成的具体结果再根据 user-specified model 去验证一下，没问题的话就会输出打印了。
      2. 如没能成功 solve constraints 的话（cannot make such event structures concrete），会调用 when_unsolved 函数。如果判定是 unloop depth 不够或者 cyclic rfmaps 的话就会调用另一个专用函数 kont_loop 函数来做事情。不过我看在现在的代码中传进来的 kont_loop 函数仅仅是 fun c -> c 这样子，这个真的会有区别么 = = 所以我猜测应该还没有实现完全，不过跟我也没有关系了，我关心的 Litmu test 都是没有 loop 的
    3. 当能够成功 solve constraints, 得到一个 concrete 的时候，calculate_rf_with_cnstrnts 函数会调用在 top_herd.ml 里的 iter_rfms 函数里传入的 call_model 函数参数：
      1. 在 call_model 调用了 check_test 函数，它会去调用 XXXMem.ml 所定义的 check_event_structure 函数。比如说在 machModelCheck.ml (mach ≡ machine) 中的 check_event_structure 函数是下边这样的。除了这个之外，还有 CAV12.ml 和 minimal.ml 里的实现，所以显然是下边这个 mach 的最通用了吧。
      2. check_event_structure 里头是会引入 bell info. 这个 bell 我在 herd7 tool demo website 里见到过的，但是不知道它什么意思，猜测应该是一些具体的 configuration 吧。
      3. 如果声明了要有 co 的话，还会自动去生成 co / fr 呢
      4. 如果是 machModelChecker 的话，因为是针对 user specified model 嘛，所以最后会去调用 run_interpret 这个函数，传 kont 进去。这个会调用 interpreter.ml 里的代码，去 interpret 一个 user-specified model! interpreter.ml 好大呢，2k+ 行，基本就是他们的类 OCaml cat DSL 的 interpreter 了吧，我就不看了 😓
      5. 然后如果 interpretation 处理后的结果全部正确的话，会调用 kont 去输出：kont st res. 代码中的注释说的是：For all success call kont, accumulating results.

  6. 终于可以说具体的 kont 函数里头做了什么事情了，其实就是在 top_herd.ml 里的 model_kont ochan test cstr 函数，它返回的是一个函数：

    1. 它是这么用的：
      1. kont conc conc.S.fs st.I.out_show st.I.out_flags res (in machModelChecker.ml)
      2. kont conc conc.S.fs vb_pp Flag.Set.empty res (in CAV12.ml)
      3. kont conc conc.S.fs pp_relns Flag.Set.empty res (in minimal.ml)
    2. 所以可以确定它的参数分别表示：
      1. concrete state / final states / vbpp: print relations 的函数 / flags / c: results
    3. 接着我们再来看 model_kont 返回的函数里究竟做了什么事情。
    4. 首先，它有去看 -through 这个 flag —— 额外打印哪些 executions. -through all 表示无论对错都给打出来，像 -through none 就表示只有正确的才打印
    5. 然后去调用 check_prop test fsc, 去看这个 final states 到底符不符合，然后继续根据其它的参数一起决定 show_exec (bool) 与否。
    6. 然后，dump_legend (ine 244 - line 283)，然后收集一下 n-pos, n-neg 这种信息而已。然后就没有了。
    7. 等等，这个 dump_legend 函数其实不仅仅 dump 了 legend ——图片标题，还有其它东西的 = = （这个渣命名..！！）在 Pretty.dump_legend 里会去调用 pp_dot_event_structure, 所有的具体代码都在它的 worker function – do_pp_dot_event_structure (line 743) 里头了，注释还说：This complex function is not meant to be used directly, 我还能说什么.. ╮(╯_╰)╭ 反正我就是围观一下，确认一下那些个具体的 data 是从哪里取出来的，每一个 data 分别表示什么而已。

  7. 在调用 kont 的时候，肯定那些个 concrete / rfmaps / 啥等等等等的东西都已经确定了，所以我直接在这里 inject 保存我想要的东西就可以了！

  8. 在上边这些都执行完了之后，终于回到了 top_herd.ml 里的 run 函数 😂，里头剩下的部分都是输出到 terminal 的那些个 output 了，我就不太关心了。

上边是大致的流程，不过还有一个问题就是，在 pretty.ml 中具体是怎么抽取出关键的信息的呢，这里还是有点门道的：

  1. events
    1. 通过 dump_es_rfm_legend 函数可以学习 herd7 是怎么去读取 events 的。其实所有的操作都是通过调用 pp_dot_event_structure 这个函数来做的。
    2. 可以看到它会首先去 filter out events / rfs. 因为在命令行参数中可能会说哪些个 events 是不需要的。哪些个是需要的。然后对于 relations 的 select 其实就是只留下俩 event 都是 valid 的那些个。而对我们来说，就不用挑了吧，都打出来！
      1. 其实默认设定 PrettyConf.showevents 的值是 NON-REG-EVENTS.
      2. 通过 disable/enable select_es 的效果可以看出，NON-REG-EVENTS 会禁用掉 write to r1 这类的 events.
      3. 比如说 r1 := y 这样的东西，会变成 read y 和 write to r1 这样两个 events. 然后更新 r1 的 event 其实毫无意义了。毕竟真正 rf relation 去连的是 read y event 呀。所以这种 events 忽略掉完全没有问题！
      4. 所以我也和 Pretty 一样地 filter events.
    3. 对于 rf 的 filter 其实也是基于 events 的 filtering, 就是去挑出真正将要显示的那些 events 的 rf relation. 因此我也留着吧。
    4. 在这里一直有一个 vbss 的参数，我看了很久它到底是个什么东西..
      1. 在 top_herd 里有一个 vbpp 的东西，可以看出这就是将来传到 vbss 里的东西。可以通过 ctrl+c, ctrl+t 看到这个的类型是个 (string, relation) pair list. 然后随便针对测试例子打印出来，就可以发现，这个是额外要打印的 relations!! 就像 ghb / fr / co 这些（虽然 co 在 concrete 里也有）
      2. 至于 vb 到底表示啥.. 我不知道..
        1. 可能是 verbose, 毕竟只有 verbose level > 0 的时候才在 pretty.ml 中去打印的
        2. 也可能是 view-before, 在 pretty.ml 打印函数的最后一个部分 “A bunch of arrows” 那里有注释说到 viewed-before edges. 诶，viewed-before 是不是就是 fr 的别称？？
    5. do_pp_dot_event_structure 还有一个 mark 参数，我看了下，感觉像是 a set of events marked for debugging 啥的..
  2. po relations
    1. conc.po 就是！！直接打印就好了！！为什么 Pretty.ml 里头还要大费周章地重新算一遍..
  3. rf relations
    1. 其实直接遍历 rfmap 就可以了！
  4. co relations
    1. 也在 conc 里就有！另外 vbs 也有..
  5. fr relations
    1. vbs 里就有！
  6. other relations

就照着这么去改就改好了~ 😄

测试流程

因为每次 make all 之后构造出来的是 herd.native 这么个东西呀。所以我就 ln -s xxx/herd.native yyy/herd7 了一下，经过确认，重新编译之后，yyy/herd7 也的确是最新的，然后就好了。

不过这样是不够的，因为 stdlib.cat 这种东西找不到.. 在 src code 是有这些的，在 herd/libdir 文件夹下，然后在命令里加上 -I path/to/herd/libdir 就可以了

一点点体会

这是第一次看 functional language 的 real code. 感觉是：确实有些东西可以写的很简洁！但是让我非常困惑的是好些个变量的命名，「用一个字母命名」这个行为真的是太不友好了 >_<