2017/11/22 9:12 +0900、Paul E. McKenney <paulmck@xxxxxxxxxxxxxxxxxx> wrote: > On Wed, Nov 22, 2017 at 12:34:08AM +0900, Akira Yokosawa wrote: >>> From 180abe9a72d4e3fbe200ce2a032a6c616a70ce03 Mon Sep 17 00:00:00 2001 >> From: Akira Yokosawa <akiyks@xxxxxxxxx> >> Date: Wed, 22 Nov 2017 00:04:40 +0900 >> Subject: [PATCH 0/2] Add Makefile in CodeSamples/formal/herd >> >> (Resending with To: Paul) >> Hi Paul, >> >> This is my attempt to add Makefile in CodeSamples/formal/herd. >> The recipes here assumes that the memory-model's repository resides >> beside the perfbook's repository on your machine. >> >> The targets include conversion of litmus7 compatible tests under >> litmus/ directory to herd7/klitmus7 compatible ones, >> running converted litmus tests by herd7, >> running herd7 benchmark tests by herd7, >> and preparing directory for klitmus7 cross-compile of converted >> tests. >> >> Currently, there is no test other than benchmarks under herd/ >> directory which is not compatible with litmus7. When such tests >> are added there, the Makefile can be updated to run and cross-compile >> them along with the converted tests. >> >> Patch #1 adds the Makefile and a helper script. >> >> Patch #2 is a fix of compiler warnings revealed in klitmus7 cross- >> compiling. >> These C-WWC-o+o-* litmus tests were modified by me in this August. >> That looked sufficient for litmus7, but definitions in kernel header >> files used in klitmus7 aren't satisfied. The change here is the result >> of some try-and-errors. There can be smarter way to describe these tests. >> They are not used in the text at the moment, so their fix is not >> urgent, I suppose. > > I queued these, but let's talk about the memory model. Currently, > it is available in this git archive: > > https://github.com/aparri/memory-model.git > > Specifically, these files: > > linux-kernel.bell > linux-kernel.cat > linux-kernel.cfg > linux-kernel.def > linux-kernel-hardware.cat > lock.cat > > We hope to get these upstream into the Linux kernel during the next > merge window. So maybe the right thing to do is to require that the > user copy the files into the formal/herd directory, and have Makefile > give instructions and stop if they are not present. > > Thoughts? I’m kind of against having those untracked files there. The directory where they reside can be specified by overriding LKMM_DIR variable in the Makefile by an option to make command. So change of the location of memory model won’t be a problem. But yes, the check of the existence of the directory can help users. I’ll see what l can do. Thoughts? Akira (from mobile, might be QP encoded) > > Thanx, Paul > >> Thanks, Akira >> -- >> Akira Yokosawa (2): >> CodeSamples/formal/herd: Add Makefile and utility script >> CodeSamples/formal/litmus: Fix type of 2:r2 in C-WWC+o+o-*.litmus test >> >> CodeSamples/formal/herd/.gitignore | 4 ++ >> CodeSamples/formal/herd/Makefile | 60 ++++++++++++++++++++++ >> CodeSamples/formal/herd/litmus2herd.sh | 20 ++++++++ >> .../formal/litmus/C-WWC+o+o-data-o+o-addr-o.litmus | 9 ++-- >> .../formal/litmus/C-WWC+o+o-r+o-addr-o.litmus | 9 ++-- >> 5 files changed, 92 insertions(+), 10 deletions(-) >> create mode 100644 CodeSamples/formal/herd/.gitignore >> create mode 100644 CodeSamples/formal/herd/Makefile >> create mode 100644 CodeSamples/formal/herd/litmus2herd.sh >> >> -- >> 2.7.4 >> >> -- >> To unsubscribe from this list: send the line "unsubscribe perfbook" in >> the body of a message to majordomo@xxxxxxxxxxxxxxx >> More majordomo info at http://vger.kernel.org/majordomo-info.html >> > -- To unsubscribe from this list: send the line "unsubscribe perfbook" in the body of a message to majordomo@xxxxxxxxxxxxxxx More majordomo info at http://vger.kernel.org/majordomo-info.html
