> Do you mean the one example in Table 3? > What about cmpxchg() or cmpxchg_acquire()? Yes, Table 3. The cmpxchg*() primitives were not discussed in the paper. IIRC, their representation has not changed since at least 1c27b644c0fd. > We're definitely getting rid of some lines in herd7, that have been added > solely for dealing with this specific case of LKMM. Good. If the herd7 maintainers are "tired" of dealing with those lines, that's definitely a big fat "why" to put in a changelog. > Deal with what, no longer having to learn OCaml to be sure that the LKMM's > formal definition matches the description in memory_barriers.txt? Nope. ;-) Dealing with the review, testing, and maintainance of a new representation. > - it makes it easier to maintain the LKMM in the future, because you don't > have to work around hidden transformations inside herd7 > - it makes implicit behavior explicit > - it makes it easier to understand that the formalization matches the > intention > - it makes it easier to learn the LKMM from the formalization without having > to cross-reference every bit with the informal documentation to avoid > misunderstandings Jonas - You write "less hidden", "less implicit", but I keep reading "a representation I/some people would expect". We've already acknowledged that's no deciding factor to abandon the current seasoned representation. Andrea
